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)

This paper considers proof-theoretic semantics for necessity within Dummett's and Prawitz's framework. Inspired by a system of Pfenning's and Davies's, the language of intuitionist logic is extended by a higher order operator which captures a notion of validity. A notion of relative necessary is defined in terms of it, which expresses a necessary connection between the assumptions and the conclusion of a deduction.

The proof theory of many-valued systems has not been investigated to an extent comparable to the work done on axiomatizatbility of many-valued logics. Proof theory requires appropriate formalisms, such as sequent calculus, natural deduction, and tableaux for classical (and intuitionistic) logic. One particular method for systematically obtaining calculi for all finite-valued logics was invented independently by several researchers, with slight variations in design and presentation. The main aim of this report is to develop the proof theory of finite-valued first order (...) logics in a general way, and to present some of the more important results in this area. In Systems covered are the resolution calculus, sequent calculus, tableaux, and natural deduction. This report is actually a template, from which all results can be specialized to particular logics. (shrink)

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.

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)

Sequent calculi for trilattice logics, including those that are determined by the truth entailment, the falsity entailment and their intersection, are given. This partly answers the problems in Shramko-Wansing.

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)

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)

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.

In this paper are studied the properties of the proofs in PRA of provability logic sentences, i.e. of formulas which are Boolean combinations of formulas of the form PIPRA, where h is the Gödel-number of a sentence in PRA. The main result is a Normal Form Theorem on the proof-trees of provability logic sequents, which states that it is possible to split the proof into an arithmetical part, which contains only atomic formulas and has an essentially intuitionistic character, and into (...) a logical part, which is merely instrumental. Moreover, the induction rules which occur in the arithmetical part are implicit. Some applications of the Normal Form Theorem are shown in order to obtain some syntactical results on the PRA-completeness of modal logic. In particular a completeness theorem for Boolean combinations of modalities is given. (shrink)

This paper gives a Gentzen-style proof of the consistency of Heyting arithmetic in an intuitionistic sequent calculus with explicit rules of weakening, contraction and cut. The reductions of the proof, which transform derivations of a contradiction into less complex derivations, are based on a method for direct cut-elimination without the use of multicut. This method treats contractions by tracing up from contracted cut formulas to the places in the derivation where each occurrence was first introduced. Thereby, Gentzen’s heightline argument, which (...) introduces additional cuts on contracted compound cut formulas, is avoided. To show termination of the reduction procedure an ordinal assignment based on techniques of Howard for Gödel’s T is used. (shrink)

The first attempt at a systematic approach to axiomatic theories of truth was undertaken by Friedman and Sheard (Ann Pure Appl Log 33:1–21, 1987). There twelve principles consisting of axioms, axiom schemata and rules of inference, each embodying a reasonable property of truth were isolated for study. Working with a base theory of truth conservative over PA, Friedman and Sheard raised the following questions. Which subsets of the Optional Axioms are consistent over the base theory? What are the proof-theoretic strengths (...) of the consistent theories? The first question was answered completely by Friedman and Sheard; all subsets of the Optional Axioms were classified as either consistent or inconsistent giving rise to nine maximal consistent theories of truth.They also determined the proof-theoretic strength of two subsets of the Optional Axioms. The aim of this paper is to continue the work begun by Friedman and Sheard. We will establish the proof-theoretic strength of all the remaining seven theories and relate their arithmetic part to well-known theories ranging from PA to the theory of ${\Sigma^1_1}$ dependent choice. (shrink)

This paper presents and motivates a new philosophical and logical approach to truth and semantic paradox. It begins from an inferentialist, and particularly bilateralist, theory of meaning---one which takes meaning to be constituted by assertibility and deniability conditions---and shows how the usual multiple-conclusion sequent calculus for classical logic can be given an inferentialist motivation, leaving classical model theory as of only derivative importance. The paper then uses this theory of meaning to present and motivate a logical system---ST---that conservatively extends classical (...) logic with a fully transparent truth predicate. This system is shown to allow for classical reasoning over the full (truth-involving) vocabulary, but to be non-transitive. Some special cases where transitivity does hold are outlined. ST is also shown to give rise to a familiar sort of model for non-classical logics: Kripke fixed points on the Strong Kleene valuation scheme. Finally, to give a theory of paradoxical sentences, a distinction is drawn between two varieties of assertion and two varieties of denial. On one variety, paradoxical sentences cannot be either asserted or denied; on the other, they must be both asserted and denied. The target theory is compared favourably to more familiar related systems, and some objections are considered. (shrink)

