In this paper, we show the equivalence between the provability of a proof system of basic hybrid logic and that of translated formulas of the classical predicate logic with equality and explicit substitution by a purely proof–theoretic method. Then we show the equivalence of two groups of proof systems of hybrid logic: the group of labelled deduction systems and the group of modal logic-based systems.

It is well known that the modal logic S5 can be embedded in the classical predicate logic by interpreting the modal operator in terms of a quantifier. Wajsberg [10] proved this fact in a syntactic way. Mints [7] extended this result to the quantified version of S5; using a purely proof-theoretic method he showed that the quantified S5 corresponds to the classical predicate logic with one-sorted variable. In this paper we extend Mints' result to the basic modal logic S4; we (...) investigate the correspondence between the quantified versions of S4 (with and without the Barcan formula) and the classical predicate logic (with one-sorted variable). We present a purely proof-theoretic proof-transformation method, reducing an LK-proof of an interpreted formula to a modal proof. (shrink)

In a classical 1976 paper, Solovay proved the arithmetical completeness of the modal logic GL; provability of a formula in GL coincides with provability of its arithmetical interpretations of it in Peano Arithmetic. In that paper, he also provided an axiomatic system GLS and proved arithmetical completeness for GLS; provability of a formula in GLS coincides with truth of its arithmetical interpretations in the standard model of arithmetic. Proof theory for GL has been studied intensively up to the present day. (...) However, it might sound somewhat strange that no proof theory for GLS was ever developed nor even suggested thus far, except for the axiomatic system offered by Solovay. In this paper, we develop a proof theory for GLS based on the sequent calculus method. We provide a sequent calculus for GLS and prove the cut-elimination and some standard consequences of it: the interpolation and definability theorems. As another consequence of cut-elimination, we also prove the equivalence of GL and GLS with respect to a special form of formulas which we call Gödel sentences, using a purely proof-theoretical method. (shrink)

LK is a natural modification of Gentzen sequent calculus for propositional logic with connectives ¬ and $\bigwedge, \bigvee$. Then for every d ≥ 0 and n ≥ 2, there is a set Td n of depth d sequents of total size O which are refutable in LK by depth d + 1 proof of size exp) but such that every depth d refutation must have the size at least exp). The sets Td n express a weaker form of the pigeonhole (...) principle. (shrink)

A proof of the (propositional) Craig interpolation theorem for cut-free sequent calculus yields that a sequent with a cut-free proof (or with a proof with cut-formulas of restricted form; in particular, with only analytic cuts) with k inferences has an interpolant whose circuit-size is at most k. We give a new proof of the interpolation theorem based on a communication complexity approach which allows a similar estimate for a larger class of proofs. We derive from it several corollaries: (1) Feasible (...) interpolation theorems for the following proof systems: (a) resolution (b) a subsystem of LK corresponding to the bounded arithmetic theory S 2 2 (α) (c) linear equational calculus (d) cutting planes. (2) New proofs of the exponential lower bounds (for new formulas) (a) for resolution ([15]) (b) for the cutting planes proof system with coefficients written in unary ([4]). (3) An alternative proof of the independence result of [43] concerning the provability of circuit-size lower bounds in the bounded arithmetic theory S 2 2 (α). In the other direction we show that a depth 2 subsystem of LK does not admit feasible monotone interpolation theorem (the so called Lyndon theorem), and that a feasible monotone interpolation theorem for the depth 1 subsystem of LK would yield new exponential lower bounds for resolution proofs of the weak pigeonhole principle. (shrink)

A proof of the (propositional) Craig interpolation theorem for cut-free sequent calculus yields that a sequent with a cut-free proof (or with a proof with cut-formulas of restricted form; in particular, with only analytic cuts) withkinferences has an interpolant whose circuit-size is at mostk. We give a new proof of the interpolation theorem based on a communication complexity approach which allows a similar estimate for a larger class of proofs. We derive from it several corollaries:(1)Feasible interpolation theorems for the following (...) proof systems:(a)resolution(b)a subsystem ofLKcorresponding to the bounded arithmetic theory(α)(c)linear equational calculus(d)cutting planes.(2)New proofs of the exponential lower bounds (for new formulas)(a)for resolution ([15])(b)for the cutting planes proof system with coefficients written in unary ([4]).(3)An alternative proof of the independence result of [43] concerning the provability of circuit-size lower bounds in the bounded arithmetic theory(α).In the other direction we show that a depth 2 subsystem ofLKdoes not admit feasible monotone interpolation theorem (the so called Lyndon theorem), and that a feasible monotone interpolation theorem for the depth 1 subsystem ofLKwould yield new exponential lower bounds for resolution proofs of the weak pigeonhole principle. (shrink)

