We show in this paper that all fragments of intuitionistic propostional logic based on a subset of the connectives $\wedge, \vee, \rightarrow, \neg$ satisfy interpolation. Fragments containing $\leftrightarrow$ or $\neg\neg$ are briefly considered.

Proof-theoretic reflection principles are schemas which attempt to express the soundness of arithmetical theories within their own language, e.g., ${\mathtt{{Prov}_{\mathsf {PA}} \rightarrow \varphi }}$ can be understood to assert that any statement provable in Peano arithmetic is true. It has been repeatedly suggested that justification for such principles follows directly from acceptance of an arithmetical theory $\mathsf {T}$ or indirectly in virtue of their derivability in certain truth-theoretic extensions thereof. This paper challenges this consensus by exploring relationships between reflection principles (...) and principles of mathematical and transfinite induction as well as the status of the latter with respect to various foundational characterizations of number theory. (shrink)

This article will study a class of deduction systems that allow for a limited use of the modus ponens method of deduction. We will show that it is possible to devise axiom systems α that can recognize their consistency under a deduction system D provided that: (1) α treats multiplication as a 3-way relation (rather than as a total function), and that (2) D does not allow for the use of a modus ponens methodology above essentially the levels of Π1 (...) and Σ1 formulae. Part of what will make this boundary-case exception to the Second Incompleteness Theorem interesting is that we will also characterize generalizations of the Second Incompleteness Theorem that take force when we only slightly weaken the assumptions of our boundary-case exceptions in any of several further directions. (shrink)

Mathematics textbooks teach logical reasoning by example, a practice started by Euclid; while logic textbooks treat logic as a subject in its own right without practical application to mathematics. Stuck in the middle are students seeking mathematical proficiency and educators seeking to provide it. To assist them, the article explains in practical detail how to teach logic-based skills such as: making mathematical reasoning fully explicit; moving from step to step in a mathematical proof in logically correct ways; and checking to (...) make sure inferences are logically correct. The methodology can easily be extended beyond the four examples analyzed. (shrink)

We prove the cut-elimination theorem, Gentzen's Hauptsatz, for the system for stratified comprehension, i. e. Quine's NF minus extensionality.

We introduce a notion of syntactical truth predicate (s.t.p.) for the second order arithmetic PA 2 . An s.t.p. is a set T of closed formulas such that: (i) T(t = u) if and only if the closed first order terms t and u are convertible, i.e., have the same value in the standard interpretation (ii) T(A → B) if and only if (T(A) $\Longrightarrow$ T(B)) (iii) T(∀ x A) if and only if (T(A[x ← t]) for any closed first (...) order term t) (iv) T(∀ X A) if and only if (T(A[X ←▵]) for any closed set definition $\triangle = \{x \mid D(x)\}$ ). S.t.p.'s can be seen as a counterpart to Tarski's notion of (model-theoretical) validity and have main model properties. In particular, their existence is equivalent to the existence of an ω-model of PA 2 , this fact being provable in PA 2 with arithmetical comprehension only. (shrink)

We introduce a notion ofsyntactical truth predicate(s.t.p.) for the second order arithmeticPA2. An s.t.p. is a setTof closed formulas such that:(i)T(t=u) if and only if the closed first order termstanduare convertible, i.e., have the same value in the standard interpretation(ii)T(A→B) if and only if (T(A) ⇒T(B))(iii)T(∀xA) if and only if (T(A[x←t]) for any closed first order termt)(iv)T(∀X A) if and only if (T(A[X← ∆]) for any closed set definition ∆ = {x∣D(x)}).S.t.p.'s can be seen as a counterpart to Tarski's notion (...) of (model-theoretical)validityand have main model properties. In particular, their existence is equivalent to the existence of anω-model ofPA2, this fact being provable inPA2with arithmetical comprehension only. (shrink)

We develop cut-free calculi of sequents for normal modal logics by using treesequents, which are trees of sequences of formulas. We introduce modal operators corresponding to the ways we move formulas along the branches of such trees, only considering fixed distance movements. Finally, we exhibit syntactic cut-elimination theorems for all the main normal modal logics.

We present sequent calculi for normal modal logics where modal and propositional behaviours are separated, and we prove a cut elimination theorem for the basic system K, so as completeness theorems both for K itself and for its most popular enrichments. MSC: 03B45, 03F05.

A type of first-order analogues of ptykes, namely ‘ptykoids’, are introduced, and bounds are found for the ptykoids of level 1 and 2 which can be proved to be ptykoids in Peano arithmetic. This gives rise toΠ 3 0 andΠ 4 0 independence results.

