In this paper we present the proof that there is no elementary translation from cut- free derivations in the sequent calculus variant of the epsilon calculus to LK-proofs with bounded cut-complexity. This is a partial answer to a question by Toshiyasu Arai. Fur- thermore, we show that the intuitionistic format of the sequent calculus variant of the epsilon calculus is not sound for intuitionistic logic, due to the presence of all classical quantifier-shift rules.

Abstract This volume is one of two special issues collecting articles by invited speakers of the conference ‘Celebrating 90 Years of Gödel’s Incompleteness Theorems’ held in Nürtingen (Germany) in July 2021. The conference was organized by the Carl Friedrich von Weizsäcker Center at the University of Tübingen with support by the ERC-funded project Gödel Enigma: Rediscovering Kurt Gödel through his unpublished works at the University of Helsinki and by the Kurt Gödel Society in Vienna.

This paper focuses on globally sound but possibly locally unsound analytic sequent calculi for quantifier macros defined by sequences of quantifiers. It is demonstrated that no locally sound analytic representation based on the usual eigenvariable condition exists. In consequence, representations by globally sound but possibly locally unsound analytic sequent calculi are used. Cut-elimination is shown by translating proofs into LK and retranslating cut-free proofs into the desired format. Finally, criteria are given for sequents to be proved without reference to the extended eigenvariable conditions.

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 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 $\tau $ -formulas and using the translation of quantifiers into $\varepsilon $ - and $\tau $ -terms to intermediate logics. It is shown that conservativity over the propositional base logic also holds for such intermediate ${\varepsilon \tau }$ -calculi. The “extended” first $\varepsilon $ -theorem holds if the base logic is finite-valued Gödel–Dummett logic, and 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.

Abstract This paper presents a methodology to construct globally sound but possibly locally unsound analytic calculi for partial theories of Henkin quantifiers. It is demonstrated that usual locally sound analytic calculi do not exist for any reasonable fragment of the full theory of Henkin quantifiers. This is due to the combination of strong and weak quantifier inferences in one quantifier rule.

Abstract We present a new method of computing Herbrand disjunctions. The up-to-date most direct approach to calculate Herbrand disjunctions is based on Hilbert’s epsilon formalism (which is in fact also the oldest framework for proof theory). The algorithm to calculate Herbrand disjunctions is an integral part of the proof of the extended first epsilon theorem. This paper introduces a more abstract form of epsilon proofs, the function variable proofs. This leads to a computational improved version of the extended first epsilon theorem, which allows a nonelementary speed up of the computation of Herbrand disjunctions. As an application, sequent calculus proofs are translated into function variable proofs and a variant of the axiom of global choice is shown to be removable from proofs in Neumann–Bernays–Gödel set theory.

Abstract We give examples of calculi that extend Gentzen’s sequent calculusLKby unsound quantifier inferences in such a way that (i) derivations lead only to true sequents, and (ii) proofs therein are nonelementarily shorter thanLK-proofs.

First-order interpolation properties are notoriously hard to determine, even for logics where propositional interpolation is more or less obvious. One of the most prominent examples is first-order G ̈odel logic. Lyndon interpolation is a strengthening of the interpolation property in the sense that propositional variables or predicate symbols are only allowed to occur positively (negatively) in the interpolant if they occur positively (negatively) on both sides of the implication. Note that Lyndon interpolation is difficult to establish for first-order logics as most proof-theoretic methods fail. In this paper we provide general derivability conditions for a first-order logic to admit Lyndon interpolation for the prenex ⊃ prenex fragment and apply the arguments to the prenex ⊃ prenex fragment of first-order Go ̈del logic.

In this paper we show that a very basic fragment of FO-LTL, the monadic fully boxed fragment (all connectives and quantifiers are guarded by P) is not recursively enumerable wrt validity and 1-satisfiability if three predicates are present. This result is obtained by reduction of the fully boxed fragment of FO-LTL to the Gödel logic G↓, the infinitely valued Gödel logic with truth values in [0,1] such that all but 0 are isolated. The result on 1-satisfiability is in no way symmetric to the result on validity as in classical logic: this is demonstrated by the analysis of G↑, the related infinitely-valued Gödel logic with truth values in [0, 1] such that all but 1 are isolated. Validity of the monadic fragment with at least two predicates is not recursively enumerable, 1-satisfiability of the monadic fragment is decidable.