We define a first-order extension LK(CP) of the cutting planes proof system CP as the first-order sequent calculus LK whose atomic formulas are CP-inequalities ∑ i a i · x i ≥ b (x i 's variables, a i 's and b constants). We prove an interpolation theorem for LK(CP) yielding as a corollary a conditional lower bound for LK(CP)-proofs. For a subsystem R(CP) of LK(CP), essentially resolution working with clauses formed by CP- inequalities, we prove a monotone interpolation theorem (...) obtaining thus an unconditional lower bound (depending on the maximum size of coefficients in proofs and on the maximum number of CP-inequalities in clauses). We also give an interpolation theorem for polynomial calculus working with sparse polynomials. The proof relies on a universal interpolation theorem for semantic derivations [16, Theorem 5.1]. LK(CP) can be viewed as a two-sorted first-order theory of Z considered itself as a discretely ordered Z-module. One sort of variables are module elements, another sort are scalars. The quantification is allowed only over the former sort. We shall give a construction of a theory LK(M) for any discretely ordered module M (e.g., LK(Z) extends LK(CP)). The interpolation theorem generalizes to these theories obtained from discretely ordered Z-modules. We shall also discuss a connection to quantifier elimination for such theories. We formulate a communication complexity problem whose (suitable) solution would allow to improve the monotone interpolation theorem and the lower bound for R(CP). (shrink)

ABSTRACTIn this paper, we present a generalisation of proof simulation procedures for Frege systems by Bonet and Buss to some logics for which the deduction theorem does not hold. In particular, we study the case of finite-valued Łukasiewicz logics. To this end, we provide proof systems and which augment Avron's Frege system HŁuk with nested and general versions of the disjunction elimination rule, respectively. For these systems, we provide upper bounds on speed-ups w.r.t. both the number of steps in proofs (...) and the length of proofs. We also consider Tamminga's natural deduction and Avron's hypersequent calculus GŁuk for 3-valued Łukasiewicz logic and generalise our results considering the disjunction elimination rule to all finite-valued Łukasiewicz logics. (shrink)

We present a sequent calculus with the Henkin constants in the place of the free variables. By disposing of the eigenvariable condition, we obtained a proof system with a strong locality property—the validity of each inference step depends only on its active formulas, not its context. Our major outcomes are: the cut elimination via a non-Gentzen-style algorithm without resorting to regularization and the elimination of Skolem functions with linear increase in the proof length for a subclass of derivations with cuts.

The logic CD is an intermediate logic which exactly corresponds to the Kripke models with constant domains. It is known that the logic CD has a Gentzen-type formulation called LD and rules are replaced by the corresponding intuitionistic rules) and that the cut-elimination theorem does not hold for LD. In this paper we present a modification of LD and prove the cut-elimination theorem for it. Moreover we prove a “weak” version of cut-elimination theorem for LD, saying that all “cuts” except (...) some special forms can be eliminated from a proof in LD. From these cut-elimination theorems we obtain some corollaries on syntactical properties of CD: fragments collapsing into intuitionistic logic. Harrop disjunction and existence properties, and a fact on the number of logical symbols in the axiom of CD. (shrink)

Two new infinitary modal logics are simply obtained from a Gentzen-type sequent calculus for infinitary logic by adding a next-time operator, and a program operator, respectively. It is shown that an any-time operator and a program-iteration operator can respectively be expressed using infinitary conjunction in these logics. The cut-elimination and completeness theorems for these logics are proved using some theorems for embedding these logics into (classical) infinitary logic.

In this study, we introduce Gentzen-type sequent calculi BDm and BDi for a modal extension and an intuitionistic modification, respectively, of De and Omori’s extended Belnap–Dunn logic BD+ with classical negation. We prove theorems for syntactically and semantically embedding BDm and BDi into Gentzen-type sequent calculi S4 and LJ for normal modal logic and intuitionistic logic, respectively. The cut-elimination, decidability, and completeness theorems for BDm and BDi are obtained using these embedding theorems. Moreover, we prove the Glivenko theorem for embedding (...) BD+ into BDi and the McKinsey–Tarski theorem for embedding BDi into BDm. (shrink)

Two intuitionistic paradefinite logics N4C and N4C+ are introduced as Gentzen-type sequent calculi. These logics are regarded as a combination of Nelson’s paraconsistent four-valued logic N4 and Wansing’s basic constructive connexive logic C. The proposed logics are also regarded as intuitionistic variants of Arieli, Avron, and Zamansky’s ideal paraconistent four-valued logic 4CC. The logic N4C has no quasi-explosion axiom that represents a relationship between conflation and paraconsistent negation, but the logic N4C+ has this axiom. The Kripke-completeness and cut-elimination theorems for (...) N4C and N4C+ are proved. (shrink)