This paper shows how to conservatively extend classical logic with a transparent truth predicate, in the face of the paradoxes that arise as a consequence. All classical inferences are preserved, and indeed extended to the full (truth—involving) vocabulary. However, not all classical metainferences are preserved; in particular, the resulting logical system is nontransitive. Some limits on this nontransitivity are adumbrated, and two proof systems are presented and shown to be sound and complete. (One proof system allows for Cut—elimination, but the (...) other does not.). (shrink)

The goal of the paper is to develop a universal semantic approach to derivable rules of propositional multiple-conclusion sequent calculi with structural rules, which explicitly involve not only atomic formulas, treated as metavariables for formulas, but also formula set variables, upon the basis of the conception of model introduced in :27–37, 2001). One of the main results of the paper is that any regular sequent calculus with structural rules has such class of sequent models that a rule is derivable in (...) the calculus iff it is sound with respect to each model of the semantics. We then show how semantics of admissible rules of such calculi can be found with using a method of free models. Next, our universal approach is applied to sequent calculi for many-valued logics with equality determinant. Finally, we exemplify this application by studying sequent calculi for some of such logics. (shrink)

In a recent article, Azzouni has argued in favor of a version of formalism according to which ordinary mathematical proofs indicate mechanically checkable derivations. This is taken to account for the quasi-universal agreement among mathematicians on the validity of their proofs. Here, the author subjects these claims to a critical examination, recalls the technical details about formalization and mechanical checking of proofs, and illustrates the main argument with aanalysis of examples. In the author's view, much of mathematical reasoning presents genuine (...) meaning-dependent mathematical characteristics that cannot be captured by formal calculi. ‘…there is a conflict between mathematical practice and the formalist doctrine.’ [Kreisel, 1969, p. 39]. (shrink)

In this paper the PA-completeness of modal logic is studied by syntactical and constructive methods. The main results are theorems on the structure of the PA-proofs of suitable arithmetical interpretationsS of a modal sequentS, which allow the transformation of PA-proofs ofS into proof-trees similar to modal proof-trees. As an application of such theorems, a proof of Solovay's theorem on arithmetical completeness of the modal system G is presented for the class of modal sequents of Boolean combinations of formulas of the (...) form p i,m i=0, 1, 2, ... The paper is the preliminary step for a forthcoming global syntactical resolution of the PA-completeness problem for modal logic. (shrink)

With each sentential logic C, identified with a structural consequence operation in a sentential language, the class Matr * (C) of factorial matrices which validate C is associated. The paper, which is a continuation of [2], concerns the connection between the purely syntactic property imposed on C, referred to as Maehara Interpolation Property (MIP), and three diagrammatic properties of the class Matr* (C): the Amalgamation Property (AP), the (deductive) Filter Extension Property (FEP) and Injections Transferable (IT). The main theorem of (...) the paper (Theorem 2.2) is analogous to the Wroski's result for equational classes of algebras [13]. It reads that for a large class of logics the conjunction of (AP) and (FEP) is equivalent to (IT) and that the latter property is equivalent to (MIP). (shrink)

This paper deals with the system of modal logicGL, in particular with a formulation of it in terms of sequents. We prove some proof theoretical properties ofGL that allow to get the cut-elimination theorem according to Gentzen's procedure, that is, by double induction on grade and rank.

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)

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)

Arnold Cusmariu ABSTRACT: The Cogito formulation in Discourse on Method attributes properties to one conceptual category that belong to another. Correcting the error ends up defeating Descartes’ response to skepticism. His own creation, the Evil Genius, is to blame. Download PDF.

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)

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.

