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

A uniform construction for sequent calculi for finite-valued first-order logics with distribution quantifiers is exhibited. Completeness, cut-elimination and midsequent theorems are established. As an application, an analog of Herbrand’s theorem for the four-valued knowledge-representation logic of Belnap and Ginsberg is presented. It is indicated how this theorem can be used for reasoning about knowledge bases with incomplete and inconsistent information.

A construction principle for natural deduction systems for arbitrary, finitely-many-valued first order logics is exhibited. These systems are systematically obtained from sequent calculi, which in turn can be automatically extracted from the truth tables of the logics under consideration. Soundness and cut-free completeness of these sequent calculi translate into soundness, completeness, and normal-form theorems for natural deduction systems.

First-order Gödel logics are a family of finite- or 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 Gödel logics GV (sets of those formulas which evaluate to 1 in every interpretation into V). It is shown that GV 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 Gödel logics are also characterized. (shrink)

A general class of labeled sequent calculi is investigated, and necessary and sufficient conditions are given for when such a calculus is sound and complete for a finite -valued logic if the labels are interpreted as sets of truth values. Furthermore, it is shown that any finite -valued logic can be given an axiomatization by such a labeled calculus using arbitrary "systems of signs," i.e., of sets of truth values, as labels. The number of labels needed is logarithmic in the (...) number of truth values, and it is shown that this bound is tight. (shrink)

Any intermediate propositional 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. (shrink)

We investigate interpolation properties of many-valued propositional logics related to continuous t-norms. In case of failure of interpolation, we characterize the minimal interpolating extensions of the languages. For finite-valued logics, we count the number of interpolating extensions by Fibonacci sequences.

Entailment in propositional Gödel logics can be defined in a natural way. While all infinite sets of truth values yield the same sets of tautologies, the entailment relations differ. It is shown that there is a rich structure of infinite-valued Gödel logics, only one of which is compact. It is also shown that the compact infinite-valued Gödel logic is the only one which interpolates, and the only one with an r.e. entailment relation.

The aim of this paper is to emphasize the fact that for all finitely-many-valued logics there is a completely systematic relation between sequent calculi and tableau systems. More importantly, we show that for both of these systems there are al- ways two dual proof sytems (not just only two ways to interpret the calculi). This phenomenon may easily escape one’s attention since in the classical (two-valued) case the two systems coincide. (In two-valued logic the assignment of a truth value and (...) the exclusion of the opposite truth value describe the same situation.). (shrink)

A t-tautology is a propositional formula which is a tautology in all fuzzy logics defined by continuous triangular norms. In this paper we show that the problem of recognizing t-tautologies is coNP complete, and thus decidable.

Takeuti and Titani have introduced and investigated a logic they called intuitionistic fuzzy logic. This logic is characterized as the first-order Gödel 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 Gödel 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. (shrink)

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

We introduce Gentzen calculi for intuitionistic logic extended with an existence predicate. Such a logic was first introduced by Dana Scott, who provided a proof system for it in Hilbert style. We prove that the Gentzen calculus has cut elimination in so far that all cuts can be restricted to very simple ones. Applications of this logic to Skolemization, truth value logics and linear frames are also discussed.

Statman and Orevkov independently proved that cut-elimination is of nonelementary complexity. Although their worst-case sequences are mathematically different the syntax of the corresponding cut formulas is of striking similarity. This leads to the main question of this paper: to what extent is it possible to restrict the syntax of formulas and — at the same time—keep their power as cut formulas in a proof? We give a detailed analysis of this problem for negation normal form , prenex normal form and (...) monotone formulas. We show that proof reduction to NNF is quadratic, while PNF behaves differently: although there exists a quadratic transformation into a proof in PNF too, additional cuts are needed; the elimination of these cuts requires nonelementary expense in general. By restricting the logical operators to {,,,}, we obtain the type of monotone formulas. We prove that the elimination of monotone cuts can be of nonelementary complexity . On the other hand, we define a large class of problems where cut-elimination of monotone cuts is only exponential and show that this bound is tight. This implies that the elimination of monotone cuts in equational theories is at most exponential. Particularly, there are no short proofs of Statman's sequence with monotone cuts. (shrink)