The notion of a “ptyx” is formalised in second-order arithmetic, and, using proof-theoretic techniques based on sequent-calculus, bounds are obtained for the ptykes of type 1 and 2 which can be proved to be ptykes using arithmetic comprehension.

This article compares classical (or -like) and nonclassical (or -like) axiomatisations of the fixed-point semantics developed by Kripke (J Philos 72(19): 690–716, 1975). Following the line of investigation of Halbach and Nicolai (J Philos Logic 47(2): 227–257, 2018), we do not compare and qua theories of truth simpliciter, but rather qua axiomatisations of the Kripkean conception of truth. We strengthen the central results of Halbach and Nicolai (2018) and Nicolai (Stud Log 106(1): 101–130, 2018), showing that, on the one hand, (...) there is a stronger sense in which some variants of and some variants of can be taken to be, truth-theoretically, equivalent. On the other hand, we show that this truth-theoretical equivalence is not preserved by some other variants of and, arguing that the variants are more adequate axiomatisations of the fixed-point semantics than the corresponding variants. (shrink)

The logical flow graphs of sequent calculus proofs might contain oriented cycles. For the predicate calculus the elimination of cycles might be non-elementary and this was shown in [Car96]. For the propositional calculus, we prove that if a proof of k lines contains n cycles then there exists an acyclic proof with O(k n+l ) lines. In particular, there is a polynomial time algorithm which eliminates cycles from a proof. These results are motivated by the search for general methods on (...) proving lower bounds on proof size and by the design of more efficient heuristic algorithms for proof search. (shrink)

We investigate a new paradigm in the context of learning in the limit, namely, learning correction grammars for classes of computably enumerable (c.e.) languages. Knowing a language may feature a representation of it in terms of two grammars. The second grammar is used to make corrections to the first grammar. Such a pair of grammars can be seen as a single description of (or grammar for) the language. We call such grammars correction grammars. Correction grammars capture the observable fact that (...) people do correct their linguistic utterances during their usual linguistic activities. We show that learning correction grammars for classes of c.e. languages in the TxtEx-model (i.e., converging to a single correct correction grammar in the limit) is sometimes more powerful than learning ordinary grammars even in the TxtBe-model (where the learner is allowed to converge to infinitely many syntactically distinct but correct conjectures in the limit). For each n ≥ 0, there is a similar learning advantage, again in learning correction grammars for classes of c.e. languages, but where we compare learning correction grammars that make n + 1 corrections to those that make n corrections. The concept of a correction grammar can be extended into the constructive transfinite, using the idea of counting-down from notations for transfinite constructive ordinals. This transfinite extension can also be conceptualized as being about learning Ershov-descriptions for c.e. languages. For u a notation in Kleene's general system $(O,\, < _o )$ of ordinal notations for constructive ordinals, we introduce the concept of an u-correction grammar, where u is used to bound the number of corrections that the grammar is allowed to make. We prove a general hierarchy result: if u and v are notations for constructive ordinals such that $u\, < _o \,v$ , then there are classes of c.e. languages that can be TxtEx-learned by conjecturing v-correction grammars but not by conjecturing u-correction grammars. Surprisingly, we show that— above "ω-many" corrections—it is not possible to strengthen the hierarchy: TxtEx-learning u-correction grammars of classes of c.e. languages, where u is a notation in O for any ordinal, can be simulated by TxtBe-learning ω-correction grammars, where ω is any notation for the smallest infinite ordinal ω. (shrink)

This paper discusses lower bounds for proof length, especially as measured by number of steps (inferences). We give the first publicly known proof of Gödel's claim that there is superrecursive (in fact. unbounded) proof speedup of (i + 1)st-order arithmetic over ith-order arithmetic, where arithmetic is formalized in Hilbert-style calculi with + and · as function symbols or with the language of PRA. The same results are established for any weakly schematic formalization of higher-order logic: this allows all tautologies as (...) axioms and allows all generalizations of axioms as axioms. Our first proof of Gödel's claim is based on self-referential sentences: we give a second proof that avoids the use of self-reference based loosely on a method of Statman. (shrink)

In this article we give a unifying approach to the theory of fundamental sequences and their related Hardy hierarchies of number-theoretic functions and we show the equivalence of the new approach with the classical one.

