Showing 1–13 of 13 results for author: Baaz, M

Skolemization In Intermediate Logics

Authors: Matthias Baaz, Mariami Gamsakhurdia, Rosalie Iemhoff, Raheleh Jalali

Abstract: Skolemization, with Herbrand's theorem, underpins automated theorem proving and various transformations in computer science and mathematics. Skolemization removes strong quantifiers by introducing new function symbols, enabling efficient proof search algorithms. We characterize intermediate first-order logics that admit standard (and Andrews) Skolemization. These are the logics that allow classica… ▽ More Skolemization, with Herbrand's theorem, underpins automated theorem proving and various transformations in computer science and mathematics. Skolemization removes strong quantifiers by introducing new function symbols, enabling efficient proof search algorithms. We characterize intermediate first-order logics that admit standard (and Andrews) Skolemization. These are the logics that allow classical quantifier shift principles. For some logics not in this category, innovative forms of Skolem functions are developed that allow Skolemization. Moreover, we analyze predicate intuitionistic logic with quantifier shift axioms and demonstrate its Kripke frame-incompleteness. These findings may foster resolution-based theorem provers for non-classical logics. This article is part of a larger project investigating Skolemization in non-classical logics. △ Less

Submitted 26 January, 2025; originally announced January 2025.

Epsilon Calculus Provides Shorter Cut-Free Proofs

Authors: Matthias Baaz, Anela Lolic

Abstract: In this paper we show that cut-free derivations in the epsilon format of sequent calculus provide for a non-elementary speed-up w.r.t. cut-free proofs in usual sequent calculi in first-order language. In this paper we show that cut-free derivations in the epsilon format of sequent calculus provide for a non-elementary speed-up w.r.t. cut-free proofs in usual sequent calculi in first-order language. △ Less

Submitted 17 January, 2024; originally announced January 2024.

First-Order Interpolation Derived from Propositional Interpolation

Authors: Matthias Baaz, Anela Lolic

Abstract: This paper develops a general methodology to connect propositional and first-order interpolation. In fact, the existence of suitable skolemizations and of Herbrand expansions together with a propositional interpolant suffice to construct a first-order interpolant. This methodology is realized for lattice-based finitely-valued logics, the top element representing true. It is shown that interpolatio… ▽ More This paper develops a general methodology to connect propositional and first-order interpolation. In fact, the existence of suitable skolemizations and of Herbrand expansions together with a propositional interpolant suffice to construct a first-order interpolant. This methodology is realized for lattice-based finitely-valued logics, the top element representing true. It is shown that interpolation is decidable for these logics. △ Less

Submitted 13 February, 2020; originally announced February 2020.

Effective Finite-Valued Approximations of General Propositional Logics

Authors: Matthias Baaz, Richard Zach

Abstract: Propositional logics in general, considered as a set of sentences, can be undecidable even if they have "nice" representations, e.g., are given by a calculus. Even decidable propositional logics can be computationally complex (e.g., already intuitionistic logic is PSPACE-complete). On the other hand, finite-valued logics are computationally relatively simple - at worst NP. Moreover, finite-valued… ▽ More Propositional logics in general, considered as a set of sentences, can be undecidable even if they have "nice" representations, e.g., are given by a calculus. Even decidable propositional logics can be computationally complex (e.g., already intuitionistic logic is PSPACE-complete). On the other hand, finite-valued logics are computationally relatively simple - at worst NP. Moreover, finite-valued semantics are simple, and general methods for theorem proving exist. This raises the question to what extent and under what circumstances propositional logics represented in various ways can be approximated by finite-valued logics. It is shown that the minimal $m$-valued logic for which a given calculus is strongly sound can be calculated. It is also investigated under which conditions propositional logics can be characterized as the intersection of (effectively given) sequences of finite-valued logics. △ Less

Submitted 3 August, 2019; originally announced August 2019.

Comments: arXiv admin note: substantial text overlap with arXiv:math/0203204

