In “Some Remarks on Extending and Interpreting Theories with a Partial Truth Predicate”, Reinhardt [21] famously proposed an instrumentalist interpretation of the truth theory Kripke–Feferman ( $\mathrm {KF}$ ) in analogy to Hilbert’s program. Reinhardt suggested to view $\mathrm {KF}$ as a tool for generating “the significant part of $\mathrm {KF}$ ”, that is, as a tool for deriving sentences of the form $\mathrm{Tr}\ulcorner {\varphi }\urcorner $. The constitutive question of Reinhardt’s program was whether it was possible “to justify the (...) use of nonsignificant sentences entirely within the framework of significant sentences”. This question was answered negatively by Halbach & Horsten [10] but we argue that under a more careful interpretation the question may receive a positive answer. To this end, we propose to shift attention from $\mathrm {KF}$ -provably true sentences to $\mathrm {KF}$ -provably true inferences, that is, we shall identify the significant part of $\mathrm {KF}$ with the set of pairs $\langle {\Gamma, \Delta }\rangle $, such that $\mathrm {KF}$ proves that if all members of $\Gamma $ are true, at least one member of $\Delta $ is true. In way of addressing Reinhardt’s question we show that the provably true inferences of suitable $\mathrm {KF}$ -like theories coincide with the provable sequents of matching versions of the theory Partial Kripke–Feferman ( $\mathrm {PKF}$ ). (shrink)