In this paper an alternative Skolemization method is introduced that, for a large class of formulas, is sound and complete with respect to intuitionistic logic. This class extends the class of formulas for which standard Skolemization is sound and complete and includes all formulas in which all strong quantifiers are existential. The method makes use of an existence predicate first introduced by Dana Scott.

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 propositional 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.

It is shown that Gqp↑, the quantified propositional Gödel logic based on the truth-value set V↑ = {1 - 1/n : n≥1}∪{1}, is decidable. This result is obtained by reduction to Büchi's theory S1S. An alternative proof based on elimination of quantifiers is also given, which yields both an axiomatization and a characterization of Gqp↑ as the intersection of all finite-valued quantified propositional Gödel logics.

Jan Krajíček posed the following problem: Is there is a generalization result in the theory of real closed fields of the form: If A is provable in length k for all n ϵ ω , then A is provable? It is argued that the answer to this question depends on the particular formulation of the “theory of real closed fields.” Four distinct formulations are investigated with respect to their generalization behavior. It is shown that there is a positive answer to (...) Krajíček's question for 1. the axiom system RCF of Artin-Schreier with Gentzen's LK as underlying logical calculus, 2. RCF with the variant LK B of LK allowing introduction of several quantifiers of the same type in one step, 3. LK B and the first-order schemata corresponding to Dedekind cuts and the supremum principle. A negative answer is given for 4. any system containing the schema of extensionality. (shrink)

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. (shrink)

This volume commemorates the life, work, and foundational views of Kurt Gödel (1906-1978), most famous for his hallmark works on the completeness of first-order logic, the incompleteness of number theory, and the consistency - with the other widely accepted axioms of set theory - of the axiom of choice and of the generalized continuum hypothesis. It explores current research, advances, and ideas for future directions not only in the foundations of mathematics and logic, but also in the fields of computer (...) science, artificial intelligence, physics, cosmology, philosophy, theology, and the history of science. The discussion is supplemented by personal reflections from several scholars who knew Gödel personally, providing some interesting insights into his life. By putting his ideas and life's work into the context of current thinking and perceptions, this book will extend the impact of Gödel's fundamental work in mathematics, logic, philosophy, and other disciplines for future generations of researchers. (shrink)

The first-order temporal logics with □ and ○ of time structures isomorphic to ω (discrete linear time) and trees of ω-segments (linear time with branching gaps) and some of its fragments are compared: the first is not recursively axiomatizable. For the second, a cut-free complete sequent calculus is given, and from this, a resolution system is derived by the method of Maslov.

We construct a faithful interpretation of ukasiewicz's logic in product logic (both propositional and predicate). Using known facts it follows that the product predicate logic is not recursively axiomatizable.We prove a completeness theorem for product logic extended by a unary connective of Baaz [1]. We show that Gödel's logic is a sublogic of this extended product logic.

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. (shrink)

It is shown how the schema of equivalence can be used to obtain short proofs of tautologies A , where the depth of proofs is linear in the number of variables in A .

The problem of algorithmic structuring of proofs in the sequent calculi LK and LKB ( LK where blocks of quantifiers can be introduced in one step) is investigated, where a distinction is made between linear proofs and proofs in tree form. In this framework, structuring coincides with the introduction of cuts into a proof. The algorithmic solvability of this problem can be reduced to the question of k-l-compressibility: "Given a proof of length k , and l ≤ k : Is (...) there is a proof of length ≤ l ?" When restricted to proofs with universal or existential cuts, this problem is shown to be (1) undecidable for linear or tree-like LK-proofs (corresponds to the undecidability of second order unification), (2) undecidable for linear LKB-proofs (corresponds to the undecidability of semi-unification), and (3) decidable for tree-like LKB -proofs (corresponds to a decidable subprob- lem of semi-unification). (shrink)