In this paper, bi-intuitionistic multilattice logic, which is a combination of multilattice logic and the bi-intuitionistic logic also known as Heyting–Brouwer logic, is introduced as a Gentzen-type sequent calculus. A Kripke semantics is developed for this logic, and the completeness theorem with respect to this semantics is proved via theorems for embedding this logic into bi-intuitionistic logic. The logic proposed is an extension of first-degree entailment logic and can be regarded as a bi-intuitionistic variant of the original classical multilattice logic (...) determined by the algebraic structure of multilattices. Similar completeness and embedding results are also shown for another logic called bi-intuitionistic connexive multilattice logic, obtained by replacing the connectives of intuitionistic implication and co-implication with their connexive variants. (shrink)

In this study, falsification-aware semantics and sequent calculi for first-order classical logic are introduced and investigated. These semantics and sequent calculi are constructed based on a falsification-aware setting for first-order Nelson constructive three-valued logic. In fact, these semantics and sequent calculi are regarded as those for a classical variant of N3. The completeness and cut-elimination theorems for the proposed semantics and sequent calculi are proved using Schütte’s method. Similar results for the propositional case are also obtained.

First-order intuitionistic and classical Nelson–Wansing and Arieli–Avron–Zamansky logics, which are regarded as paradefinite and connexive logics, are investigated based on Gentzen-style sequent calculi. The cut-elimination and completeness theorems for these logics are proved uniformly via theorems for embedding these logics into first-order intuitionistic and classical logics. The modified Craig interpolation theorems for these logics are also proved via the same embedding theorems. Furthermore, a theorem for embedding first-order classical Arieli–Avron–Zamansky logic into first-order intuitionistic Arieli–Avron–Zamansky logic is proved using a modified (...) Gödel–Gentzen negative translation. The failure of a theorem for embedding first-order classical Nelson–Wansing logic into first-order intuitionistic Nelson–Wansing logic is also shown. (shrink)

In this study, we prove the completeness and cut-elimination theorems for a first-order extension F4CC of Arieli, Avron, and Zamansky’s ideal paraconsistent four-valued logic known as 4CC. These theorems are proved using Schütte’s method, which can simultaneously prove completeness and cut-elimination.

In this paper we will state and prove some comparative theorems concerning PRA and IΣ1. We shall provide a characterization of IΣ1 in terms of PRA and iterations of a class of functions. In particular, we prove that for this class of functions the difference between IΣ1 and PRA is exactly that, where PRA is closed under iterations of these functions, IΣ1 is moreover provably closed under iteration. We will formulate a sufficient condition for a model of PRA to be (...) a model of IΣ1. This condition is used to give a model-theoretic proof of Parsons’ theorem, that is, IΣ1 is Π2-conservative over PRA. We shall also give a purely syntactical proof of Parsons’ theorem. Finally, we show that IΣ1 proves the consistency of PRA on a definable IΣ1-cut. This implies that proofs in IΣ1 can have non-elementary speed up over proofs in PRA. (shrink)

This paper deals with: (i) the theory ID # 1 which results from $\widehat{\mathrm{ID}}_1$ by restricting induction on the natural numbers to formulas which are positive in the fixed point constants, (ii) the theory BON(μ) plus various forms of positive induction, and (iii) a subtheory of Peano arithmetic with ordinals in which induction on the natural numbers is restricted to formulas which are Σ in the ordinals. We show that these systems have proof-theoretic strength φω 0.

We study and some of its most important extensions primarily from a proof-theoretic perspective, determine their consistency strengths by exhibiting equivalent systems in the realm of traditional set theory and introduce a new and interesting extension of which is conservative over.

This paper presents several proof-theoretic results concerning weak fixed point theories over second order number theory with arithmetic comprehension and full or restricted induction on the natural numbers. It is also shown that there are natural second order theories which are proof-theoretically equivalent but have different proof-theoretic ordinals.

Hypersequent calculus, developed by A. Avron, is one of the most interesting proof systems suitable for nonclassical logics. Although HC has rather simple form, it increases significantly the expressive power of standard sequent calculi. In particular, HC proved to be very useful in the field of proof theory of various nonclassical logics. It may seem surprising that it was not applied to temporal logics so far. In what follows, we discuss different approaches to formalization of logics of linear frames and (...) provide a cut-free HC formalization ofKt4.3, the minimal temporal logic of linear frames, and some of its extensions. The novelty of our approach is that hypersequents are defined not as finite sets but as finite lists of ordinary sequents. Such a solution allows both linearity of time flow, and symmetry of past and future, to be incorporated by means of six temporal rules. Extensions of the basic calculus with simple structural rules cover logics of serial and dense frames. Completeness is proved by Schütte/Hintikka-style argument using models built from saturated hypersequents. (shrink)

