Proof Theory

This paper surveys the common approach to quantification and generalised quantification in formal linguistics and philosophy of language. We point out how this general setting departs from empirical linguistic data, and give some hints for a different view based on proof theory, which on many aspects gets closer to the language itself. We stress the importance of Hilbert's oper- ator epsilon and tau for, respectively, existential and universal quantifications. Indeed, these operators help a lot to construct semantic representation close to (...) natural language, in particular with quantified noun phrases as individual terms. We also define guidelines for the design of the proof rules corresponding to generalised quantifiers. (shrink)

Reverse mathematics studies which subsystems of second order arithmetic are equivalent to key theorems of ordinary, non-set-theoretic mathematics. The main philosophical application of reverse mathematics proposed thus far is foundational analysis, which explores the limits of different foundations for mathematics in a formally precise manner. This paper gives a detailed account of the motivations and methodology of foundational analysis, which have heretofore been largely left implicit in the practice. It then shows how this account can be fruitfully applied in the (...) evaluation of major foundational approaches by a careful examination of two case studies: a partial realization of Hilbert’s program due to Simpson [1988], and predicativism in the extended form due to Feferman and Schütte. -/- Shore [2010, 2013] proposes that equivalences in reverse mathematics be proved in the same way as inequivalences, namely by considering only omega-models of the systems in question. Shore refers to this approach as computational reverse mathematics. This paper shows that despite some attractive features, computational reverse mathematics is inappropriate for foundational analysis, for two major reasons. Firstly, the computable entailment relation employed in computational reverse mathematics does not preserve justification for the foundational programs above. Secondly, computable entailment is a Pi-1-1 complete relation, and hence employing it commits one to theoretical resources which outstrip those available within any foundational approach that is proof-theoretically weaker than Pi-1-1-CA0. (shrink)

While non-classical theories of truth that take truth to be transparent have some obvious advantages over any classical theory that evidently must take it as non-transparent, several authors have recently argued that there's also a big disadvantage of non-classical theories as compared to their “external” classical counterparts: proof-theoretic strength. While conceding the relevance of this, the paper argues that there is a natural way to beef up extant internal theories so as to remove their proof-theoretic disadvantage. It is suggested that (...) the resulting internal theories should seem preferable to their external counterparts. (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)

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)

This paper explores an alternative non-relational semantics for modal logic, framing modal systems as "poly-logics"—intersections of simpler, foundational logics. Building on pioneering work by J. Kearns and subsequent developments, we demonstrate how established systems such as K series (K, K4, K5, K45), KD series (KD, KD4, KD5, KD45), KB series (KDB, KB, KB4, KB5, KB45) emerge as intersections of logics like KT, KTB, FN, TR, and their extensions. Utilizing Resolution Matrix Semantics (RMS), we establish soundness and completeness for key systems (...) with sketched proofs and introduce an innovative tableau-based proof procedure tailored to RMS. This approach not only unifies disparate modal frameworks but also yields efficient algorithmic tools for validity checking, offering fresh insights into the algebraic structure of modal deduction. Examples illustrate the method's efficacy, highlighting its advantages over traditional Kripke-style model checking. (shrink)

This paper describes a decision procedure for disjunctions of conjunctions of anti-prenex normal forms of pure first-order logic (FOLDNFs) that do not contain V within the scope of quantifiers. The disjuncts of these FOLDNFs are equivalent to prenex normal forms whose quantifier-free parts are conjunctions of atomic and negated atomic formulae (= Herbrand formulae). In contrast to the usual algorithms for Herbrand formulae, neither skolemization nor unification algorithms with function symbols are applied. Instead, a procedure is described that rests on (...) nothing but equivalence transformations within pure first-order logic (FOL). This procedure involves the application of a calculus for negative normal forms (the NNF-calculus) with A -||- A & A (= &I) as the sole rule that increases the complexity of given FOLDNFs. The described algorithm illustrates how, in the case of Herbrand formulae, decision problems can be solved through a systematic search for proofs that reduce the number of applications of the rule &I to a minimum in the NNF-calculus. In the case of Herbrand formulae, it is even possible to entirely abstain from applying &I. Finally, it is shown how the described procedure can be used within an optimized general search for proofs of contradiction and what kind of questions arise for a &I-minimal proof strategy in the case of a general search for proofs of contradiction. (shrink)

