The Problem of Consistency

2017 ◽  
Author(s):  
Jan von Plato
Keyword(s):  
Consistency Problem ◽  
Classical Arithmetic ◽  
Intuitionistic Arithmetic

This chapter talks about how the translations from classical to intuistic arithmetic that Gödel and Gentzen found in 1932–33 showed that the consistency of classical arithmetic reduces to that of intuitionistic arithmetic. The main aim of Hilbert's program in the 1920s had been to show that the infinitistic component of arithmetic, namely the use of quantificational inferences in indirect proofs, does not lead to contradiction. It followed from Gödel's and Gentzen's result that these classical steps are harmless. Therefore, the consistency problem of arithmetic has an intuitionistic sense and, consequently, possibly also an intuitionistic solution. Bernays was quick to point out that intuitionism transcends the boundaries of strictly finitary reasoning.

scholarly journals Implicational complexity in intuitionistic arithmetic

1981 ◽  
Vol 46 (2) ◽  
pp. 240-248 ◽  
Author(s):  
Daniel Leivant
Keyword(s):  
Normal Form ◽  
Form Theorem ◽  
Natural Measure ◽  
Normal Form Theorem ◽  
Propositional Constants ◽  
Image Position ◽  
Classical Arithmetic ◽  
Intuitionistic Arithmetic

In classical arithmetic a natural measure for the complexity of relations is provided by the number of quantifier alternations in an equivalent prenex normal form. However, the proof of the Prenex Normal Form Theorem uses the following intuitionistically invalid rules for permuting quantifiers with propositional constants.Each one of these schemas, when added to Intuitionistic (Heyting's) Arithmetic IA, generates full Classical (Peano's) Arithmetic. Schema (3) is of little interest here, since one can obtain a formula intuitionistically equivalent to A ∨ ∀xBx, which is prenex if A and B are:For the two conjuncts on the r.h.s. (1) may be successively applied, since y = 0 is decidable.We shall readily verify that there is no way of similarly going around (1) or (2). This fact calls for counting implication (though not conjunction or disjunction) in measuring in IA the complexity of arithmetic relations. The natural implicational measure for our purpose is the depth of negative nestings of implication, defined as follows. I(F): = 0 if F is atomic; I(F ∧ G) = I(F ∨ G): = max[I(F), I(G)]; I(∀xF) = I(∃xF): = I(F); I(F → G):= max[I(F) + 1, I(G)].

Epistemic arithmetic is a conservative extension of intuitionistic arithmetic

1984 ◽  
Vol 49 (1) ◽  
pp. 192-203 ◽  
Author(s):  
Nicolas D. Goodman
Keyword(s):  
Propositional Calculus ◽  
Cut Elimination ◽  
Conservative Extension ◽  
First Order ◽  
Classical Mathematics ◽  
Order Arithmetic ◽  
Classical Propositional Calculus ◽  
Epistemic Arithmetic ◽  
Classical Arithmetic ◽  
Intuitionistic Arithmetic

Questions about the constructive or effective character of particular arguments arise in several areas of classical mathematics, such as in the theory of recursive functions and in numerical analysis. Some philosophers have advocated Lewis's S4 as the proper logic in which to formalize such epistemic notions. (The fundamental work on this is Hintikka [4].) Recently there have been studies of mathematical theories formalized with S4 as the underlying logic so that these epistemic notions can be expressed. (See Shapiro [7], Myhill [5], and Goodman [2]. The motivation for this work is discussed in Goodman [3].) The present paper is a contribution to the study of the simplest of these theories, namely first-order arithmetic as formalized in S4. Following Shapiro, we call this theory epistemic arithmetic (EA). More specifically, we show that EA is a conservative extension of Hey ting's arithmetic HA (ordinary first-order intuitionistic arithmetic). The question of whether EA is conservative over HA was raised but left open in Shapiro [7].The idea of our proof is as follows. We interpret EA in an infinitary propositional S4, pretty much as Tait, for example, interprets classical arithmetic in his infinitary classical propositional calculus in [8]. We then prove a cut-elimination theorem for this infinitary propositional S4. A suitable version of the cut-elimination theorem can be formalized in HA. For cut-free infinitary proofs, there is a reflection principle provable in HA. That is, we can prove in HA that if there is a cut-free proof of the interpretation of a sentence ϕ then ϕ is true. Combining these results shows that if the interpretation of ϕ is provable in EA, then ϕ is provable in HA.

Arithmetic Certainty

2015 ◽  
Author(s):  
José Ferreirós
Keyword(s):  
Number Theory ◽  
Model Theory ◽  
Algebraic Number ◽  
Analytic Number Theory ◽  
Algebraic Number Theory ◽  
Elementary Number Theory ◽  
Arithmetical Knowledge ◽  
Classical Arithmetic ◽  
Similar Claim ◽  
Intuitionistic Arithmetic

This chapter considers the idea that we have certainty in our basic arithmetic knowledge. The claim that arithmetical knowledge enjoys certainty cannot be extended to a similar claim about number theory “as a whole.” It is thus necessary to distinguish between elementary number theory and other, more advanced, levels in the study of numbers: algebraic number theory, analytic number theory, and perhaps set-theoretic number theory. The chapter begins by arguing that the axioms of Peano Arithmetic are true of counting numbers and describing some elements found in counting practices. It then offers an account of basic arithmetic and its certainty before discussing a model theory of arithmetic and the logic of mathematics. Finally, it asks whether elementary arithmetic, built on top of the practice of counting, should be classical arithmetic or intuitionistic arithmetic.