MSC Class: 03B50

Journal ref: Avron, Arnon; Dershowitz, Nachum; Rabinovich, Alexander (Eds.). Pillars of Computer Science. LNCS 4800. Berlin: Springer, 2008. 107-129

Epsilon Theorems in Intermediate Logics

Authors: Matthias Baaz, Richard Zach

Abstract: Any intermediate propositional logic (i.e., a logic including intuitionistic logic and contained in classical logic) can be extended to a calculus with epsilon- and tau-operators and critical formulas. For classical logic, this results in Hilbert's $\varepsilon$-calculus. The first and second $\varepsilon$-theorems for classical logic establish conservativity of the $\varepsilon$-calculus over its… ▽ More Any intermediate propositional logic (i.e., a logic including intuitionistic logic and contained in classical logic) can be extended to a calculus with epsilon- and tau-operators and critical formulas. For classical logic, this results in Hilbert's $\varepsilon$-calculus. The first and second $\varepsilon$-theorems for classical logic establish conservativity of the $\varepsilon$-calculus over its classical base logic. It is well known that the second $\varepsilon$-theorem fails for the intuitionistic $\varepsilon$-calculus, as prenexation is impossible. The paper investigates the effect of adding critical $\varepsilon$- and $τ$-formulas and using the translation of quantifiers into $\varepsilon$- and $τ$-terms to intermediate logics. It is shown that conservativity over the propositional base logic also holds for such intermediate $\varepsilonτ$-calculi. The "extended" first $\varepsilon$-theorem holds if the base logic is finite-valued Gödel-Dummett logic, fails otherwise, but holds for certain provable formulas in infinite-valued Gödel logic. The second $\varepsilon$-theorem also holds for finite-valued first-order Gödel logics. The methods used to prove the extended first $\varepsilon$-theorem for infinite-valued Gödel logic suggest applications to theories of arithmetic. △ Less

Submitted 30 November, 2021; v1 submitted 9 July, 2019; originally announced July 2019.

MSC Class: 03F05; 03B20; 03B55

An interpolant in predicate Gödel logic

Authors: Matthias Baaz, Mai Gehrke, Sam van Gool

Abstract: A logic satisfies the interpolation property provided that whenever a formula Δ is a consequence of another formula Γ, then this is witnessed by a formula Θ which only refers to the language common to Γ and Δ. That is, the relational (and functional) symbols occurring in Θ occur in both Γ and Δ, Γ has Θ as a consequence, and Θ has Δ as a consequence. Both classical and intuitionistic predicate log… ▽ More A logic satisfies the interpolation property provided that whenever a formula Δ is a consequence of another formula Γ, then this is witnessed by a formula Θ which only refers to the language common to Γ and Δ. That is, the relational (and functional) symbols occurring in Θ occur in both Γ and Δ, Γ has Θ as a consequence, and Θ has Δ as a consequence. Both classical and intuitionistic predicate logic have the interpolation property, but it is a long open problem which intermediate predicate logics enjoy it. In 2013 Mints, Olkhovikov, and Urquhart showed that constant domain intuitionistic logic does not have the interpolation property, while leaving open whether predicate Gödel logic does. In this short note, we show that their counterexample for constant domain intuitionistic logic does admit an interpolant in predicate Gödel logic. While this has no impact on settling the question for predicate Gödel logic, it lends some credence to a common belief that it does satisfy interpolation. Also, our method is based on an analysis of the semantic tools of Olkhovikov and it is our hope that this might eventually be useful in settling this question. △ Less

Submitted 12 February, 2019; v1 submitted 8 March, 2018; originally announced March 2018.

Unsound Inferences Make Proofs Shorter

Authors: Juan P. Aguilera, Matthias Baaz

