Reflecting on incompleteness

1991 ◽  
Vol 56 (1) ◽  
pp. 1-49 ◽  
Author(s):  
Solomon Feferman

To what extent can mathematical thought be analyzed in formal terms? Gödel's theorems show the inadequacy of single formal systems for this purpose, except in relatively restricted parts of mathematics. However at the same time they point to the possibility of systematically generating larger and larger systems whose acceptability is implicit in acceptance of the starting theory. The engines for that purpose are what have come to be called reflection principles. These may be iterated into the constructive transfinite, leading to what are called recursive progressions of theories. A number of informative technical results have been obtained about such progressions (cf. Feferman [1962], [1964], [1968] and Kreisel [1958], [1970]). However, for some years I had hoped to give a more realistic and perspicuous finite generation procedure. This was first done in a rather special way in Feferman [1979] for the characterization of predicativity, which may be regarded as that part of mathematical thought implicit in our acceptance of elementary number theory. What is presented here is a new and simple notion of the reflective closure of a schematic theory which can be applied quite generally.Two examples of schematic theories in the sense used here are versions of Peano arithmetic and Zermelo set theory.


1962 ◽  
Vol 27 (1) ◽  
pp. 11-18 ◽  
Author(s):  
S. C. Kleene

Let Pp, Pd, and N be the intuitionistic formal systems of prepositional calculus, predicate calculus, and elementary number theory, respectively.1 Consider the following six propositions.8(1) ├A V B only if ├A or ├B.(2) ├∋xA(x) only if ├Ã(t) for some formula Ã(x) congruent to A(x) and some term t free for x in Ã(x).



1960 ◽  
Vol 25 (1) ◽  
pp. 27-32 ◽  
Author(s):  
Ronald Harrop

In a previous paper [1] it was proved, among other results, that a closed disjunction of intuitionistic elementary number theory N can be proved if and only if at least one of its disjunctands is provable and that a closed formula of the type (Ex)B(x) is provable in N if and only if B(n) is provable for some numeral n. The method of proof was to show that, as far as closed formulas are concerned, N is equivalent to a calculus N1 for which the result is immediate. The main step in the proof consisted in showing that the set of provable formulas of N1 is closed under modus ponens. This was done by obtaining a subset of the set which is closed under modus ponens and contains all members of the original set, with which it is therefore identical.



1955 ◽  
Vol 20 (1) ◽  
pp. 31-43 ◽  
Author(s):  
Hao Wang

In applying the method of arithmetization to a proof of the completeness of the predicate calculus, Bernays has obtained a result which, when applied to set theories formulated in the predicate calculus, may be stated thus.1.1. By adding an arithmetic sentence Con(S) (expressing the consistency of a set theory S) as a new axiom to the elementary number theory Zμ (HB II, p. 293), we can prove in the resulting system arithmetic translations of all theorems of S.It then follows that things definable or expressible in S have images in a simple extension of Zμ, if S is consistent. Since S can be a “strong” system, this fact has interesting consequences. Some of these are discussed by me and some are discussed by Kreisel. Kreisel finds an undecidable sentence of set theory by combining 1.1 and the Cantor diagonal argument. I shall prove below, using similar methods, a few further results, concerned with the notions of truth and designation. The method of numbering sets which I use (see 3.1 below) is different from Kreisel's. While the method used here is formally more elegant, Kreisel's method is much more efficient if we wish actually to calculate the numerical values.



1957 ◽  
Vol 22 (1) ◽  
pp. 1-14 ◽  
Author(s):  
Leon Henkin

The concepts of ω-consistency and ω-completeness are closely related. The former concept has been generalized to notions of Γ-consistency and strong Γ-consistency, which are applicable not only to formal systems of number theory, but to all functional calculi containing individual constants; and in this general setting the semantical significance of these concepts has been studied. In the present work we carry out an analogous generalization for the concept of ω-completeness.Suppose, then, that F is an applied functional calculus, and that Γ is a non-empty set of individual constants of F. We say that F is Γ-complete if, whenever B(x) is a formula (containing the single free individual variable x) such that ⊦ B(α) for every α in Γ, then also ⊦ (x)B(x). In the paper “Γ-con” a sequence of increasingly strong concepts, Γ-consistency, n = 1,2, 3,…, was introduced; and it is possible in a formal way to define corresponding concepts of Γn-completeness, as follows. We say that F is Γn-complete if, whenever B(x1,…, xn) is a formula (containing exactly n distinct free variables, namely x1…, xn) such that ⊦ B(α1,…,αn) for all α1,…,αn in Γ, then also ⊦ (X1)…(xn)B(x1,…,xn). However, unlike the situation encountered in the paper “Γ-con”, these definitions are not of interest – for the simple reason that F is Γn-complete if and only if it is Γ-complete, as one easily sees.



1937 ◽  
Vol 38 (2) ◽  
pp. 451 ◽  
Author(s):  
Max Zorn


1967 ◽  
Vol 8 (4) ◽  
pp. 353-356 ◽  
Author(s):  
Albert A. Mullin


2016 ◽  
pp. 1-32
Author(s):  
Gary L. Mullen ◽  
James A. Sellers


Axioms ◽  
2021 ◽  
Vol 10 (4) ◽  
pp. 263
Author(s):  
Yuri N. Lovyagin ◽  
Nikita Yu. Lovyagin

The standard elementary number theory is not a finite axiomatic system due to the presence of the induction axiom scheme. Absence of a finite axiomatic system is not an obstacle for most tasks, but may be considered as imperfect since the induction is strongly associated with the presence of set theory external to the axiomatic system. Also in the case of logic approach to the artificial intelligence problems presence of a finite number of basic axioms and states is important. Axiomatic hyperrational analysis is the axiomatic system of hyperrational number field. The properties of hyperrational numbers and functions allow them to be used to model real numbers and functions of classical elementary mathematical analysis. However hyperrational analysis is based on well-known non-finite hyperarithmetic axiomatics. In the article we present a new finite first-order arithmetic theory designed to be the basis of the axiomatic hyperrational analysis and, as a consequence, mathematical analysis in general as a basis for all mathematical application including AI problems. It is shown that this axiomatics meet the requirements, i.e., it could be used as the basis of an axiomatic hyperrational analysis. The article in effect completes the foundation of axiomatic hyperrational analysis without calling in an arithmetic extension, since in the framework of the presented theory infinite numbers arise without invoking any new constants. The proposed system describes a class of numbers in which infinite numbers exist as natural objects of the theory itself. We also do not appeal to any “enveloping” set theory.



1942 ◽  
Vol 7 (2) ◽  
pp. 65-89 ◽  
Author(s):  
Paul Bernays

The foundation of analysis does not require the full generality of set theory but can be accomplished within a more restricted frame. Just as for number theory we need not introduce a set of all finite ordinals but only a class of all finite ordinals, all sets which occur being finite, so likewise for analysis we need not have a set of all real numbers but only a class of them, and the sets with which we have to deal are either finite or enumerable.We begin with the definitions of infinity and enumerability and with some consideration of these concepts on the basis of the axioms I—III, IV, V a, V b, which, as we shall see later, are sufficient for general set theory. Let us recall that the axioms I—III and V a suffice for establishing number theory, in particular for the iteration theorem, and for the theorems on finiteness.



Sign in / Sign up

Export Citation Format

Share Document