The paper studies a cluster of systems for fully disquotational truth based on the restriction of initial sequents. Unlike well-known alternative approaches, such systems display both a simple and intuitive model theory and remarkable proof-theoretic properties. We start by showing that, due to a strong form of invertibility of the truth rules, cut is eliminable in the systems via a standard strategy supplemented by a suitable measure of the number of applications of truth rules to formulas in derivations. Next, we (...) notice that cut remains eliminable when suitable arithmetical axioms are added to the system. Finally, we establish a direct link between cut-free derivability in infinitary formulations of the systems considered and fixed-point semantics. Noticeably, unlike what happens with other background logics, such links are established without imposing any restriction to the premisses of the truth rules. (shrink)

This paper considers Rumfitt’s bilateral classical logic (BCL), which is proposed to counter Dummett’s challenge to classical logic. First, agreeing with several authors, we argue that Rumfitt’s notion of harmony, used to justify logical rules by a purely proof theoretical manner, is not sufficient to justify coordination rules in BCL purely proof-theoretically. For the central part of this paper, we propose a notion of proof-theoretical validity similar to Prawitz for BCL and proves that BCL is sound and complete respect to (...) this notion of validity. The major difficulty in defining validity for BCL is that validity of positive +A appears to depend on negative −A, and vice versa. Thus, the straightforward inductive definition does not work because of this circular dependance. However, Knaster-Tarski’s fixed point theorem can resolve this circularity. Finally, we discuss the philosophical relevance of our work, in particular, the impact of the use of fixed point theorem and the issue of decidability. (shrink)

When modeling informal proofs like that of Euclid’s Elements using a sound logical system, we go from proofs seen as somewhat unrigorous – even having gaps to be filled – to rigorous proofs. However, metalogic grounds the soundness of our logical system, and proofs in metalogic are not like formal proofs and look suspiciously like the informal proofs. This brings about what I am calling here the groundedness problem: how can we decide with certainty that our metalogical proofs are rigorous (...) and sustain our logical system? In this paper, I will expose this problem. I will not try to solve it here. (shrink)

We investigate involutive commutative residuated lattices without unit, which are commutative residuated lattice-ordered semigroups enriched with a unary involutive negation operator. The logic of this structure is discussed and the Genzten-style sequent calculus of it is presented. Moreover, we prove the decidability of this logic.

To appear in the Proceedings of Logic Colloquium 2006. (32 pages).

As part of a broader family of logics, [2, 4] introduced two key logical systems: $$\mathsf {iK_d}$$, which encapsulates the basic logical structure of dynamic topological systems, and $$\mathsf {iK_{d*}}$$, which provides a well-behaved yet sufficiently general framework for an abstract notion of implication. These logics have been thoroughly examined through their algebraic, Kripke-style, and topological semantics. To complement these investigations with their missing proof-theoretic analysis, this paper introduces a cut-free G3-style sequent calculus for $$\mathsf {iK_d}$$ and $$\mathsf {iK_{d*}}$$. Using (...) these systems, we prove that they satisfy the disjunction property and, more broadly, admit a generalization of Visser’s rules. Additionally, we establish that $$\mathsf {iK_d}$$ enjoys the Craig interpolation property and that its sequent system possesses the deductive interpolation property. (shrink)

In this paper we provide a proof theoretical investigation of logical argumentation, where arguments are represented by sequents, conflicts between arguments are represented by sequent elimination rules, and deductions are made by dynamic proof systems extending standard sequent calculi. The idea is to imitate argumentative movements in which certain claims are introduced or withdrawn in the presence of counter-claims. This is done by a dynamic evaluation of sequences of sequents, in which the latter are considered ‘derived’ or ‘not derived’ according (...) to the content of the sequence. We show that decisive conclusions of such a process correspond to well-accepted consequences of the underlying argumentation framework. The outcome is therefore a general and modular proof-theoretical approach for paraconsistent and non-monotonic reasoning with argumentation systems. (shrink)