The paper presents a uniform proof-theoretic treatment of several kinds of free logic, including the logics of existence and definedness applied in constructive mathematics and computer science, and called here quasi-free logics. All free and quasi-free logics considered are formalised in the framework of sequent calculus, the latter for the first time. It is shown that in all cases remarkable simplifications of the starting systems are possible due to the special rule dealing with identity and existence predicate. Cut elimination is (...) proved in a constructive way for sequent calculi adequate for all logics under consideration. (shrink)

We investigate the logical structure of intuitionistic Kripke-Platek set theory , and show that the first-order logic of is intuitionistic first-order logic IQC.

This paper deals with some structural properties of the sequent calculus and describes strong symmetries between cut-free derivations and derivations, which do not make use of identity axioms. Both of them are discussed from a semantic and syntactic point of view. Identity axioms and cuts are closely related to the treatment of negation in the sequent calculus, so the results of this article explain some nice symmetries of negation.

Nonclassical theories of truth have in common that they reject principles of classical logic to accommodate an unrestricted truth predicate. However, different nonclassical strategies give up different classical principles. The paper discusses one criterion we might use in theory choice when considering nonclassical rivals: the maxim of minimal mutilation.

We first note that Gentzen's proof-reduction for his consistency proof of PA can be directly interpreted as moves of Kirby-Paris' Hydra Game, which implies a direct independence proof of the game . Buchholz's Hydra Game for labeled hydras is known to be much stronger than PA. However, we show that the one-dimensional version of Buchholz's Game can be exactly identified to Kirby-Paris' Game , by a simple and natural interpretation . Jervell proposed another type of a combinatorial game, by abstracting (...) Gentzen's proof-reductions and showed that his game is independent of PA. We show that this Jervell's game is actually much stronger than PA, by showing that the critical ordinal of Jervell's game is φω = ϵ0) in the Veblen hierarchy of ordinals. (shrink)

The general notions of object- and metalanguage are discussed and as a special case of this relation an arbitrary first order language with an infinite model is expanded by a predicate symbol T0 which is interpreted as truth predicate for . Then the expanded language is again augmented by a new truth predicate T1 for the whole language plus T0. This process is iterated into the transfinite to obtain the Tarskian hierarchy of languages. It is shown that there are natural (...) points for stopping this process. The sets which become definable in suitable hierarchies are investigated, so that the relevance of the Tarskian hierarchy to some subjects of philosophy of mathematics are clarified. (shrink)

The uniform reflection principle for the theory of uniform T-sentences is added to PA. The resulting system is justified on the basis of a disquotationalist theory of truth where the provability predicate is conceived as a special kind of analyticity. The system is equivalent to the system ACA of arithmetical comprehension. If the truth predicate is also allowed to occur in the sentences that are inserted in the T-sentences, yet not in the scope of negation, the system with the reflection (...) schema for these T-sentences assumes the strength of the Kripke-Feferman theory KF, and thus of ramified analysis up to go. (shrink)

Cantor argued that absolute infinity is beyond mathematical comprehension. His arguments imply that the domain of mathematics cannot be grasped by mathematical means. We argue that this inability constitutes a foundational problem. For Cantor, however, the domain of mathematics does not belong to mathematics, but to theology. We thus discuss the theological significance of Cantor’s treatment of absolute infinity and show that it can be interpreted in terms of negative theology. Proceeding from this interpretation, we refer to the recent debate (...) on absolute generality and argue that the method of diagonalization constitutes a modern version of the vianegativa. On our reading, negative theology can evoke an attitude of humility with respect to the boundedness of the human condition. Along these lines, we think that the foundational problem of mathematics concerning its domain can be addressed through a methodological attitude of humility. (shrink)

ABSTRACT: It is argued that the equivalence, which is usually postulated to hold between infinite descent and transfinite induction in the foundations of arithmetic uses the law of excluded middle through the use of a double negation on the infinite set of natural numbers and therefore cannot be admitted in intuitionistic logic and mathematics, and a fortiori in more radical constructivist foundational schemes. Moreover it is shown that the infinite descent used in Dedekind-Peano arithmetic does not correspond to the infinite (...) descent of classical Fermatian arithmetic or number theory. However, from the point of view of classical logic, the principles of complete induction and transfinite induction, the least number principle and infinite descent are all equivalent. We find here a focal point for a foundational critique that aims for a a clarification of philosophical options in the foundations of logic and mathematics. (shrink)

