Different natural deduction proof systems for intuitionistic and classical logic —and related logical systems—differ in fundamental properties while sharing significant family resemblances. These differences become quite stark when it comes to the structural rules of contraction and weakening. In this paper, I show how Gentzen and Jaśkowski’s natural deduction systems differ in fine structure. I also motivate directed proof nets as another natural deduction system which shares some of the design features of Genzen and Jaśkowski’s systems, but which (...) differs again in its treatment of the structural rules, and has a range of virtues absent from traditional natural deduction systems. (shrink)

Tetravalent modal logic (TML) was introduced by Font and Rius in 2000. It is an expansion of the Belnap-Dunn four-valued logic FOUR, a logical system that is well-known for the many applications found in several fields. Besides, TML is the logic that preserves degrees of truth with respect to Monteiro’s tetravalent modal algebras. Among other things, Font and Rius showed that TML has a strongly adequate sequent system, but unfortunately this system does not enjoy the cut-elimination property. However, in a (...) previous work we presented a sequent system for TML with the cut-elimination property. Besides, in this same work, it was also presented a sound and complete natural deduction system for this logic. In the present article we continue with the study of TML under a proof-theoretic perspective. In the first place, we show that the natural deduction system that we introduced before admits a normalization theorem. In the second place, taking advantage of the contrapositive implication for the tetravalent modal algebras introduced by A. V. Figallo and P. Landini, we define a decidable tableau system adequate to check validity in the logic TML. Finally, we provide a sound and complete tableau system for TML in the original language. These two tableau systems constitute new (proof-theoretic) decision procedures for checking validity in the variety of tetravalent modal algebras. (shrink)

A minimal formula is a formula which is minimal in provable formulas with respect to the substitution relation. This paper shows the following: (1) A β-normal proof of a minimal formula of depth 2 is unique in NJ. (2) There exists a minimal formula of depth 3 whose βη-normal proof is not unique in NJ. (3) There exists a minimal formula of depth 3 whose βη-normal proof is not unique in NK.

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, I provide a thorough discussion and reconstruction of Bernard Bolzano’s theory of grounding and a detailed investigation into the parallels between his concept of grounding and current notions of normal proofs. Grounding (Abfolge) is an objective ground-consequence relation among true propositions that is explanatory in nature. The grounding relation plays a crucial role in Bolzano’s proof-theory, and it is essential for his views on the ideal buildup of scientific theories. Occasionally, similarities have been pointed out (...) between Bolzano’s ideas on grounding and cut-free proofs in Gentzen’s sequent calculus. My thesis is, however, that they bear an even stronger resemblance to the normal natural deduction proofs employed in proof-theoretic semantics in the tradition of Dummett and Prawitz. (shrink)

In this paper a proof of the normal form theorem for the closed terms of Girard's system F is given by using a computability method à la Tait. It is worth noting that most of the standard consequences of the normal form theorem can be obtained using this version of the theorem as well. From the proof-theoretical point of view the interest of the proof is that the definition of computable derivation here used does not (...) seem to be well founded. MSC: 03F05, 03B15. (shrink)

Natural deduction (for short: nd-) calculi have not been used systematically as a basis for automated theorem proving in classical logic. To remove objective obstacles to their use we describe (1) a method that allows to give semantic proofs of normal form theorems for nd-calculi and (2) a framework that allows to search directly for normal nd-proofs. Thus, one can try to answer the question: How do we bridge the gap between claims and assumptions in heuristically motivated ways? (...) This informal question motivates the formulation of intercalation calculi. Ic-calculi are the technical underpinnings for (1) and (2), and our paper focuses on their detailed presentation and meta-mathematical investigation in the case of classical predicate logic. As a central theme emerges the connection between restricted forms of nd-proofs and (strategies for) proof search: normal forms are not obtained by removing local "detours", but rather by constructing proofs that directly reflect proof-strategic considerations. That theme warrants further investigation. (shrink)