A bilateralist take on proof-theoretic semantics can be understood as demanding of a proof system to display not only rules giving the connectives’ provability conditions but also their refutability conditions. On such a view, then, a system with two derivability relations is obtained, which can be quite naturally expressed in a proof system of natural deduction but which faces obstacles in a sequent calculus representation. Since in a sequent calculus there are two derivability relations inherent, one expressed by the sequent (...) sign and one by the horizontal lines holding _between sequents_, in a truly bilateral calculus both need to be dualized. While dualizing the sequent sign is rather straightforwardly corresponding to dualizing the horizontal lines in natural deduction, dualizing the horizontal lines in sequent calculus, uncovers problems that, as will be argued in this paper, shed light on deeper conceptual issues concerning an imbalance between the notions of proof vs. refutation. The roots of this problem will be further analyzed and possible solutions on how to retain a bilaterally desired balance in our system are presented. (shrink)

μ $\mu $ mu -Abstract Elementary Classes are a model theoretic framework introduced in [4] to encompass classes axiomatized by L ∞, ∞ $\mathbb {L}_{\infty, \infty }$ double struck upper L Subscript infinity comma infinity. We show that the framework extends beyond these logics by showing classes axiomatized in L ( a a ) $\mathbb {L}(aa)$ double struck upper L left parenthesis a a right parenthesis with just the a a $aa$ a a quantifier are an ℵ 1 $\aleph _1$ (...) normal first transfinite cardinal 1 -Abstract Elementary Class. (shrink)

This paper clarifies, revises, and extends the account of the transmission of truthmakers by core proofs that was set out in chap. 9 of Tennant. Brauer provided two kinds of example making clear the need for this. Unlike Brouwer’s counterexamples to excluded middle, the examples of Brauer that we are dealing with here establish the need for appeals to excluded middle when applying, to the problem of truthmaker-transmission, the already classical metalinguistic theory of model-relative evaluations.

The notion of reduced sequents plays an important role in proving the decidability of some sequent calculi. A reduced sequent is a sequent without repetitive substructures. While it is straightforward to obtain reduced sequents in Gentzen-style calculi, it is unclear how to obtain them algorithmically in modal display calculi, because modal display calculi contain more complex structures in sequents so that repetitive substructures cannot be recognized at first sight. This paper provides an algorithm to count minimal repetitive substructures in a (...) sequent and to obtain reduced sequents and shows that reduced sequents obtained from a sequent are ‘equivalent’ in a certain sense. Moreover, the paper discusses a proposal for proving the decidability of a modal display calculus and analyzes the reasons why it does not work. The algorithm and proposal may serve as a stepping stone for analyzing calculi with complex structures in sequents and proving their decidability. (shrink)

The notion of $$(\varOmega, \varepsilon )$$-inductive sequents plays an important role in correspondence theory and proof theory. This paper simplifies the definition of $$(\varOmega, \varepsilon )$$-inductive sequents for distributive modal logic by ‘internalizing’ the dependency order $$.

This paper investigates the logic of compatibility as a ground for the logic of conditionals. We identify a family of principles expressing key properties of compatibility, which can be coherently ordered. Assuming that conditionals are definable in terms of incompatibility — the negation of compatibility — each of the principles identified yields corresponding principles governing conditionals. Clarifying these derivability relations provides a new perspective on several existing accounts of conditionals.

This paper investigates the proof theory of contra-classical logics, with a focus on Heinrich Wansing’s constructive connexive logic C. Drawing on Wansing’s semantic ‘bilateral’ framework – which characterizes connectives in terms of ‘support of truth’ and ‘support of falsity’ – we introduce a bilateral labeled sequent calculus incorporating specific ‘verification’ and ‘falsification’ rules. The resulting calculus is shown to exhibit key structural properties: all logical rules are height-preserving invertible, all structural rules are height-preserving admissible, and the cut rule is admissible. (...) Moreover, the system, proven to be both sound and complete, allows for terminating proof search and the extraction of countermodels from failed root-first proof search. Finally, the computational complexity of the resulting decision procedure is established. The paper concludes with some observations on systems related to C, such as C3 and N4, and outlines potential directions for future work. (shrink)