Semantic and soritical paradoxes display remarkable family resemblances. For one thing, several non-classical logics have been independently applied to both kinds of paradoxes. For another, revenge paradoxes and higher-order vagueness—among the most serious problems targeting solutions to semantic and soritical paradoxes—exhibit a rather similar dynamics. Some authors have taken these facts to suggest that truth and vagueness require a unified logical framework, or perhaps that the truth predicate is itself vague. However, a common core of semantic and soritical paradoxes has (...) not been identified yet, and no explanation of their relationships has been provided. Here we aim at filling this lacuna, in the framework of many-valued logics. We provide a unified diagnosis of semantic and soritical paradoxes, identifying their source in a general form of indiscernibility. We then develop our diagnosis into a theory of paradoxicality, which formalizes both semantic and soritical paradoxes as arguments involving specific instances of our generalized indiscernibility principle, and correctly predicts which logics can non-trivially solve them. (shrink)

Gentzen’s approach to deductive systems, and Carnap’s and Popper’s treatment of probability in logic were two fruitful ideas that appeared in logic of the mid-twentieth century. By combining these two concepts, the notion of sentence probability, and the deduction relation formalized in the sequent calculus, we introduce the notion of ’probabilized sequent’ \ with the intended meaning that “the probability of truthfulness of \ belongs to the interval [a, b]”. This method makes it possible to define a system of derivations (...) based on ’axioms’ of the form \, obtained as a result of empirical research, and then infer conclusions of the form \. We discuss the consistency, define the models, and prove the soundness and completeness for the defined probabilized sequent calculus. (shrink)

The logic of the weak law of excluded middleKC p is obtained by adding the formula A A as an axiom scheme to Heyting's intuitionistic logicH p . A cut-free sequent calculus for this logic is given. As the consequences of the cut-elimination theorem, we get the decidability of the propositional part of this calculus, its separability, equality of the negationless fragments ofKC p andH p , interpolation theorems and so on. From the proof-theoretical point of view, the formulation presented (...) in this paper makes clearer the relations betweenKC p ,H p , and the classical logic. In the end, an interpretation of classical propositional logic in the propositional part ofKC p is given. (shrink)

We introduce new proof systems for propositional logic, simple deduction Frege systems, general deduction Frege systems, and nested deduction Frege systems, which augment Frege systems with variants of the deduction rule. We give upper bounds on the lengths of proofs in Frege proof systems compared to lengths in these new systems. As applications we give near-linear simulations of the propositional Gentzen sequent calculus and the natural deduction calculus by Frege proofs. The length of a proof is the number of lines (...) in the proof. A general deduction Frege proof system provides at most quadratic speedup over Frege proof systems. A nested deduction Frege proof system provides at most a nearly linear speedup over Frege system where by "nearly linear" is meant the ratio of proof lengths is O) where α is the inverse Ackermann function. A nested deduction Frege system can linearly simulate the propositional sequent calculus, the tree-like general deduction Frege calculus, and the natural deduction calculus. Hence a Frege proof system can simulate all those proof systems with proof lengths bounded by O). Also we show that a Frege proof of n lines can be transformed into a tree-like Frege proof of O lines and of height O. As a corollary of this fact we can prove that natural deduction and sequent calculus tree-like systems simulate Frege systems with proof lengths bounded by O. (shrink)

In this paper we re-examine the semantics of classical higher-order logic with the purpose of clarifying the role of extensionality. To reach this goal, we distinguish nine classes of higher-order models with respect to various combinations of Boolean extensionality and three forms of functional extensionality. Furthermore, we develop a methodology of abstract consistency methods (by providing the necessary model existence theorems) needed to analyze completeness of (machine-oriented) higher-order calculi with respect to these model classes.

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.

A quasi-canonical Gentzen-type system is a Gentzen-type system in which each logical rule introduces either a formula of the form , or of the form , and all the active formulas of its premises belong to the set . In this paper we investigate quasi-canonical systems in which exactly one of the two classical rules for negation is included, turning the induced logic into either a paraconsistent logic or a paracomplete logic, but not both. We provide a constructive coherence criterion (...) for such systems, and show that a quasi-canonical system of the type we investigate is coherent iff it is strongly paraconsistent or strongly paracomplete (in a sense defined in the paper), iff it has a trivalent, non-deterministic semantics of a special type (also defined in the paper) for which it is sound and complete. Finally, we determine when a system of this sort admits cut-elimination, and provide a simple procedure for transforming one which does not into one which does. (shrink)