The Paradox of the Knower was originally presented by Kaplan and Montague [26] as a puzzle about the everyday notion of knowledge in the face of self-reference. The paradox shows that any theory extending Robinson arithmetic with a predicate K satisfying the factivity axiom K → A as well as a few other epistemically plausible principles is inconsistent. After surveying the background of the paradox, we will focus on a recent debate about the role of epistemic closure principles in the (...) Knower. We will suggest this debate sheds new light on the concept of knowledge which is at issue in the paradox – i.e. is it a “thin” notion divorced from concepts such as evidence or justification, or is it a “thick” notion more closely resembling mathematical provability? We will argue that a number of features of the paradox suggest that the latter option is more plausible. Along the way, we will provide a reconstruction of the paradox using a quantified extension of Artemovʼs [2] Logic of Proofs, as well as a series of results linking the original formulation of the paradox to reflection principles for formal arithmetic. On this basis, we will argue that while the Knower can be understood to motivate a distinction between levels of knowledge, it does not provide a rationale for recognizing a uniform hierarchy of knowledge predicates in the manner suggested by Anderson. (shrink)

The aim of this paper is the analysis of uniformity in Feferman's explicit mathematics. The proof-strength of those systems for constructive mathematics is determined by reductions to subsystems of second-order arithmetic: If uniformity is absent, the method of standard structures yields that the strength of the join axiom collapses. Systems with uniformity and join are treated via cut elimination and asymmetrical interpretations in standard structures.

We introduce a Gentzen-style modal predicate logic and prove the cut-elimination theorem for it. This sequent calculus of cut-free proofs is chosen as a proxy to develop the proof-theory of the logics introduced in [14, 15, 4]. We present syntactic proofs for all the metatheoretical results that were proved model-theoretically in loc. cit. and moreover prove that the form of weak reflection proved in these papers is as strong as possible.

We define theories of bounded arithmetic, whose definable functions and relations are exactly those in certain complexity classes. Based on a recursion-theoretic characterization of NC in Clote , the first-order theory TNC, whose principal axiom scheme is a form of short induction on notation for nondeterministic polynomial-time computable relations, has the property that those functions having nondeterministic polynomial-time graph Θ such that TNC x y Θ are exactly the functions in NC, computable on a parallel random-access machine in polylogarithmic parallel (...) time with a polynomial number of processors.0 We then define three theories of weak second-order arithmetic which respectively characterize relations in the classes of alternating logarithmic time, logspace and nondeterministic logspace. (shrink)

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

Gentzen's original proof of the Hauptsatz used a rule of multicut in the case that the right premiss of cut was derived by contraction. Cut elimination is here proved without multicut, by transforming suitably the derivation of the premiss of the contraction.

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.

Let T(Ω) be the ordinal notation system from Buchholz-Schütte (1988). [The order type of the countable segmentT(Ω)0 is — by Rathjen (1988) — the proof-theoretic ordinal the proof-theoretic ordinal ofACA 0 + (Π 1 l −TR).] In particular let ↦Ω a denote the enumeration function of the infinite cardinals and leta ↦ ψ0 a denote the partial collapsing operation on T(Ω) which maps ordinals of T(Ω) into the countable segment TΩ 0 of T(Ω). Assume that the (fast growing) extended Grzegorczyk (...) hierarchy $(F_a )_{a \in T(\Omega )_0 }$ and the slow growing hierarchy $(G_a )_{a \in T(\Omega )_0 }$ are defined with respect to the natural system of distinguished fundamental sequences of Buchholz and Schütte (1988) in the following way: $$\begin{array}{*{20}c} {G_0 (n): = 0,} & {F_0 (n): = (n + 1)^2 ,} \\ {\begin{array}{*{20}c} {G_{a + 1} (n): = G_a (n) + 1,} \\ {G_l (n): = G_{l[n]} (n),} \\ \end{array} } & {\begin{array}{*{20}c} {F_{a + 1} (n): = \underbrace {F_a (...F_a }_{n + 1 - times}(n)...),} \\ {F_l (n): = F_{l[n]} (n),} \\ \end{array} } \\ \end{array}$$ wherel is a countable limit ordinal (term) and (l[n]) n ∈N is the distinguished fundamental sequence assigned tol. For each ordinal (term)a in T(Ω) and each natural numbern letC n (a) be the formal term which results from the ordinal terma by successively replacing every occurence ofψ a by $\psi _{ - 1 + C_n (a)}$ whereψ −1 is considered as a defined function symbol, namely $\psi _{ - 1} b: = F_{\psi _0 b + 1} (n + 1)$ . (Note thatψ a 0=Ω a ) In this article it is shown that for each ordinal termψ 0 a in T(Ω) there exists a natural numbern 0 such thatψ 0 C n (a) ∈ T(Ω) and $G_{\psi _0 a} (n) \leqslant F_{\psi _0 C_n (a) + 1} (n + 1)$ holds for alln≥n 0. This hierarchy comparison theorem yields a plethora of new results on nontrivial lower bounds for the slow growing ordinals — i.e. ordinals for which the slow growing hierarchy yields a classification of the provably total functions of the theory in question — of various theories of iterated inductive definitions (and subsystems ofKPi) and on the number and size of the subrecursively inaccessible ordinals — i.e. ordinals at which the extended Grzegorczyk hierarchy and the slow growing hierarchy catch up — below the proof-theoretic ordinal ofACA 0+(Π 1 l −TR). In particular these subrecursively inaccessibles ordinals are necessarily of the form $\psi _0 \Omega ..._{\Omega _\omega }$. (shrink)