Abstract: We give examples of calculi that extend Gentzen's sequent calculus LK by unsound quantifier inferences in such a way that (i) derivations lead only to true sequents, and (ii) proofs therein are non-elementarily shorter than LK-proofs. We give examples of calculi that extend Gentzen's sequent calculus LK by unsound quantifier inferences in such a way that (i) derivations lead only to true sequents, and (ii) proofs therein are non-elementarily shorter than LK-proofs. △ Less

Submitted 6 May, 2019; v1 submitted 27 August, 2016; originally announced August 2016.

Comments: 21 pages. July 2017 preprint

Journal ref: J. symb. log. 84 (2019) 102-122

First-order Goedel logics

Authors: Matthias Baaz, Norbert Preining, Richard Zach

Abstract: First-order Goedel logics are a family of infinite-valued logics where the sets of truth values V are closed subsets of [0, 1] containing both 0 and 1. Different such sets V in general determine different Goedel logics G_V (sets of those formulas which evaluate to 1 in every interpretation into V). It is shown that G_V is axiomatizable iff V is finite, V is uncountable with 0 isolated in V, or e… ▽ More First-order Goedel logics are a family of infinite-valued logics where the sets of truth values V are closed subsets of [0, 1] containing both 0 and 1. Different such sets V in general determine different Goedel logics G_V (sets of those formulas which evaluate to 1 in every interpretation into V). It is shown that G_V is axiomatizable iff V is finite, V is uncountable with 0 isolated in V, or every neighborhood of 0 in V is uncountable. Complete axiomatizations for each of these cases are given. The r.e. prenex, negation-free, and existential fragments of all first-order Goedel logics are also characterized. △ Less

Submitted 7 January, 2006; originally announced January 2006.

Comments: 37 pages

MSC Class: 03B50; 03B52; 03B55

Characterization of the Axiomatizable Prenex Fragments of First-Order Goedel Logics

Authors: Matthias Baaz, Norbert Preining, Richard Zach

Abstract: The prenex fragments of first-order infinite-valued Goedel logics are classified. It is shown that the prenex Goedel logics characterized by finite and by uncountable subsets of [0, 1] are axiomatizable, and that the prenex fragments of all countably infinite Goedel logics are not axiomatizable. The prenex fragments of first-order infinite-valued Goedel logics are classified. It is shown that the prenex Goedel logics characterized by finite and by uncountable subsets of [0, 1] are axiomatizable, and that the prenex fragments of all countably infinite Goedel logics are not axiomatizable. △ Less

Submitted 1 March, 2003; originally announced March 2003.

Comments: 6 pages; forthcoming in ISMVL 2003

MSC Class: 03B50 (Primary) 03B52; 03B55 (Secondary)

Journal ref: 33rd International Symposium on Multiple-valued Logic. Proceedings. Tokyo, May 16-19, 2003 (IEEE Computer Society Press, 2003) 175-180

n=3 Nilpotent differential calculus on some non-commutative (super) spaces

Authors: M. El Baz, A. El Hassouni, Y. Hassouni, E. H. Zakkari

Abstract: In this paper, we construct a covariant differential calculus on quantum plane with two-parametric quantum group as a symmetry group. The two cases $d^2=0$ and $d^3=0$ are completly established. We also construct differential calculi $n=2$ and $n=3$ nilpotent on super quantum space with one and two-parametric symmetry quantum supergroup. In this paper, we construct a covariant differential calculus on quantum plane with two-parametric quantum group as a symmetry group. The two cases $d^2=0$ and $d^3=0$ are completly established. We also construct differential calculi $n=2$ and $n=3$ nilpotent on super quantum space with one and two-parametric symmetry quantum supergroup. △ Less

Submitted 1 March, 2004; v1 submitted 25 March, 2003; originally announced March 2003.

MSC Class: 81R60

Approximating Propositional Calculi by Finite-valued Logics

Authors: Matthias Baaz, Richard Zach