This volume contains selected papers from the workshop ‘Concepts and Meaning’ held on 2–5 May 2012 at the Vienna University of Technology in honour of the 60th birthday of Alexander Leitsch. Alexander Leitsch made substantial contributions to a variety of different research areas including automated deduction, computability theory, proof theory and formal mathematics. The broad scope of his research interests is reflected in the contents of this special issue that features the following papers (in alphabetic order): ... A common thread that runs through Alexander Leitsch' scientific work is his mastery of syntactic precision rooted in the conviction that the syntactic form not only captures but even determines the semantic meaning of concepts, hence also the title of this special issue. In addition to his scientific activities he is also an inspiring colleague and a dedicated and enthusiastic teacher as witnessed by generations of his students who are now successful in academia as well as in industry, some of which are represented in this volume.

Gödel logics are an important class of intermediate logics with connections to many areas and applications of logic such as temporal logic, Heyting algebras, fuzzy logic, and parallel processing. In this paper, we present ten open problems in the proof and model theories of Gödel Logic. The problems can be seen to be ordered both thematically and by generality. Some of the problems have been open for more than thirty years. The second author discussed many of them with Franco Montagna, to whose memory this paper is dedicated.

We introduce a first sequent-style calculus for witnessed Gödel logic. Our calculus makes use of the cut rule. We show that this is inescapable by establishing a general result on the non-existence of suitable analytic calculi for a large class of first-order logics. These include witnessed Gödel logic, (fragments of) Łukasiewicz logic and intuitionistic logic extended with the quantifiers of classical logic.

The size of shortest cut-free proofs of first-order formulas in intuitionistic sequent calculus is known to be non-elementary in the worst case in terms of the size of given sequent proofs with cuts of the same formulas. In contrast to that fact, we provide an elementary bound for the size of cut-free proofs for disjunction-free intuitionistic logic for the case where the cut-formulas of the original proof are prenex. Moreover, we establish non-elementary lower bounds for classical disjunction-free proofs with prenex cut-formulas and intuitionistic disjunction-free proofs with non-prenex cut-formulas.

We show an effective cut-free variant of Glivenko's theorem extended to formulas with weak quantifiers: "There is an elementary function f such that if φ is a cut-free LK proof of ⊢ A with symbol complexity ≤ c, then there exists a cut-free LJ proof of ⊢ ⊯ ⊯ A with symbol complexity ≤ f(c)". This follows from the more general result: "There is an elementary function f such that if φ is a cut-free LK proof of A ⊢ with symbol complexity ≤ c, then there exists a cut-free LJ proof of A ⊢ with symbol complexity ≤ f(c)". The result is proved using a suitable variant of cut-elimination by resolution (CERES) and subsumption.

We consider the extension of Godel logic by a unary operator interpreted by functions on the unit interval with certain monotonicity properties. We prove that validity of propositional formulas is decidable by giving a sound and complete proof system with finitely many axioms. We show also how to transfer the deduction theorem, the lifting lemma and the agreement of entailment and 1-entailment from Godel logic to the propositional fragment of our extension. Finally, we prove an enumerability result for a ring-normal prenex fragment.

Abstract We consider the following problem: Given a proof of the Skolemization of a formulaF, what is the length of the shortest proof ofF? For the restriction of this question to cut-free proofs we prove corresponding exponential upper and lower bounds.

Abstract We study cut-elimination in first-order classical logic. We construct a sequence of polynomial-length proofs having a non-elementary number of different cut-free normal forms. These normal forms are different in a strong sense: they not only represent different Herbrand-disjunctions but also differ in their prepositional structure. This result illustrates that the constructive content of a proof in classical logic is not uniquely determined but rather depends on the chosen method for extracting it.

In Baaz and Iemhoff (2006, Annals of Pure and Applied Logic, 142, 269–295), an alternative skolemization method called eskolemization was introduced that is sound and complete for existence logic with respect to existential quantifiers. Existence logic is a conservative extension of intuitionistic logic by an existence predicate. Therefore, eskolemization provides a skolemization method for intuitionistic logic as well. All proofs in Baaz and Iemhoff (2006, Annals of Pure and Applied Logic, 142, 269–295) were semantical. In this article, a proof-theoretic proof of the completeness of eskolemization with respect to existential quantifiers is presented.

An approximate Herbrand theorem is established for first-order infinite-valued Łukasiewicz Logic and used to obtain a proof-theoretic proof of Skolemization. These results are then used to define proof systems in the framework of hypersequents. In particular, a calculus lacking cut elimination is defined for the first-order logic characterized by linearly ordered MV-algebras, a cut-free calculus with an infinitary rule for the full first-order Łukasiewicz Logic, and a cut-free calculus with finitary rules for its one-variable fragment.