Paul Cohen’s method of forcing, together with Saul Kripke’s related semantics for modal and intuitionistic logic, has had profound effects on a number of branches of mathematical logic, from set theory and model theory to constructive and categorical logic. Here, I argue that forcing also has a place in traditional Hilbert-style proof theory, where the goal is to formalize portions of ordinary mathematics in restricted axiomatic theories, and study those theories in constructive or syntactic terms. I will discuss the aspects (...) of forcing that are useful in this respect, and some sample applications. The latter include ways of obtaining conservation results for classical and intuitionistic theories, interpreting classical theories in constructive ones, and constructivizing model-theoretic arguments. (shrink)

In 1933 Godel introduced a calculus of provability (also known as modal logic S4) and left open the question of its exact intended semantics. In this paper we give a solution to this problem. We find the logic LP of propositions and proofs and show that Godel's provability calculus is nothing but the forgetful projection of LP. This also achieves Godel's objective of defining intuitionistic propositional logic Int via classical proofs and provides a Brouwer-Heyting-Kolmogorov style provability semantics for Int which (...) resisted formalization since the early 1930s. LP may be regarded as a unified underlying structure for intuitionistic, modal logics, typed combinatory logic and λ-calculus. (shrink)

Paradefinite logics are logics that can be used for handling contradictory or partial information. As such, paradefinite logics should be both paraconsistent and paracomplete. In this paper we consider the simplest semantic framework for introducing paradefinite logics. It consists of the four-valued matrices that expand the minimal matrix which is characteristic for first degree entailments: Dunn–Belnap matrix. We survey and study the expressive power and proof theory of the most important logics that can be developed in this framework.

Weiermann [18] introduces a new method to generate fast growing functions in order to get an elegant and perspicuous proof of a bounding theorem for provably total recursive functions in a formal theory, e.g., in PA. His fast growing function θαn is described as follows. For each ordinal α and natural number n let T α n denote a finitely branching, primitive recursive tree of ordinals, i.e., an ordinal as a label is attached to each node in the tree so (...) that the labelling is compatible with the tree ordering. Then the tree T α n is well founded and hence finite by Konig's lemma. Define θαn=the depth of the tree T α n =the length of the longest branch in T α n . We introduce new fast and slow growing functions in this mode of definitions and show that each of these majorizes provably total recursive functions in PA. (shrink)

A variety of projects in proof theory of relevance to the philosophy of mathematics are surveyed, including Gödel's incompleteness theorems, conservation results, independence results, ordinal analysis, predicativity, reverse mathematics, speed-up results, and provability logics.

In this note the proof-theoretic ordinal of the well-ordering principle for the normal functions \ on ordinals is shown to be equal to the least fixed point of \. Moreover corrections to the previous paper are made.

Many mathematicians and philosophers of mathematics believe some proofs contain elements extraneous to what is being proved. In this paper I discuss extraneousness generally, and then consider a specific proposal for measuring extraneousness syntactically. This specific proposal uses Gentzen's cut-elimination theorem. I argue that the proposal fails, and that we should be skeptical about the usefulness of syntactic extraneousness measures.

In this note the well-ordering principle for the derivative \ of normal functions \ on ordinals is shown to be equivalent to the existence of arbitrarily large countable coded \-models of the well-ordering principle for the function \.

In this paper we will study a formal system of intuitionistic modal predicate logic. The main result is its semantic completeness theorem with respect to algebraic structures. At the end of the paper we will also present a brief consideration of its syntactic relationships with some similar systems.

A minimal theorem in a logic L is an L-theorem which is not a non-trivial substitution instance of another L-theorem. Komori (1987) raised the question whether every minimal implicational theorem in intuitionistic logic has a unique normal proof in the natural deduction system NJ. The answer has been known to be partially positive and generally negative. It is shown here that a minimal implicational theorem A in intuitionistic logic has a unique -normal proof in NJ whenever A is provable without (...) non-prime contraction. The non-prime contraction rule in NJ is the implication introduction rule whose cancelled assumption differs from a propositional variable and appears more than once in the proof. Our result improves the known partial positive solutions to Komori's problem. Also, we present another simple example of a minimal implicational theorem in intuitionistic logic which does not have a unique -normal proof in NJ. (shrink)

In this paper we address the problem of combining a logic with nonmonotonic modal logic. In particular we study the intuitionistic case. We start from a formal analysis of the notion of intuitionistic consistency via the sequent calculus. The epistemic operator M is interpreted as the consistency operator of intuitionistic logic by introducing intuitionistic stable sets. On the basis of a bimodal structure we also provide a semantics for intuitionistic stable sets.

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.