In 1983, Valentini presented a syntactic proof of cut elimination for a sequent calculus GLSV for the provability logic GL where we have added the subscript V for “Valentini”. The sequents in GLSV were built from sets, as opposed to multisets, thus avoiding an explicit contraction rule. From a syntactic point of view, it is more satisfying and formal to explicitly identify the applications of the contraction rule that are ‘hidden’ in these set based proofs of cut elimination. There is (...) often an underly ing assumption that the move to a proof of cut elimination for sequents built from multisets is easy. Recently, however, it has been claimed that Valentini’s arguments to eliminate cut do not terminate when applied to a multiset formulation of GLSV with an explicit rule of contraction. The claim has led to much confusion and various authors have sought new proofs of cut elimination for GL in a multiset setting. Here we refute this claim by placing Valentini’s arguments in a formal setting and proving cut elimination for sequents built from multisets. The formal setting is particularly important for sequents built from multisets, in order to accurately account for the interplay between the weakening and contraction rules. Furthermore, Valentini’s original proof relies on a novel induction parameter called “width” which is computed ‘globally’. It is diffi cult to verify the correctness of his induction argument based on “width”. In our formulation however, verification of the induction argument is straight forward. Finally, the multiset setting also introduces a new complication in the the case of contractions above cut when the cut formula is boxed. We deal with this using a new transformation based on Valentini’s original arguments. Finally, we show that the algorithm purporting to show the non termi nation of Valentini’s arguments is not a faithful representation of the original arguments, but is instead a transformation already known to be insufficient. (shrink)

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.

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.

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)

A semantical proof of Craig's interpolation theorem for the intuitionistic predicate logic and some intermediate prepositional logics will be given. Our proof is an extension of Henkin's method developed in [4]. It will clarify the relation between the interpolation theorem and Robinson's consistency theorem for these logics and will enable us to give a uniform way of proving the interpolation theorem for them.

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

In the first part we show why ordinals and ordinal notations are naturally connected with proof theoretical research. We introduce the program of ordinal analysis. The second part gives examples of applications of ordinal analysis.

We introduce the appropriate iterated version of the system of ordinal notations from [G1] whose order type is the familiar Howard ordinal. As in [G1], our ordinal notations are partly inspired by the ideas from [P] where certain crucial properties of the traditional Munich' ordinal notations are isolated and used in the cut-elimination proofs. As compared to the corresponding “impredicative” Munich' ordinal notations (see e.g. [B1, B2, J, Sch1, Sch2, BSch]), our ordinal notations arearbitrary terms in the appropriate simple term (...) algebra based on the notion of collapsing functions (which we would rather identify as projective functions). In Sect. 1 below we define the systems of ordinal notationsPRJ( ), for any primitive recursive limit wellordering . In Sect. 2 we prove the crucial well-foundness property by using the appropriate well-quasi-ordering property of the corresponding binary labeled trees [G3]. In Sect. 3 we interprete inPRJ( ) the familiar Veblen-Bachmann hierarchy of ordinal functions, and in Sect. 4 we show that the corresponding Buchholz's system of ordinal notationsOT( ) is a proper subsystem ofPRJ( ), although it has the same order type according to [G3] together with the interpretation from Sect. 2 in the terms of labeled trees. In Sect. 5 we use Friedman's approach in order to obtain an appropriate purely combinatorial statement which is not provable in the theory of iterated inductive definitions ID< λ, for arbitrarily large limit ordinalλ. Formal theories, axioms, etc. used below are familiar in the proof theory of subsystems of analysis (see [BFPS, T, BSch]). (shrink)