Journal Article Fuzzy Logic Corner Get access Matthias Baaz, Matthias Baaz Search for other works by this author on: Oxford Academic Google Scholar George Metcalfe George Metcalfe Search for other works by this author on: Oxford Academic Google Scholar Journal of Logic and Computation, Volume 19, Issue 2, April 2009, Page 343, https://doi.org/10.1093/logcom/exn053 Published: 18 August 2008

Abstract In this paper a method for the replacement, in formulas, of strong quantifiers by functions is introduced that can be considered as an alternative to Skolemization in the setting of constructive theories. A constructive extension of intuitionistic predicate logic that captures the notions of preorder and existence is introduced and the method, orderization, is shown to be sound and complete with respect to this logic. This implies an analogue of Herbrand's theorem for intuitionistic logic. The orderization method is applied to the constructive theories of equality and groups.

The minimal extension of intuitionistic propositional language is characterized, where propositional quantifiers are eliminable w.r.t. Kripke frames of type ω.

Journal Article Editorial Get access S. I. Adian, S. I. Adian Search for other works by this author on: Oxford Academic Google Scholar M. Baaz, M. Baaz Search for other works by this author on: Oxford Academic Google Scholar L. D. Beklemishev L. D. Beklemishev Search for other works by this author on: Oxford Academic Google Scholar Journal of Logic and Computation, Volume 15, Issue 4, August 2005, Page 409, https://doi.org/10.1093/logcom/exi036 Published: 01 August 2005

Hypersequent calculi arise by generalizing standard sequent calculi to refer to whole contexts of sequents instead of single sequents. We present a number of results using hypersequents to obtain a Gentzen-style characterization for the family of Gödel logics. We first describe analytic calculi for propositional finite and infinite-valued Gödel logics. We then show that the framework of hypersequents allows one to move straightforwardly from the propositional level to first-order as well as propositional quantification. A certain type of modality, enhancing the expressive power of Gödel logic, is also considered.

We investigate the effects of different types of translations of first-order formulas to clausal form on minimal proof length. We show that there is a sequence of unsatisfiable formulassuch that the length of all refutations of non-structural clause forms of F/sub n/ is non-elementary (in the size of F/sub n/), but there are refutations of structural clause forms of F/sub n/ that are of elementary (at most triple exponential) length.>

The impact of Skolemization on the complexity of proofs in the sequent calculus is investigated. It is shown that prefix Skolemization may result in a nonelementary increase of Herbrand complexity (i. e. the minimal number of constituents in a Herbrand disjunction) versus structural Skolemization. Moreover it is shown that restricting the range of quantifiers never increases Herbrand complexity. The results provide a general mathematical justification for minimizing the range of quantifiers (by means of shifting) before Skolemization of formulas.

Although problem reduction is a very important tool in mathematical practice, relatively little attention has been paid to problem reduction in automated theorem proving. A systematical treatment of different problem reduction methods can be found in [BI71] and [Lo78]. (In [BI71] we find unary and binary reduction rules. In the unary case we reduce a problem E to a problem E', where E is provable (refutable) if E' is; for binary reduction we have to produce problems E1, E2 out of E such that E is provable (refutable) if both E1, E2 are provable (refutable).) In finding stronger reduction strategies, one has to give up completeness of the split of E into E1, E2; that means, we only require that the provability of E1 and E2 implies that of E. The authors therefore propose problem reduction based on a splitting rule of the form C → C', where C ∼ C1 n C2, C' ∼ C1 n C'2, C'2 ∼ C2 {× ← ƒ(y1,…yn)}, {x,y1,…yn} is the set of variables both in C1 and C2 and ƒ is a new function symbol up to this point not occurring in any clause. Note that the Herbrand universe is extended by ƒ and consequently C' is not derivable from C by usual resolution methods! As (∀y1) … (∀yn(∀x) (C1 n C2) → (∀y1) … (∀yn ((∀x) C1 n (∃x) (C2) is valid in first order predicate logic and C1 n C'2 is the Skolemization of the implied formula, splitting of this kind is correct. For reasons of efficiency (reduction of search space and restriction of compound terms) the authors restrict the application of the rule above to sequences of applications (called Q-reduction) completely separating the variables in C1 and C2. Finally the authors construct a sequence of clause sets Cn having resolution proofs exponential in n only, but application of the new reduction rule reduces the problem to two problems linear in n. Thus it turns out that the introduction of (elementary) quantificational rules into clause logic can strongly influence the structure of proofs and the performance of theorem provers.