Relativized realizability in intuitionistic arithmetic of all finite types

1978 ◽  
Vol 43 (1) ◽  
pp. 23-44 ◽  
Author(s):  
Nicolas D. Goodman
Keyword(s):  
Extension Theorem ◽  
General Notion ◽  
Conservative Extension ◽  
First Order ◽  
New Information ◽  
Reflection Theorem ◽  
Order Arithmetic ◽  
Special Case ◽  
Dependent Choice ◽  
Intuitionistic Arithmetic

In this paper we introduce a new notion of realizability for intuitionistic arithmetic in all finite types. The notion seems to us to capture some of the intuition underlying both the recursive realizability of Kjeene [5] and the semantics of Kripke [7]. After some preliminaries of a syntactic and recursion-theoretic character in §1, we motivate and define our notion of realizability in §2. In §3 we prove a soundness theorem, and in §4 we apply that theorem to obtain new information about provability in some extensions of intuitionistic arithmetic in all finite types. In §5 we consider a special case of our general notion and prove a kind of reflection theorem for it. Finally, in §6, we consider a formalized version of our realizability notion and use it to give a new proof of the conservative extension theorem discussed in Goodman and Myhill [4] and proved in our [3]. (Apparently, a form of this result is also proved in Mine [13]. We have not seen this paper, but are relying on [12].) As a corollary, we obtain the following somewhat strengthened result: Let Σ be any extension of first-order intuitionistic arithmetic (HA) formalized in the language of HA. Let Σω be the theory obtained from Σ by adding functionals of finite type with intuitionistic logic, intensional identity, and axioms of choice and dependent choice at all types. Then Σω is a conservative extension of Σ. An interesting example of this theorem is obtained by taking Σ to be classical first-order arithmetic.

scholarly journals Formalism and Hilbert’s understanding of consistency problems

2021 ◽  
Author(s):  
Michael Detlefsen
Keyword(s):  
Philosophy Of Mathematics ◽  
Model Construction ◽  
Traditional Model ◽  
Consistency Proof ◽  
Salient Points ◽  
Consistency Problem ◽  
Late Nineteenth ◽  
Similarity And Difference ◽  
Traditional Understanding

AbstractFormalism in the philosophy of mathematics has taken a variety of forms and has been advocated for widely divergent reasons. In Sects. 1 and 2, I briefly introduce the major formalist doctrines of the late nineteenth and early twentieth centuries. These are what I call empirico-semantic formalism (advocated by Heine), game formalism (advocated by Thomae) and instrumental formalism (advocated by Hilbert). After describing these views, I note some basic points of similarity and difference between them. In the remainder of the paper, I turn my attention to Hilbert’s instrumental formalism. My primary aim there will be to develop its formalist elements more fully. These are, in the main, (i) its rejection of the axiom-centric focus of traditional model-construction approaches to consistency problems, (ii) its departure from the traditional understanding of the basic nature of proof and (iii) its distinctively descriptive or observational orientation with regard to the consistency problem for arithmetic. More specifically, I will highlight what I see as the salient points of connection between Hilbert’s formalist attitude and his finitist standard for the consistency proof for arithmetic. I will also note what I see as a significant tension between Hilbert’s observational approach to the consistency problem for arithmetic and his expressed hope that his solution of that problem would dispense with certain epistemological concerns regarding arithmetic once and for all.

The consistency problem for positive comprehension principles

1989 ◽  
Vol 54 (4) ◽  
pp. 1401-1418 ◽  
Author(s):  
M. Forti ◽  
R. Hinnion
Keyword(s):  
Set Theory ◽  
Difficult Problem ◽  
Large Cardinal ◽  
Positive Theory ◽  
Construction Principle ◽  
Short Summary ◽  
Free Construction ◽  
Unpublished Thesis ◽  
Consistency Problem ◽  
Original Construction

Since Gilmore showed that some theory with a positive comprehension scheme is consistent when the axiom of extensionality is dropped and inconsistent with it (see [1] and [2]), the problem of the consistency of various positive comprehension schemes has been investigated. We give here a short classification, which shows clearly the importance of the axiom of extensionality and of the abstraction operator in these consistency problems. The most difficult problem was to show the consistency of the comprehension scheme for positive formulas, with extensionality but without abstraction operator. In his unpublished thesis, Set theory in which the axiom of foundation fails [3], Malitz solved partially this problem but he needed to assume the existence of some unusual kind of large cardinal; as his original construction is very interesting and his thesis is unpublished, we give a short summary of it. M. Forti solved the problem completely by working in ZF with a free-construction principle (sometimes called an anti-foundation axiom), instead of ZF with the axiom of foundation, as Malitz did.This permits one to obtain the consistency of this positive theory, relative to ZF. In his general investigations about “topological set theories” (to be published), E. Weydert has independently proved the same result. The authors are grateful to the Mathematisches Forshungsinstitut Oberwolfach for giving them the opportunity of discussing these subjects and meeting E. Weydert during the meeting “New Foundations”, March 1–7, 1987.

Sign in / Sign up

Export Citation Format

Share Document