The present paper suggests relative truth definability as a tool for comparing conceptual aspects of axiomatic theories of truth and gives an overview of recent developments of axiomatic theories of truth in the light of it. We also show several new proof-theoretic results via relative truth definability including a complete answer to the conjecture raised by Feferman in [13].

Approximately speaking, an urn model for first-order logic is a model where the domain of quantification changes depending on the values of variables which have been bound by quantifiers previously. In this paper we introduce a model-changing semantics for urn-models, and then give a sequent calculus for urn logic by introducing formulas which can be read as saying that “after the individuals a1,..., an have been drawn, A is the case”.

This paper concerns the relationship between transitivity of entailment, omega-inconsistency and nonstandard models of arithmetic. First, it provides a cut-free sequent calculus for non-transitive logic of truth STT based on Robinson Arithmetic and shows that this logic is omega-inconsistent. It then identifies the conditions in McGee for an omega-inconsistent logic as quantified standard deontic logic, presents a cut-free labelled sequent calculus for quantified standard deontic logic based on Robinson Arithmetic where the deontic modality is treated as a predicate, proves omega-inconsistency (...) and shows thus, pace Cobreros et al., that the result in McGee does not rely on transitivity. Finally, it also explains why the omega-inconsistent logics of truth in question do not require nonstandard models of arithmetic. (shrink)

This paper presents a sound and complete five-sided sequent calculus for first-order weak Kleene valuations which permits not only elegant representations of four logics definable on first-order weak Kleene valuations, but also admissibility of five cut rules by proof analysis.

In this paper we discuss sequent calculi for the propositional fragment of the logic of HYPE. The logic of HYPE was recently suggested by Leitgeb as a logic for hyperintensional contexts. On the one hand we introduce a simple \-system employing rules of contraposition. On the other hand we present a \-system with an admissible rule of contraposition. Both systems are equivalent as well as sound and complete proof-system of HYPE. In order to provide a cut-elimination procedure, we expand the (...) calculus by connections as introduced in Kashima and Shimura. (shrink)

Questions concerning the proof-theoretic strength of classical versus nonclassical theories of truth have received some attention recently. A particularly convenient case study concerns classical and nonclassical axiomatizations of fixed-point semantics. It is known that nonclassical axiomatizations in four- or three-valued logics are substantially weaker than their classical counterparts. In this paper we consider the addition of a suitable conditional to First-Degree Entailment—a logic recently studied by Hannes Leitgeb under the label HYPE. We show in particular that, by formulating the theory (...) PKF over HYPE, one obtains a theory that is sound with respect to fixed-point models, while being proof-theoretically on a par with its classical counterpart KF. Moreover, we establish that also its schematic extension—in the sense of Feferman—is as strong as the schematic extension of KF, thus matching the strength of predicative analysis. (shrink)

In this paper we will investigate different axiomatic theories of truth that are minimal in some sense. One criterion for minimality will be conservativity over Peano Arithmetic. We will then give a more fine-grained characterization by investigating some interpretability relations. We will show that disquotational theories of truth, as well as compositional theories of truth with restricted induction are relatively interpretable in Peano Arithmetic. Furthermore, we will give an example of a theory of truth that is a conservative extension of (...) Peano Arithmetic but not interpretable in it. We will then use stricter versions of interpretations to compare weak theories of truth to subsystems of second-order arithmetic. (shrink)

Leo Harrington showed that the second-order theory of arithmetic WKL 0 is ${\Pi^1_1}$ -conservative over the theory RCA 0. Harrington’s proof is model-theoretic, making use of a forcing argument. A purely proof-theoretic proof, avoiding forcing, has been eluding the efforts of researchers. In this short paper, we present a proof of Harrington’s result using a cut-elimination argument.

A constructivisation of the cut-elimination proof for sequent calculi for classical, intuitionistic and minimal infinitary logics with geometric rules—given in earlier work by the second author—is presented. This is achieved through a procedure where the non-constructive transfinite induction on the commutative sum of ordinals is replaced by two instances of Brouwer’s Bar Induction. The proof of admissibility of the structural rules is made ordinal-free by introducing a new well-founded relation based on a notion of embeddability of derivations. Additionally, conservativity for (...) classical over intuitionistic/minimal logic for the seven (finitary) Glivenko sequent classes is here shown to hold also for the corresponding infinitary classes. (shrink)