In this paper, we investigate the proof theory of a modal expansion of intuitionistic propositional logic obtained by adding an 'actuality' operator among the connectives. This logic was initially considered by L. Humberstone, and, more recently, also by S. Niki and H. Omori to present a possible application of intuitionism to empirical discourse. Niki and Omori's idea to consider the notion of actuality based on intuitionistic logic was presented, among other things, using Gentzen sequents. Unfortunately, their proof system is not (...) cut-free. In this paper, we define another proof system for Niki and Omori’s logic, namely a hypersequent calculus, and present a proof of cut-elimination for it. (shrink)

The past decades have seen remarkable progress in the study of substructural logics, be it mathematically or philosophically oriented. This progress has a somewhat perplexing effect: the more subst...

In proof-theoretic semantics, meaning is based on inference. It may seen as the mathematical expression of the inferentialist interpretation of logic. Much recent work has focused on base-extension semantics, in which the validity of formulas is given by an inductive definition generated by provability in a ‘base’ of atomic rules. Base-extension semantics for classical and intuitionistic propositional logic have been explored by several authors. In this paper, we develop base-extension semantics for the classical propositional modal systems |$K$|⁠, |$KT$|⁠, |$K4$| and (...) |$S4$|⁠, with |$\square $| as the primary modal operator. We establish appropriate soundness and completeness theorems and establish the duality between |$\square $| and a natural presentation of |$\lozenge $|⁠. We also show that our semantics is in its current form not complete with respect to euclidean modal logics. Our formulation makes essential use of relational structures on bases. (shrink)

The paper “Tautology elimination, cut elimination, and S5” published in this journal presents a novel method for establishing by proof analysis the admissibility of the rule of tautology elimination for certain sequent calculi. Since tautology elimination will typically imply the admissibility of cut, the method promises a new path to show the admissibility of cut for cut-free calculi on which the standard techniques within structural proof theory seem inapplicable. This paper shows that the method as presented involves an error.

Natural deduction inference rules seem to reflect the way we actually reason. Hence, many if not most inferentialist theories maintain that meaning is conferred on linguistic expressions by natural deduction rules, rather than the more abstract alternative of sequent rules. In the present paper, I argue, to the contrary, that an inferentialist theory of meaning must take a somewhat metainferential form, whereby the meanings of linguistic expressions—in particular, the logical constants—are conferred by sequent rules, conceived of as licensing inferences between (...) inferences. To that end, I propose that sequent rules are to be understood as inferential semantic clauses, i.e., as playing a role analogous to that of the semantic clauses in truth conditional theories of meaning. I establish this proposal on the basis of an argument to the effect that inferentialists must adopt an extended version of Frege's context principle, according to which only within a complete sentence potentially serving either as a premise or as a conclusion of an inference do words have meaning. The resultant inferentialist theory is not disconnected from the way we actually reason. Moreover, on its basis one can make a meaning-theoretic case for rather unintuitive features of many sequent calculi, such as multiple conclusions and various ways of going substructural. (shrink)

We encode Belnap’s basic theory of display calculi in the proof assistant Coq/Rocq version 8.18.0 and formalise the proof that Belnap’s conditions C2–C8 imply the cut-elimination theorem. Our framework allows us to formally prove meta-theoretic results such as Hilbert-completeness and derivability of explicit rules, such as cut, but also others if required. What makes our formalisation powerful is that it works entirely with an abstraction that can be instantiated to many possible logics and display calculi, although we make no attempt (...) to precisely characterise the logics that can be properly displayed in our formalisation. For this reason, our work can be seen as a formalisation of a display calculus framework and a cut-elimination theorem for a wide range of display calculi. As examples, we apply our work to classical propositional logic (CPL), tense logic (Kt), and non-commutative non-associative Lambek calculus to obtain complete display calculi as well as formally proved cut-elimination theorems, but we believe our formalisation to be also applicable to many others. We also encoded a proof of the decidability of CPL that relies only on the structure of proofs within an additive display calculus for CPL. To our knowledge, our work is the first formalisation of a decidability result in display calculus. Moreover, all of our formal proofs are constructive as they never require the addition of the law of excluded middle in Coq’s environment (which is constructive by default), which means we were also able to extract computer programs from our proof of cut-elimination able to convert CPL/Kt/Lambek derivation trees into cut-free ones. As formal proofs are known to be significantly longer to write than usual pen-and-paper proofs, our work led to the development of a multitude of files of Coq code comprising more than 15,000 lines. (shrink)