Abstract: Bernays introduced a method for proving underivability results in propositional calculi by truth tables. In general, this motivates an investigations of how to find, given a propositional logic, a finite-valued logic which has as few tautologies as possible, but which has all the valid formulas of the given logic as tautologies. It is investigated how far this method can be carried using (1) one… ▽ More Bernays introduced a method for proving underivability results in propositional calculi by truth tables. In general, this motivates an investigations of how to find, given a propositional logic, a finite-valued logic which has as few tautologies as possible, but which has all the valid formulas of the given logic as tautologies. It is investigated how far this method can be carried using (1) one or (2) an infinite sequence of finite-valued logics. It is shown that the best candidate matrices for (1) can be computed from a calculus, and how sequences for (2) can be found for certain classes of logics (including, in particular, logics characterized by Kripke semantics). △ Less

Submitted 19 March, 2002; originally announced March 2002.

Comments: 20 pages

MSC Class: 03B50 (Primary); 03B45; 03B60 (Secondary)

Journal ref: 24th International Symposium on Multiple Valued Logic. Boston. Proceedings (IEEE Press, Los Alamitos, 1994) 257-263

Quantified propositional Goedel logics

Authors: Matthias Baaz, Agata Ciabattoni, Richard Zach

Abstract: It is shown that G-up, the quantified propositional Goedel-Dummett logic based on the truth-values set V-up = {1 - 1/n : n >= 1} u {1}, is decidable. This result is obtained by reduction to Buechi's theory S1S. An alternative proof based on elimination of quantifiers is also given, which yields both an axiomatization and a characterization of G-up as the intersection of all finite-valued quantif… ▽ More It is shown that G-up, the quantified propositional Goedel-Dummett logic based on the truth-values set V-up = {1 - 1/n : n >= 1} u {1}, is decidable. This result is obtained by reduction to Buechi's theory S1S. An alternative proof based on elimination of quantifiers is also given, which yields both an axiomatization and a characterization of G-up as the intersection of all finite-valued quantified propositional Goedel logics. △ Less

Submitted 3 October, 2000; v1 submitted 17 June, 2000; originally announced June 2000.

Comments: v.2: 17 pages, revised published version (v.1: 15 pages)

MSC Class: 03B50; 03B55

Journal ref: Michel Parigot, Andrei Voronkov (Eds.): Logic for Programming and Automated Reasoning. 7th International Conference, LPAR 2000, Reunion Island, France, November 11-12, 2000. Lecture Notes in Computer Science, Vol. 1955, Springer, 2000. pp. 240-256

Hypersequents and the Proof Theory of Intuitionistic Fuzzy Logic

Authors: Matthias Baaz, Richard Zach

Abstract: Takeuti and Titani have introduced and investigated a logic they called intuitionistic fuzzy logic. This logic is characterized as the first-order Goedel logic based on the truth value set [0,1]. The logic is known to be axiomatizable, but no deduction system amenable to proof-theoretic, and hence, computational treatment, has been known. Such a system is presented here, based on previous work o… ▽ More Takeuti and Titani have introduced and investigated a logic they called intuitionistic fuzzy logic. This logic is characterized as the first-order Goedel logic based on the truth value set [0,1]. The logic is known to be axiomatizable, but no deduction system amenable to proof-theoretic, and hence, computational treatment, has been known. Such a system is presented here, based on previous work on hypersequent calculi for propositional Goedel logics by Avron. It is shown that the system is sound and complete, and allows cut-elimination. A question by Takano regarding the eliminability of the Takeuti-Titani density rule is answered affirmatively. △ Less

Submitted 26 August, 2000; v1 submitted 18 May, 2000; originally announced May 2000.

Comments: v.2: 15 pages. Final version. (v.1: 15 pages. To appear in Computer Science Logic 2000 Proceedings.)

MSC Class: 03B50 (Primary) 03B55; 03F05 (Secondary)

Journal ref: Clote, Peter G., and Helmut Schwichtenberg (eds.), Computer Science Logic. 14th International Workshop, CSL 2000. Fischbachau, Germany, August 21-26, 2000. Proceedings, pp. 187-201. Springer, Berlin, 2000