All first-order Gödel logics G_V with globalization operator based on truth value sets V C [0,1] where 0 and 1 lie in the perfect kernel of V are axiomatized by Ciabattoni’s hypersequent calculus HGIF.

It is shown that the infinite-valued first-order Gödel logic G° based on the set of truth values {1/k: k ε w {0}} U {0} is not r.e. The logic G° is the same as that obtained from the Kripke semantics for first-order intuitionistic logic with constant domains and where the order structure of the model is linear. From this, the unaxiomatizability of Kröger's temporal logic of programs (even of the fragment without the nexttime operator O) and of the authors' temporal (...) logic of linear discrete time with gaps follows. (shrink)

The problem of approximating a propositional calculus is to find many-valued logics which are sound for the calculus (i.e., all theorems of the calculus are tautologies) with as few tautologies as possible. This has potential applications for representing (computationally complex) logics used in AI by (computationally easy) many-valued logics. It is investigated how far this method can be carried using (1) one or (2) an infinite sequence of many-valued logics. It is shown that the optimal candidate matrices for (1) can (...) be computed from the calculus. (shrink)

The length of resolution proofs is investigated, relative to the model-theoretic measure of Herband complexity. A concept of resolution deduction is introduced which is somewhat more general than the classical concepts. It is shown that proof complexity is exponential in terms of Herband complexity and that this bound is tight. The concept of R-deduction is extended to FR-deduction, where, besides resolution, a function introduction rule is allowed. As an example, consider the clause P Q: conclude P) Q, where a, f (...) are new function symbols extending Herbrand's universe. P ()Q from Q) and Skolemization). By modification of a construction of Statman it is shown that FR-deductions may be nonelementarily shorter than R-deductions . Finally it is proved that FR-deduction has weaker effects only if clausal logic is restricted to Horn logic. (shrink)

The generalization properties of algebraically closed fields $ACF_p$ of characteristic $p > 0$ and $ACF_0$ of characteristic 0 are investigated in the sequent calculus with blocks of quantifiers. It is shown that $ACF_p$ admits finite term bases, and $ACF_0$ admits term bases with primality constraints. From these results the analogs of Kreisel's Conjecture for these theories follow: If for some $k$ , $A(1 + \cdots + 1)$ ( $n$ 1's) is provable in $k$ steps, then $(\forall x)A(x)$ is provable.

This paper presents a translation which allows one to describe constructive provability within classical first-order logic.

This paper develops a proof theory for logical forms of proofs in the case of monadic languages. Among the consequences are different kinds of generalization of proofs in various schematic proof systems. The results use suitable relations between logical properties of partial proof data and algebraic properties of corresponding sets of linear diophantine equations.

We study the formal first order system TIND in the standard language of Gentzen's LK . TIND extends LK by the purely logical rule of term-induction, that is a restricted induction principle, deriving numerals instead of arbitrary terms. This rule may be conceived as the logical image of full induction.

Witnessed Gödel logics are based on the interpretation of () by minimum instead of supremum . Witnessed Gödel logics appear for many practical purposes more suited than usual Gödel logics as the occurrence of proper infima/suprema is practically irrelevant. In this note we characterize witnessed Gödel logics with absoluteness operator w.r.t. witnessed Gödel logics using a uniform translation.

We construct peculiar Hilbert spaces from counterexamples to the axiom of choice. We identify the intrinsically effective Hamiltonians with those observables of quantum theory which may coexist with such spaces. Here a self adjoint operator is intrinsically effective if and only if the Schrödinger equation of its generated semigroup is soluble by means of eigenfunction series expansions.

We consider an extension of Gödel logic by a unary operator that enables the addition of non-negative reals to truth-values. Although its propositional fragment has a simple proof system, first-order validity is Π2-hard. We explain the close connection to Scarpellini’s result on Π2-hardness of Łukasiewicz’s logic.