This paper introduces a $$\textsf{G3}$$ G 3 -style sound and complete sequent calculus for the Russellian approach to definite description presented by Indrzejczak and some co-authors in previous works. We show that the calculi introduced have the good structural properties that are distinctive of $$\textsf{G3}$$ G 3 -style calculi: weakening and contraction are height-preserving admissible, all rules are height-preserving invertible, and cut is admissible. Having all rules invertible, the calculus allows to extract a countermodel from a failed proof search. Moreover, (...) we use the calculus to give a Maehara-style constructive proof of Craig Interpolation Property. Finally, we extend the approach to intuitionistic logic. (shrink)

A Gentzen-style sequent calculus, GA4, for a first-order extension of Avron’s self-extensional paradefinite four-valued logic is introduced. Avron’s logic is known as a unique self-extensional extension of Belnap–Dunn logic. GA4 yields two new Gentzen-style sequent calculi, $$\hbox {GCL}_1$$ and $$\hbox {GCL}_2$$, for first-order classical logic by introducing some new inference rules or initial sequents. $$\hbox {GCL}_1$$ is obtained from GA4 by adding the rules of explosion and excluded middle, which correspond to the principle of explosion and the law of excluded (...) middle. $$\hbox {GCL}_2$$ is obtained from GA4 by adding initial sequents that correspond to the same principle and law. A theorem proving the equivalence among $$\hbox {GCL}_1$$, $$\hbox {GCL}_2$$, and Gentzen’s sequent calculus LK for first-order classical logic is established. The cut-elimination, contraposition-elimination, and completeness theorems for GA4, $$\hbox {GCL}_1$$, and $$\hbox {GCL}_2$$ are proved. The self-extensional properties of GA4, $$\hbox {GCL}_1$$, and $$\hbox {GCL}_2$$ are derived using the contraposition-elimination theorems. (shrink)

Gentzen-style sequent calculi and Gentzen-style natural deduction systems are introduced for a family (C-family) of connexive logics over Wansing’s basic constructive connexive logic C. The C-family is derived from C by incorporating Peirce’s law, the law of excluded middle, and the generalized law of excluded middle. Natural deduction systems with general elimination rules are also introduced for the C-family. Theorems establishing the equivalence between the proposed sequent calculi and natural deduction systems are demonstrated. Cutelimination and normalization theorems are established for (...) the proposed sequent calculi and natural deduction systems, respectively. Additionally, similar results are obtained for a family (N-family) of paraconsistent logics over Nelson’s constructive four-valued logic N4. (shrink)

First, G0-style sequent calculi for extended Belnap–Dunn and intuitionistic logics, including Nelson and Gurevich logics, are introduced. A theorem establishing the equivalence between G0- and G3-style sequent calculi for these logics is then presented, and the cut-elimination theorem for these G0-style calculi is obtained as a result. Next, natural deduction systems with general elimination rules are introduced for these logics, and a full normalization theorem for these natural deduction systems is proved. This proof is achieved using bi-directional translations between the (...) proposed G0-style sequent calculi and the natural deduction systems with general elimination rules. (shrink)