Wilfred Sieg and Saverio Cittadini. Normal Natural Deduction Proof (In Non-Classical Logics.

Natural deduction (for short: nd-) calculi have not been used systematically as a basis for automated theorem proving in classical logic. To remove objective obstacles to their use we describe (1) a method that allows to give semantic proofs of normal form theorems for nd-calculi and (2) a framework that allows to search directly for normal nd-proofs. Thus, one can try to answer the question: How do we bridge the gap between claims and assumptions in heuristically motivated ways? (...) This informal question motivates the formulation of intercalation calculi. Ic-calculi are the technical underpinnings for (1) and (2), and our paper focuses on their detailed presentation and meta-mathematical investigation in the case of classical predicate logic. As a central theme emerges the connection between restricted forms of nd-proofs and (strategies for) proof search: normal forms are not obtained by removing local "detours", but rather by constructing proofs that directly reflect proof-strategic considerations. That theme warrants further investigation. (shrink)

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

A method is described for obtaining conjunctive normal forms for logics using Gentzen-style rules possessing a special kind of strong invertibility. This method is then applied to a number of prominent fuzzy logics using hypersequent rules adapted from calculi defined in the literature. In particular, a normal form with simple McNaughton functions as literals is generated for łukasiewicz logic, and normal forms with simple implicational formulas as literals are obtained for Gödel logic, Product logic, and Cancellative hoop (...) logic. (shrink)

In this paper we provide a detailed proof-theoretical analysis of a natural deduction system for classical propositional logic that (i) represents classical proofs in a more natural way than standard Gentzen-style natural deduction, (ii) admits of a simple normalization procedure such that normal proofs enjoy the Weak Subformula Property, (iii) provides the means to prove a Non-contamination Property of normal proofs that is not satisfied by normal proofs in the Gentzen tradition and is useful for applications, (...) especially in formal argumentation, (iv) naturally leads to defining a notion of depth of a proof, to the effect that, for every fixed natural k, normal k-depth deducibility is a tractable problem and converges to classical deducibility as k tends to infinity. (shrink)

Proof-theoretical notions and techniques, developed on the basis of sentential/symbolic representations of formal proofs, are applied to Euler diagrams. A translation of an Euler diagrammatic system into a natural deduction system is given, and the soundness and faithfulness of the translation are proved. Some consequences of the translation are discussed in view of the notion of free ride, which is mainly discussed in the literature of cognitive science as an account of inferential efficacy of diagrams. The translation enables us (...) to formalize and analyze free ride in terms of proof theory. The notion of normal form of Euler diagrammatic proofs is investigated, and a normalization theorem is proved. Some consequences of the theorem are further discussed: in particular, an analysis of the structure of normal diagrammatic proofs; a diagrammatic counterpart of the usual subformula property; and a characterization of diagrammatic proofs compared with natural deduction proofs. (shrink)

There is much to like about the idea that justification should be understood in terms of normality or normic support (Smith 2016, Goodman and Salow 2018). The view does a nice job explaining why we should think that lottery beliefs differ in justificatory status from mundane perceptual or testimonial beliefs. And it seems to do that in a way that is friendly to a broadly internalist approach to justification. In spite of its attractions, we think that the normic support view (...) faces two serious challenges. The first is that it delivers the wrong result in preface cases. These cases suggest that the view is either too sceptical or too externalist. The second is that the view struggles with certain kinds of Moorean absurdities. It turns out that these problems can easily be avoided. If we think of normality as a condition on *knowledge*, we can characterise justification in terms of its connection to knowledge and thereby avoid the difficulties discussed here. The resulting view does an equally good job explaining why we should think that our perceptual and testimonial beliefs are justified when lottery beliefs cannot be. Thus, it seems that little could be lost and much could be gained by revising the proposal and adopting a view on which it is knowledge, not justification, that depends directly upon normality. (shrink)

I give an account of proof terms for derivations in a sequent calculus for classical propositional logic. The term for a derivation δ of a sequent Σ≻Δ encodes how the premises Σ and conclusions Δ are related in δ. This encoding is many–to–one in the sense that different derivations can have the same proof term, since different derivations may be different ways of representing the same underlying connection between premises and conclusions. However, not all proof terms for (...) a sequent Σ≻Δ are the same. There may be different ways to connect those premises and conclusions. -/- Proof terms can be simplified in a process corresponding to the elimination of cut inferences in sequent derivations. However, unlike cut elimination in the sequent calculus, each proof term has a unique normal form (from which all cuts have been eliminated) and it is straightforward to show that term reduction is strongly normalising—every reduction process terminates in that unique normal form. Further- more, proof terms are invariants for sequent derivations in a strong sense—two derivations δ1 and δ2 have the same proof term if and only if some permutation of derivation steps sends δ1 to δ2 (given a relatively natural class of permutations of derivations in the sequent calculus). Since not every derivation of a sequent can be permuted into every other derivation of that sequent, proof terms provide a non-trivial account of the identity of proofs, independent of the syntactic representation of those proofs. (shrink)

A complementary system for a given logic is a proof system whose theorems are exactly the formulas that are not valid according to the logic in question. This article is a contribution to the complementary proof theory of classical propositional logic. In particular, we present a complementary proof-net system, $$\textsf{CPN}$$ CPN, that is sound and complete with respect to the set of all classically invalid (one-side) sequents. We also show that cut elimination in $$\textsf{CPN}$$ CPN enjoys strong (...) normalization along with strong confluence (and, hence, uniqueness of normal forms). (shrink)

Algebraic proofs of the cut-elimination theorems for classical and intuitionistic logic are presented, and are used to show how one can sometimes extract a constructive proof and an algorithm from a proof that is nonconstructive. A variation of the double-negation translation is also discussed: if ϕ is provable classically, then ¬(¬ϕ)nf is provable in minimal logic, where θnf denotes the negation-normal form of θ. The translation is used to show that cut-elimination theorems for classical logic can be (...) viewed as special cases of the cut-elimination theorems for intuitionistic logic. (shrink)

We extend natural deduction for first-order logic (FOL) by introducing diagrams as components of formal proofs. From the viewpoint of FOL, we regard a diagram as a deductively closed conjunction of certain FOL formulas. On the basis of this observation, we first investigate basic heterogeneous logic (HL) wherein heterogeneous inference rules are defined in the styles of conjunction introduction and elimination rules of FOL. By examining what is a detour in our heterogeneous proofs, we discuss that an elimination-introduction pair of (...) rules constitutes a redex in our HL, which is opposite the usual redex in FOL. In terms of the notion of a redex, we prove the normalization theorem for HL, and we give a characterization of the structure of heterogeneous proofs. Every normal proof in our HL consists of applications of introduction rules followed by applications of elimination rules, which is also opposite the usual form of normal proofs in FOL. Thereafter, we extend the basic HL by extending the heterogeneous rule in the style of general elimination rules to include a wider range of heterogeneous systems. (shrink)

A general method for generating contraction- and cut-free sequent calculi for a large family of normal modal logics is presented. The method covers all modal logics characterized by Kripke frames determined by universal or geometric properties and it can be extended to treat also Gödel-Löb provability logic. The calculi provide direct decision methods through terminating proof search. Syntactic proofs of modal undefinability results are obtained in the form of conservativity theorems.

In this dissertation, we shall investigate whether Tennant's criterion for paradoxicality(TCP) can be a correct criterion for genuine paradoxes and whether the requirement of a normal derivation(RND) can be a proof-theoretic solution to the paradoxes. Tennant’s criterion has two types of counterexamples. The one is a case which raises the problem of overgeneration that TCP makes a paradoxical derivation non-paradoxical. The other is one which generates the problem of undergeneration that TCP renders a non-paradoxical derivation paradoxical. Chapter 2 (...) deals with the problem of undergeneration and Chapter 3 concerns the problem of overgeneration. Chapter 2 discusses that Tenant’s diagnosis of the counterexample which applies CR−rule and causes the undergeneration problem is not correct and presents a solution to the problem of undergeneration. Chapter 3 argues that Tennant’s diagnosis of the counterexample raising the overgeneration problem is wrong and provides a solution to the problem. Finally, Chapter 4 addresses what should be explicated in order for RND to be a proof-theoretic solution to the paradoxes. (shrink)

Let ℳ be a countable, recursively saturated model of Peano Arithmetic, and let Aut be its automorphism group considered as a topological group with the pointwise stabilizers of finite sets being the basic open subgroups. Kaye proved that the closed normal subgroups are precisely the obvious ones, namely the stabilizers of invariant cuts. A proof of Kaye's theorem is given here which, although based on his proof, is different enough to yield consequences not obtainable from Kaye's (...) class='Hi'>proof. (shrink)

This paper provides a proof-theoretic study of quantified non-normal modal logics. It introduces labelled sequent calculi based on neighbourhood semantics for the first-order extension, with both varying and constant domains, of monotone NNML, and studies the role of the Barcan formulas in these calculi. It will be shown that the calculi introduced have good structural properties: invertibility of the rules, height-preserving admissibility of weakening and contraction and syntactic cut elimination. It will also be shown that each of the (...) calculi introduced is sound and complete with respect to the appropriate class of neighbourhood frames. In particular, the completeness proof constructs a formal derivation for derivable sequents and a countermodel for non-derivable ones, and gives a semantic proof of the admissibility of cut. (shrink)

In this paper it is suggested to generalize our understanding of general (structural) proof theory and to consider it as a general theory of two kinds of derivations, namely proofs and dual proofs. The proposal is substantiated by (i) considerations on assertion, denial, and bi-lateralism, (ii) remarks on compositionality in proof-theoretic semantics, and (iii) comments on falsification and co-implication. The main formal result of the paper is a normal form theorem for the natural deduction proof system (...) N2Int of the bi-intuitionistic logic 2Int. The proof makes use of the faithful embedding of 2Int into intuitionistic logic with respect to validity and shows that conversions of dual proofs can be sidestepped. (shrink)

Normal 0 false false false MicrosoftInternetExplorer4 /* Style Definitions */ table.MsoNormalTable {mso-style-name:"Table Normal"; mso-tstyle-rowband-size:0; mso-tstyle-colband-size:0; mso-style-noshow:yes; mso-style-parent:""; mso-padding-alt:0in 5.4pt 0in 5.4pt; mso-para-margin:0in; mso-para-margin-bottom:.0001pt; mso-pagination:widow-orphan; font-size:10.0pt; font-family:"Times New Roman"; mso-ansi-language:#0400; mso-fareast-language:#0400; mso-bidi-language:#0400;} Focusing mainly on a number of unpublished texts by Collingwood, especially his “Lectures on the Ontological Proof of the Existence of God,” the study examines the English philosopher’s innovative interpretation of the Anselm’s main contribution to the philosophical-theological tradition. Collingwood insightfully shows how the ontological argument can (...) be used in analyzing and discussing the religious experience, not in trying to formulate a logical proof of God’s existence. When abstracted from the individual’s practical religious life, that is, from the experience of prayer, worship, and the like, mind’s awareness of God cannot be understood. Resorting mainly to Anselm, Augustine, Thomas Aquinas, and Descartes, Collingwood argues that the externality of the Platonic absolute is that of an absolute transcendent whereas the Christian God is not only conceived as the transcendent cause of all things, but also as the immanent spirit in them. By asserting the unity of the mind—regarded as identical with its acts—this interpretation is meant to serve both as a means towards self-knowledge, and as a starting point for a future conceptual unification of religion and philosophy. (shrink)

We discuss the content and significance of John von Neumann’s quantum ergodic theorem (QET) of 1929, a strong result arising from the mere mathematical structure of quantum mechanics. The QET is a precise formulation of what we call normal typicality, i.e., the statement that, for typical large systems, every initial wave function ψ0 from an energy shell is “normal”: it evolves in such a way that |ψt ψt| is, for most t, macroscopically equivalent to the micro-canonical density matrix. (...) The QET has been mostly forgotten after it was criticized as a dynamically vacuous statement in several papers in the 1950s. However, we point out that this criticism does not apply to the actual QET, a correct statement of which does not appear in these papers, but to a different (indeed weaker) statement. Furthermore, we formulate a stronger statement of normal typicality, based on the observation that the bound on the deviations from the average specified by von Neumann is unnecessarily coarse and a much tighter (and more relevant) bound actually follows from his proof. (shrink)

The essay collection "Kant on Proofs for God's Existence" provides a highly needed, comprehensive analysis of the radical turns of Kant's views on proofs for God's existence.— In the "Theory of Heavens" (1755), Kant intends to harmonize the Newtonian laws of motion with a physico-theological argument for the existence of God. But only a few years later, in the "Ground of Proof" essay (1763), Kant defends an ontological ('possibility' or 'modal') argument on the basis of its logical exactitude while (...) he praises the physico-theological argument for its beauty and appeal to the common sense. In the first "Critique" (1781/7), Kant replaces traditional constitutive ontological, cosmological, and physico-theological proofs with his own regulative theoretical and moral-practical religious arguments. He continues to defend a moral argument in the second "Critique" (1788). But in the third "Critique" (1790), Kant reintroduces a physico-theological besides an ethicotheological argument in order to unify the critical system of philosophy. Kant develops further moral arguments and arguments from evil in the "Theodicy" essay (1791) and the "Religion" (1793/4), and still searches for the right kind of proof for God's existence in the "Opus postumum" (1796–1804).—Part one of this volume is dedicated to an analysis of Kant's proofs for God's existence in their historical order that explains which proofs Kant favors or rejects in various periods of his thought. Part two contains a systematic classification of main kinds of proof for God's existence in Kant that outlines the argumentative structure of particular kinds of proof and discusses Kant's potential reasons for their variations and modifications. The essay collection speaks to Kant specialists, philosophers, and theologians, but introduces the topic to non-academic readers also. -/- Contributers: Uygar Abaci (Pennsylvania State University), Craig Bacon (University of South Carolina), Andrew Chignell (Princeton University), Eckart Förster (Humboldt University, Johns Hopkins University), Ina Goy (Beijing Normal University) Paul Guyer (Brown University), Graham Oppy (Monash University), Lara Ostaric (Temple University), Stephen Palmquist (Independent Scholar), Lawrence Pasternack (Oklahoma State University), Konstantin Pollok (University of Mainz), Oliver Sensen (University of Tulane), Allen Wood (Bloomington University, Stanford University). (shrink)

Akama et al. [1] systematically studied an arithmetical hierarchy of the law of excluded middle and related principles in the context of first-order arithmetic. In that paper, they first provide a prenex normal form theorem as a justification of their semi-classical principles restricted to prenex formulas. However, there are some errors in their proof. In this paper, we provide a simple counterexample of their prenex normal form theorem [1, Theorem 2.7], then modify it in an appropriate way (...) which still serves to largely justify the arithmetical hierarchy. In addition, we characterize a variety of prenex normal form theorems by logical principles in the arithmetical hierarchy. The characterization results reveal that our prenex normal form theorems are optimal. For the characterization results, we establish a new conservation theorem on semi-classical arithmetic. The theorem generalizes a well-known fact that classical arithmetic is $\Pi _2$ -conservative over intuitionistic arithmetic. (shrink)

A notation for an ordinal using patterns of resemblance is based on choosing an isominimal set of ordinals containing the given ordinal. There are many choices for this set meaning that notations are far from unique. We establish that among all such isominimal sets there is one which is smallest under inclusion thus providing an appropriate notion of normal form notation in this context. In addition, we calculate the elements of this isominimal set using standard notations based on collapsing (...) functions. This provides a capstone to the results in [2, 6, 8, 9, 7], using further refinement of ordinal arithmetic developed in [8] which then both allows for a simple characterization of normal forms for patterns of order one and will play a key role in the arithmetical analysis of pure patterns of order two, [5]. (shrink)

We present some proof-theoretic results for the normal modal logic whose characteristic axiom is \. We present a sequent system for this logic and a hypersequent system for its first-order form and show that these are equivalent to Hilbert-style axiomatizations. We show that the question of validity for these logics reduces to that of classical tautologyhood and first-order logical truth, respectively. We close by proving equivalences with a Fitch-style proof system for revision theory.

The paper begins with a conceptual discussion of Michael Dummett's proof-theoretic justification of deduction or proof-theoretic semantics, which is based on what we might call Gentzen's thesis: 'the introductions constitute, so to speak, the "definitions" of the symbols concerned, and the eliminations are in the end only consequences thereof, which could be expressed thus: In the elimination of a symbol, the formula in question, whose outer symbol it concerns, may only "be used as that which it means on (...) the basis of the introduction of this symbol".' The intuitive philosophical content of Dummett's notions of harmony and stability is that harmony obtains if the grounds for asserting a proposition match the consequences of accepting it, and stability obtains if the converse also holds. Rules of inference define the meanings of a logical constant they govern if and only if they are stable. Gentzen observed that 'it should be possible to establish on the basis of certain requirements that the elimination rules are functions of the corresponding introduction rules.' One of the objectives of this paper is to specify such a function: I will specify a process by which it is possible to determine the elimination rules of logical constants from their introduction rules, and conversely, to determine the introduction rules from the elimination rules. I'll give the general forms of rules of inference and generalised reduction procedures for the normalisation of deduction. I'll give a formally precise characterisations of harmony and stability and show that deductions in logics that contain only constants governed by stable rules always normalise. (shrink)

We introduce an effective translation from proofs in the display calculus to proofs in the labelled calculus in the context of tense logics. We identify the labelled calculus proofs in the image of this translation as those built from labelled sequents whose underlying directed graph possesses certain properties. For the basic normal tense logic Kt, the image is shown to be the set of all proofs in the labelled calculus G3Kt.

This article presents modal versions of resource-conscious logics. We concentrate on extensions of variants of linear logic with one minimal non-normal modality. In earlier work, where we investigated agency in multi-agent systems, we have shown that the results scale up to logics with multiple non-minimal modalities. Here, we start with the language of propositional intuitionistic linear logic without the additive disjunction, to which we add a modality. We provide an interpretation of this language on a class of Kripke resource (...) models extended with a neighbourhood function: modal Kripke resource models. We propose a Hilbert-style axiomatisation and a Gentzen-style sequent calculus. We show that the proof theories are sound and complete with respect to the class of modal Kripke resource models. We show that the sequent calculus admits cut elimination and that proof-search is in PSPACE. We then show how to extend the results when non-commutative connectives are added to the language. Finally, we put the l.. (shrink)

A normalization procedure is given for classical natural deduction with the standard rule of indirect proof applied to arbitrary formulas. For normal derivability and the subformula property, it is sufficient to permute down instances of indirect proof whenever they have been used for concluding a major premiss of an elimination rule. The result applies even to natural deduction for classical modal logic.

This volume examines the notion of an analytic proof as a natural deduction, suggesting that the proof's value may be understood as its normal form--a concept with significant implications to proof-theoretic semantics.

The system of natural deduction that originated with Gentzen , and for which Prawitz proved a normalization theorem, is re-cast so that all elimination rules are in parallel form. This enables one to prove a very exigent normalization theorem. The normal forms that it provides have all disjunction-eliminations as low as possible, and have no major premisses for eliminations standing as conclusions of any rules. Normal natural deductions are isomorphic to cut-free, weakening-free sequent proofs. This form of normalization (...) theorem renders unnecessary Gentzen's resort to sequent calculi in order to establish the desired metalogical properties of his logical system.Ultimate normal forms are well-adapted to the needs of the computational logician, affording valuable constraints on proof-search. They also provide an analysis of deductive relevance. There is a deep isomorphism between natural deductions and sequent proofs in the relevantized system. (shrink)

The original decision criterion and method of the combined calculus, presented by D. Hilbert and W. Ackermann, and applied by later logicians, are illuminating, but also go seriously awry and lead the universality and preciseness of the combined calculus to be damaged. The main error is that they confuse the two levels of the combined calculus in the course of calculating. This paper aims to resolve the problem through dividing the levels of the combined calculus, introducing a mixed operation mode, (...) and therefore finding a normal-form decision method approximated by that in sentential logic. Finally, this paper provides a more precise proof of Hauber’s theorem by using the normal-form decision method of the combined calculus. (shrink)

A proof-theoretic test for paradoxicality was famously proposed by Tennant: a paradox must yield a closed derivation of absurdity with no normal form. Drawing on the remark that all derivations of a given proposition can be transformed into derivations in normal form of a logically equivalent proposition, we investigate the possibility of paradoxes in normal form. We compare paradoxes à la Tennant and paradoxes in normal form from the viewpoint of the computational interpretation of proofs (...) and from the viewpoint of proof-theoretic semantics. (shrink)

In our previous work we proved the conjecture NP = PSPACE by advanced proof theoretic methods that combined Hudelmaier’s cut-free sequent calculus for minimal logic with the horizontal compressing in the corresponding minimal Prawitz-style natural deduction. In this Addendum we show how to prove a weaker result NP = coNP without referring to HSC. The underlying idea is to omit full minimal logic and compress only “naive” normal tree-like ND refutations of the existence of Hamiltonian cycles in given (...) non-Hamiltonian graphs, since the Hamiltonian graph problem in NPcomplete. Thus, loosely speaking, the proof of NP = coNP can be obtained by HSC-elimination from our proof of NP = PSPACE. (shrink)

Montague [7] translates English into a tensed intensional logic, an extension of the typed -calculus. We prove that each translation reduces to a formula without -applications, unique to within change of bound variable. The proof has two main steps. We first prove that translations of English phrases have the special property that arguments to functions are modally closed. We then show that formulas in which arguments are modally closed have a unique fully reduced -normal form. As a corollary, (...) translations of English phrases are contained in a simply defined proper subclass of the formulas of the intensional logic. (shrink)

Herbrand’s theorem is one of the most fundamental results about first-order logic. In the context of proof analysis, Herbrand-disjunctions are used for describing the constructive content of cut-free proofs. However, given a proof with cuts, the computation of a Herbrand-disjunction is of significant computational complexity, as the cuts in the proof have to be eliminated first.In this paper we prove a generalization of Herbrand’s theorem: From a proof with cuts, one can read off a small tautology (...) composed of instances of the end-sequent and the cut formulas. This tautology describes the proof in the following way: Each cut induces a formula stating that a disjunction of instances of the cut formula implies a conjunction of instances of the cut formula. All these cut-implications together then imply the already existing instances of the end-sequent. The proof that this formula is a tautology is carried out by transforming the instances in the proof to normal forms and using characteristic clause sets to relate them. These clause sets have first been studied in the context of cut-elimination.This extended Herbrand theorem is then applied to cut-elimination sequences in order to show that, for the computation of an Herbrand-disjunction, the knowledge of only the term substitutions performed during cut-elimination is already sufficient. (shrink)

We describe a short model-theoretic proof of an extended normal form theorem for derivations in predicate logic which implies in PRA a normal form theorem for the arithmetic derivations . Consider the Gentzen-type formulation of predicate logic with invertible rules. A derivation with proper variables is one where a variable b can occur in the premiss of an inference L but not below this premiss only in the case when L is () or () and b is (...) its eigenvariable. Free variables of such derivation are eigenvariables and free variables of its last sequent. Then any sequent derivable in predicate logic has a cut-free derivation with proper variables where the main formula of any antecedent rule is underivable. The proof is by a simple modification of the construction of a countermodel of the formula from the open branch of its canonical proof-search tree. It extends to intuitionistic and higher order systems. The proof of the corresponding normalization theorem outlined in [8] uses the passage to the infinitary derivations enriched by finitary derivations. The normal form after a modification to make it decidable can be considered as a realization of Gentzen's idea stated at the end of [2], that his notion of reduction for arithmetic can be extended to other fields of mathematics. (shrink)

We start with a simple proof of Leivant's normal form theorem for ∑11 formulas over finite successor structures. Then we use that normal form to prove the following:1. over all finite structures, every ∑21 formula is equivalent to a ∑21 formula whose first-order part is a Boolean combination of existential formulas, and2. over finite successor structures, the Kolaitis-Thakur hierarchy of minimization problems collapses completely and the Kolaitis-Thakur hierarchy of maximization problems collapses partially.The normal form theorem for (...) ∑21 fails if ∑21 is replaced with ∑11 or if infinite structures are allowed. (shrink)