Kreisel’s conjecture is the statement: if, for all$n\in \mathbb {N}$,$\mathop {\text {PA}} \nolimits \vdash _{k \text { steps}} \varphi (\overline {n})$, then$\mathop {\text {PA}} \nolimits \vdash \forall x.\varphi (x)$. For a theory of arithmeticT, given a recursive functionh,$T \vdash _{\leq h} \varphi $holds if there is a proof of$\varphi $inTwhose code is at most$h(\#\varphi )$. This notion depends on the underlying coding.${P}^h_T(x)$is a predicate for$\vdash _{\leq h}$inT. It is shown that there exist a sentence$\varphi $and a total recursive functionhsuch that$T\vdash (...) _{\leq h}\mathop {\text {Pr}} \nolimits _T(\ulcorner \mathop {\text {Pr}} \nolimits _T(\ulcorner \varphi \urcorner )\rightarrow \varphi \urcorner )$, but, where$\mathop {\text {Pr}} \nolimits _T$stands for the standard provability predicate inT. This statement is related to a conjecture by Montagna. Also variants and weakenings of Kreisel’s conjecture are studied. By the use of reflexion principles, one can obtain a theory$T^h_\Gamma $that extendsTsuch that a version of Kreisel’s conjecture holds: given a recursive functionhand$\varphi (x)$a$\Gamma $-formula (where$\Gamma $is an arbitrarily fixed class of formulas) such that, for all$n\in \mathbb {N}$,$T\vdash _{\leq h} \varphi (\overline {n})$, then$T^h_\Gamma \vdash \forall x.\varphi (x)$. Derivability conditions are studied for a theory to satisfy the following implication: if, then$T\vdash \forall x.\varphi (x)$. This corresponds to an arithmetization of Kreisel’s conjecture. It is shown that, for certain theories, there exists a functionhsuch that$\vdash _{k \text { steps}}\ \subseteq\ \vdash _{\leq h}$. (shrink)

We systematically study conservation theorems on theories of semi-classical arithmetic, which lie in-between classical arithmetic $\mathsf {PA}$ and intuitionistic arithmetic $\mathsf {HA}$. Using a generalized negative translation, we first provide a structured proof of the fact that $\mathsf {PA}$ is $\Pi _{k+2}$ -conservative over $\mathsf {HA} + {\Sigma _k}\text {-}\mathrm {LEM}$ where ${\Sigma _k}\text {-}\mathrm {LEM}$ is the axiom scheme of the law-of-excluded-middle restricted to formulas in $\Sigma _k$. In addition, we show that this conservation theorem is optimal in the (...) sense that for any semi-classical arithmetic T, if $\mathsf {PA}$ is $\Pi _{k+2}$ -conservative over T, then ${T}$ proves ${\Sigma _k}\text {-}\mathrm {LEM}$. In the same manner, we also characterize conservation theorems for other well-studied classes of formulas by fragments of classical axioms or rules. This reveals the entire structure of conservation theorems with respect to the arithmetical hierarchy of classical principles. (shrink)

This paper is dedicated to extending and adapting to modal logic the approach of fractional semantics to classical logic. This is a multi-valued semantics governed by pure proof-theoretic considerations, whose truth-values are the rational numbers in the closed interval $[0,1]$. Focusing on the modal logic K, the proposed methodology relies on three key components: bilateral sequent calculus, invertibility of the logical rules, and stability (proof-invariance). We show that our semantic analysis of K affords an informational refinement with respect to the (...) standard Kripkean semantics (a new proof of Dugundji’s theorem is a case in point) and it raises the prospect of a proof-theoretic semantics for modal logic. (shrink)

Vardanyan’s Theorems [36, 37] state that $\mathsf {QPL}(\mathsf {PA})$ —the quantified provability logic of Peano Arithmetic—is $\Pi ^0_2$ complete, and in particular that this already holds when the language is restricted to a single unary predicate. Moreover, Visser and de Jonge [38] generalized this result to conclude that it is impossible to computably axiomatize the quantified provability logic of a wide class of theories. However, the proof of this fact cannot be performed in a strictly positive signature. The system $\mathsf (...) {QRC_1}$ was previously introduced by the authors [1] as a candidate first-order provability logic. Here we generalize the previously available Kripke soundness and completeness proofs, obtaining constant domain completeness. Then we show that $\mathsf {QRC_1}$ is indeed complete with respect to arithmetical semantics. This is achieved via a Solovay-type construction applied to constant domain Kripke models. As corollaries, we see that $\mathsf {QRC_1}$ is the strictly positive fragment of $\mathsf {QGL}$ and a fragment of $\mathsf {QPL}(\mathsf {PA})$. (shrink)

Purity is known as an ideal of proof that restricts a proof to notions belonging to the ‘content’ of the theorem. In this paper, our main interest is to develop a conception of purity for formal (natural deduction) proofs. We develop two new notions of purity: one based on an ontological notion of the content of a theorem, and one based on the notions of surrogate ontological content and structural content. From there, we characterize which (classical) first-order natural deduction proofs (...) of a mathematical theorem are pure. Formal proofs that refer to the ontological content of a theorem will be called ‘fully ontologically pure’. Formal proofs that refer to a surrogate ontological content of a theorem will be called ‘secondarily ontologically pure’, because they preserve the structural content of a theorem. We will use interpretations between theories to develop a proof-theoretic criterion that guarantees secondary ontological purity for formal proofs. (shrink)

We present a series of proof systems for exact entailment (i.e. relevant truthmaker preservation from premises to conclusion) and prove soundness and completeness. Using the proof systems, we observe that exact entailment is not only hyperintensional in the sense of Cresswell but also in the sense recently proposed by Odintsov and Wansing.

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)

This article provides a detailed comparison between two systems of collapsing functions. These functions play a crucial role in proof theory, in the analysis of patterns of resemblance, and the analysis of maximal order types of well partial orders. The exact correspondence given here serves as a starting point for far reaching extensions of current results on patterns and well partial orders. © 2011 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim.

In this paper I argue for an association between impurity and explanatory power in contemporary mathematics. This proposal is defended against the ancient and influential idea that purity and explanation go hand-in-hand (Aristotle, Bolzano) and recent suggestions that purity/impurity ascriptions and explanatory power are more or less distinct (Section 1). This is done by analyzing a central and deep result of additive number theory, Szemerédi’s theorem, and various of its proofs (Section 2). In particular, I focus upon the radically impure (...) (ergodic) proof due to Furstenberg (Section 3). Furstenberg’s ergodic proof is striking because it utilizes intuitively foreign and infinitary resources to prove a finitary combinatorial result and does so in a perspicuous fashion. I claim that Furstenberg’s proof is explanatory in light of its clear expression of a crucial structural result, which provides the “reason why” Szemerédi’s theorem is true. This is, however, rather surprising: how can such intuitively different conceptual resources “get a grip on” the theorem to be proved? I account for this phenomenon by articulating a new construal of the content of a mathematical statement, which I call structural content (Section 4). I argue that the availability of structural content saves intuitive epistemic distinctions made in mathematical practice and simultaneously explicates the intervention of surprising and explanatorily rich conceptual resources. Structural content also disarms general arguments for thinking that impurity and explanatory power might come apart. Finally, I sketch a proposal that, once structural content is in hand, impure resources lead to explanatory proofs via suitably understood varieties of simplification and unification (Section 5). (shrink)