The article investigates a system of polymorphically typed combinatory logic which is equivalent to Gödel’s T. A notion of (strong) reduction is defined over terms of this system and it is proved that the class of well-formed terms is closed under both bracket abstraction and reduction. The main new result is that the number of contractions needed to reduce a term to normal form is computed by an ε 0-recursive function. The ordinal assignments used to obtain this result are also (...) used to prove that the system under consideration is indeed equivalent to Gödel’s T. It is hoped that the methods used here can be extended so as to obtain similar results for stronger systems of polymorphically typed combinatory terms. An interesting corollary of such results is that they yield ordinally informative proofs of normalizability for sub-systems of second-order intuitionist logic, in natural deduction style. (shrink)

This paper concerns the paraconsistent logic LPQ⊃,F and an application of it in the area of relational database theory. The notions of a relational database, a query applicable to a relational database, and a consistent answer to a query with respect to a possibly inconsistent relational database are considered from the perspective of this logic. This perspective enables among other things the definition of a consistent answer to a query with respect to a possibly inconsistent database without resort to database (...) repairs. In an earlier paper, LPQ⊃,F is presented with a sequent-style natural deduction proof system. In this paper, a sequent calculus proof system is presented instead because such proof systems are generally considered more suitable as the basis of proof search procedures than natural deduction proof systems and proof search procedures can serve as the core of algorithms for computing consistent answers to queries. (shrink)

In this paper we explain our pretense account of truth-talk and apply it in a diagnosis and treatment of the Liar Paradox. We begin by assuming that some form of deflationism is the correct approach to the topic of truth. We then briefly motivate the idea that all T-deflationists should endorse a fictionalist view of truth-talk, and, after distinguishing pretense-involving fictionalism (PIF) from error- theoretic fictionalism (ETF), explain the merits of the former over the latter. After presenting the basic framework (...) of our PIF account of truth-talk, we demonstrate a few advantages it offers over T-deflationist accounts that do not explicitly acknowledge pretense at work in the discourse. In turning to the Liar Paradox, we explain how the quasi-anaphoric functioning that our account attributes to truth-talk provides a diagnosis of the Liar Paradox (and other instances of semantic pathology) as having no content—in the sense of not specifying any of what we call M-conditions. At the same time, however, we vindicate the intuition that we can understand liar sentences, thereby avoiding one standard objection to “meaningless strategy” responses to the Liar Paradox. With this diagnosis in place, we then, by way of treatment, introduce a new predicate, ‘semantically defective’, and show how the explanation we give for its application allows for a consistent, yet revenge-immune, (dis)solution of the Liar Paradox, and semantic pathology generally. (shrink)

This book explains the first published consistency proof of PA. It contains the original Gentzen's proof, but it uses modern terminology and examples to illustrate the essential notions. The author comments on Gentzen's steps which are supplemented with exact calculations and parts of formal derivations. A notable aspect of the proof is the representation of ordinal numbers that was developed by Gentzen. This representation is analysed and connection to set-theoretical representation is found, namely an algorithm for translating Gentzen's notation into (...) Cantor normal form. The topic should interest researchers and students who work on proof theory, history of proof theory or Hilbert's program and who do not mind reading mathematical texts.​. (shrink)

The semantic valuations of classical logic, strong Kleene logic, the logic of paradox and the logic of first-degree entailment, all respect the Dunn conditions: we call them Dunn logics. In this paper, we study the interpolation properties of the Dunn logics and extensions of these logics to more expressive languages. We do so by relying on the \ calculus, a signed tableau calculus whose rules mirror the Dunn conditions syntactically and which characterizes the Dunn logics in a uniform way. In (...) terms of the \ calculus, we first introduce two different interpolation methods, each of which uniformly shows that the Dunn logics have the interpolation property. One of the methods is closely related to Maehara’s method but the other method, which we call the pruned tableau method, is novel to this paper. We provide various reasons to prefer the pruned tableau method to the Maehara-style method. We then turn our attention to extensions of Dunn logics with so-called appropriate implication connectives. Although these logics have been considered at various places in the literature, a study of the interpolation properties of these logics is lacking. We use the pruned tableau method to uniformly show that these extended Dunn logics have the interpolation property and explain that the same result cannot be obtained via the Maehara-style method. Finally, we show how the pruned tableau method constructs interpolants for functionally complete extensions of the Dunn logics. (shrink)