This paper proves normalisation theorems for intuitionist and classical positive free logic, without and with the iota operator for definite descriptions `the F'. Positive free logic also opens a number of options for rules for iota. In total, six different formalisations of theories of definite descriptions will be discussed, three proposed by Lambert, and three alternatives. The latter are motivated by considerations relating to proof-theoretic harmony between introduction and elimination rules. The philosophical importance of the various systems and results is (...) indicated. The paper builds on Kürbis (2025), but is largely self-contained. The proofs for the present systems are easier than those for negative free logic. (shrink)

The paper provides a cut-free sequent calculus for the theory of tight apartness in a language where both apartness and equality are primitive notions. The result is obtained by aptly modifying the underlying logical calculus for intuitionistic logic and adding rules of inference corresponding to the axioms of apartness and the principles governing the mutual deductive relationships between apartness and equality. While the rules for apartness are found directly from the axioms by applying standard proof-theoretic methods, the others, especially the (...) rule corresponding to the principle of tight apartness, are found by exploiting the logical law of _consequentia mirabilis_. Along the way, we also provide a cut-free sequent calculus for the theory of weak tight apartness, also known as the theory of negated equality, thus answering in the positive to an open problem in the existing literature on the subject. (shrink)

In this paper we show how to extend the standard cut-elimination procedure from first-order intuitionistic stable logic to a class of intuitionistic stable theories. Building on previous works by Negri and von Plato, we aptly modify the underlying calculus for first-order intuitionistic logic so as to preserve the admissibility of all the structural rules, including cut, in the presence of a restricted version of the rule of classical reductio ad absurdum and of a special case of universal rules.

It is an unusual property for a logic to prove a formula and its negation without ending up in triviality. Some systems have nonetheless been observed to satisfy this property: one group of such non-trivial negation inconsistent logics has its archetype in H. Wansing’s constructive connexive logic, whose negation-implication fragment already proves contradictions. N. Francez and Y. Weiss subsequently investigated relevant subsystems of this fragment, and Weiss in particular showed that they remain negation inconsistent. In this note, we take a (...) closer look at this phenomenon in the systems of Francez and Weiss, and point out two types of necessary conditions, one proof-theoretic and one relevant, which any contradictory formula must satisfy. As a consequence, we propose a nine-fold classification of provable contradictions for the logics. (shrink)

We show that the replacement rule of the sequent calculi ${\bf G3[mic]}^= $ in [8] can be replaced by the simpler rule in which one of the principal formulae is not repeated in the premiss.

This paper introduces nested sequent calculi for modal logics that include non-standard modalities as primitive operators in their languages. By non-standard modalities, we mean non-contingency, contingency, essence, accident, impossibility, and unnecessity. We consider basic normal modal logic K and its serial, reflexive, transitive, and symmetric extensions. Our research begins by using Poggiolesi’s nested sequent calculi as a foundation. These calculi are specifically designed for logics that are formulated in a language that includes the necessity operator. Next, we proceed to modify (...) their rules to accommodate non-standard modalities. We then establish the soundness and completeness of the resulting calculi. As a consequence, we get that the nested sequent calculus for K is cut-free. Subsequently, we provide a constructive cut admissibility proof for K. Finally, we discuss the issues pertaining to the cut admissibility for the extensions of K and their relationships with the so-called special structural rules as well as the potential for considering other forms of non-standard modalities. (shrink)

summary of work in relevant in the Anderson– tradition.]; Mares Troestra, Anne, 1992, Lectures on , CSLI Publications [A quick, easy-to.

In his seminal 1931 paper, Gödel had shown the existence of finitary statements that required infinitary resources to prove them. This led him to postulate that the unlimited transfinite iteration of the power-set operation is necessary to account for finitary mathematics (Gödel's Doctrine; GD). GD garnered support over the course of the 20th century because of the production of other finitary independence results (Paris-Harrington theorem, etc.). In order to counter the platonistic assumptions taken to be implicit in GD, Solomon Feferman (...) challenged the significance of these independence results on the following grounds: (i) they are "artificial"; (ii) their proofs do not ultimately require infinitary set-existence principles but only the weaker 1-consistency of such principles; (iii) the technique of "proof-theoretic reduction" shows that these finitary results can be proved using weaker resources than was initially thought. Although his technical results are unimpeachable, I argue that Feferman's case against GD is overstated. First, via a detailed examination of particular independence results, I show that these should be construed as reasonably "mathematical" given their fruitfulness in mathematical practice. Second, I argue that, when we weigh Feferman's anti-platonist programme against its epistemic costs, his objections (ii) and (iii) are much less compelling. In particular, Feferman's proposals leave us with (a) less than satisfactory proofs of individual results; and (b) a less than satisfactory account of the interplay between metamathematics and mathematics, viz., a loss of global explanatory structure. That is, the higher infinite plays both a significant verificational role and a significant explanatory role in proving results about the finite. Thus, I provide a reassessment and partial vindication of an epistemic version of GD. I conclude by sketching a proposal for how this epistemic version of GD might be used to provide a novel argument for a form of mathematical platonism. (shrink)