Minimally inconsistent LP (MiLP) is a nonmonotonic paraconsistent logic based on Graham Priest's logic of paradox (LP). Unlike LP, MiLP purports to recover, in consistent situations, all of classical reasoning. The present paper conducts a proof-theoretic analysis of MiLP. I highlight certain properties of this logic, introduce a simple sequent system for it, and establish soundness and completeness results. In addition, I show how to use my proof system in response to a criticism of this logic put forward by JC (...) Beall. (shrink)

Isomorphism between formulae is defined with respect to categories formalizing equality of deductions in classical propositional logic and in the multiplicative fragment of classical linear propositional logic caught by proof nets. This equality is motivated by generality of deductions. Characterizations are given for pairs of isomorphic formulae, which lead to decision procedures for this isomorphism.

This paper is a direct successor to 12. Its aim is to introduce a new realisability interpretation for weak systems of explicit mathematics and use it in order to analyze extensions of the theory PET in 12 by the so-called join axiom of explicit mathematics.

We provide a sound and complete proof system for an extension of Kleene’s ternary logic to predicates. The concept of theory is extended with, for each function symbol, a formula that specifies when the function is defined. The notion of “is defined” is extended to terms and formulas via a straightforward recursive algorithm. The “is defined” formulas are constructed so that they themselves are always defined. The completeness proof relies on the Henkin construction. For each formula, precisely one of the (...) formula, its negation, and the negation of its “is defined” formula is true on the constructed model. Many other ternary logics in the literature can be reduced to ours. Partial functions are ubiquitous in computer science and even in (in)equation solving at schools. Our work was motivated by an attempt to precisely explain, in terms of logic, typical informal methods of reasoning in such applications. (shrink)

In order to allow the use of axioms in a second‐order system of extracting programs from proofs, we define constant terms, a form of Curry‐Howard terms, whose types are intended to correspond to those axioms. We also define new reduction rules for these new terms so that all consequences of the axioms can be represented. We finally show that the extended Curry‐Howard terms are strongly normalizable.

We consider fragments of uniform reflection for formulas in the analytic hierarchy over theories of second order arithmetic. The main result is that for any second order arithmetic theory $T_0$ extending $\mathsf {RCA}_0$ and axiomatizable by a $\Pi ^1_{k+2}$ sentence, and for any $n\geq k+1$, $$\begin{align*}T_0+ \mathrm{RFN}_{\varPi^1_{n+2}} \ = \ T_0 + \mathrm{TI}_{\varPi^1_n}, \end{align*}$$ $$\begin{align*}T_0+ \mathrm{RFN}_{\varSigma^1_{n+1}} \ = \ T_0+ \mathrm{TI}_{\varPi^1_n}^{-}, \end{align*}$$ where T is $T_0$ augmented with full induction, and $\mathrm {TI}_{\varPi ^1_n}^{-}$ denotes the schema of transfinite induction up (...) to $\varepsilon _0$ for $\varPi ^1_n$ formulas without set parameters. (shrink)

We introduce and analyze a new axiomatic theory $\mathsf {CD}$ of truth. The primitive truth predicate can be applied to sentences containing the truth predicate. The theory is thoroughly classical in the sense that $\mathsf {CD}$ is not only formulated in classical logic, but that the axiomatized notion of truth itself is classical: The truth predicate commutes with all quantifiers and connectives, and thus the theory proves that there are no truth value gaps or gluts. To avoid inconsistency, the instances (...) of the T-schema are restricted to determinate sentences. Determinateness is introduced as a further primitive predicate and axiomatized. The semantics and proof theory of $\mathsf {CD}$ are analyzed. (shrink)

The paper provides a proof theoretic characterization of the Russellian theory of definite descriptions (RDD) as characterized by Kalish, Montague and Mar (KMM). To this effect three sequent calculi are introduced: LKID0, LKID1 and LKID2. LKID0 is an auxiliary system which is easily shown to be equivalent to KMM. The main research is devoted to LKID1 and LKID2. The former is simpler in the sense of having smaller number of rules and, after small change, satisfies cut elimination but fails to (...) satisfy the subformula property. In LKID2 an additional analysis of different kinds of identities leads to proliferation of rules but yields the subformula property. This refined proof theoretic analysis leading to fully analytic calculus with constructive proof of cut elimination is the main contribution of the paper. (shrink)

Inferentialism is a theory in the philosophy of language which claims that the meanings of expressions are constituted by inferential roles or relations. Instead of a traditional model-theoretic semantics, it naturally lends itself to a proof-theoretic semantics, where meaning is understood in terms of inference rules with a proof system. Most work in proof-theoretic semantics has focused on logical constants, with comparatively little work on the semantics of non-logical vocabulary. Drawing on Robert Brandom’s notion of material inference and Greg Restall’s (...) bilateralist interpretation of the multiple conclusion sequent calculus, I present a proof-theoretic semantics for atomic sentences and their constituent names and predicates. The resulting system has several interesting features: (1) the rules are harmonious and stable; (2) the rules create a structure analogous to familiar model-theoretic semantics; and (3) the semantics is compositional, in that the rules for atomic sentences are determined by those for their constituent names and predicates. (shrink)

Alongside the analogy between maximal ideals and complete theories, the Jacobson radical carries over from ideals of commutative rings to theories of propositional calculi. This prompts a variant of Lindenbaum’s Lemma that relates classical validity and intuitionistic provability, and the syntactical counterpart of which is Glivenko’s Theorem. The Jacobson radical in fact turns out to coincide with the classical deductive closure. As a by-product we obtain a possible interpretation in logic of the axioms-as-rules conservation criterion for a multi-conclusion Scott-style entailment (...) relation over a single-conclusion one. (shrink)

Let T be Kripke–Platek set theory with infinity extended by the axiom (Beta) plus the schema that claims that every set-bounded Σ-definable monotone operator from the collection of all sets to Pow(a) for some set a has a fixed point. Then T proves that every such operator has a least fixed point. This result is obtained by following the proof of an analogous result for von Neumann–Bernays–Gödel set theory in an earlier work by Sato, with some minor modifications.

We prove a result relating the author's monotone functional interpretation to the bounded functional interpretation due to Ferreira and Oliva. More precisely we show that largely a solution for the bounded interpretation also is a solution for the monotone functional interpretation although the latter uses the existence of an underlying precise witness. This makes it possible to focus on the extraction of bounds while using the conceptual benefit of having precise realizers at the same time without having to construct them.

Inferentialism is a theory in the philosophy of language which claims that the meanings of expressions are constituted by inferential roles or relations. Instead of a traditional model-theoretic semantics, it naturally lends itself to a proof-theoretic semantics, where meaning is understood in terms of inference rules with a proof system. Most work in proof-theoretic semantics has focused on logical constants, with comparatively little work on the semantics of non-logical vocabulary. Drawing on Robert Brandom’s notion of material inference and Greg Restall’s (...) bilateralist interpretation of the multiple conclusion sequent calculus, I present a proof-theoretic semantics for atomic sentences and their constituent names and predicates. The resulting system has several interesting features: (1) the rules are harmonious and stable; (2) the rules create a structure analogous to familiar model-theoretic semantics; and (3) the semantics is compositional, in that the rules for atomic sentences are determined by those for their constituent names and predicates. (shrink)

We explore the problems that confront any attempt to explain or explicate exactly what a primitive logical rule of inferenceis, orconsists in. We arrive at a proposed solution that places a surprisingly heavy load on the prospect of being able to understand and deal with specifications of rules that are essentiallyself-referring. That is, any rule$\rho $is to be understood via a specification that involves, embedded within it, reference to rule$\rho $itself. Just how we arrive at this position is explained by (...) reference to familiar rules as well as less familiar ones with unusual features. An inquiry of this kind is surprisingly absent from the foundations of inferentialism—the view that meanings of expressions (especially logical ones) are to be characterized by the rules of inference that govern them. (shrink)