Ordinal bounds for κ-consistency

1974 ◽  
Vol 39 (4) ◽  
pp. 693-699 ◽  
Author(s):  
Warren D. Goldfarb
Keyword(s):  
Nonnegative Integer ◽  
Transfinite Induction ◽  
Axiom Schema ◽  
First Order ◽  
Order Arithmetic ◽  
Definition Of ◽  
Image Position ◽  
Primitive Recursive

In [1] the ω-consistency of arithmetic was proved by a method which yields fine ordinal bounds for κ-consistency, κ ≥ 1. In this paper these bounds are shown to be best possible. The ω-consistency of a number-theoretic system S can be expressed thus: for all sentences ∃xM,where ProvS is the proof predicate for S, if n is a nonnegative integer then n is the formal numeral (of S) for n, and if G is a formula then ˹G˺ is the Gödel number of G. The κ-consistency of S is the restriction of (1) to Σκ0 sentences ∃xM. The proof in [1] establishes the no-counterexample interpretation of (1), that is, the existence of a constructive functional Φ such that, for all sentences ∃xM, all numbers p, and all functions f,(see [1, §2]). A functional Φ is an ω-consistency functional for S if it satisfies (2) for all sentences ∃xM, and a κ-consistency functional for S if it satisfies (2) for all Σκ0 sentences ∃xM.The systems considered in [1] are those obtained from classical first-order arithmetic Z, including the schema for definition of primitive recursive (p.r.) functions, by adjoining, for some p.r. well-founded ordering ≺ of the nonnegative integers, the axiom schemathat is, the least number principle on ≺; it is equivalent to the schema of transfinite induction on ≺.

A formalization of the theory of ordinal numbers

1965 ◽  
Vol 30 (3) ◽  
pp. 295-317 ◽  
Author(s):  
Gaisi Takeuti
Keyword(s):  
Set Theory ◽  
Natural Extension ◽  
Mathematical Induction ◽  
Predicate Calculus ◽  
Transfinite Induction ◽  
First Order ◽  
Recursive Functions ◽  
Ordinal Numbers ◽  
Primitive Recursive ◽  
Order Predicate Calculus

Although Peano's arithmetic can be developed in set theories, it can also be developed independently. This is also true for the theory of ordinal numbers. The author formalized the theory of ordinal numbers in logical systems GLC (in [2]) and FLC (in [3]). These logical systems which contain the concept of ‘arbitrary predicates’ or ‘arbitrary functions’ are of higher order than the first order predicate calculus with equality. In this paper we shall develop the theory of ordinal numbers in the first order predicate calculus with equality as an extension of Peano's arithmetic. This theory will prove to be easy to manage and fairly powerful in the following sense: If A is a sentence of the theory of ordinal numbers, then A is a theorem of our system if and only if the natural translation of A in set theory is a theorem of Zermelo-Fraenkel set theory. It will be treated as a natural extension of Peano's arithmetic. The latter consists of axiom schemata of primitive recursive functions and mathematical induction, while the theory of ordinal numbers consists of axiom schemata of primitive recursive functions of ordinal numbers (cf. [5]), of transfinite induction, of replacement and of cardinals. The latter three axiom schemata can be considered as extensions of mathematical induction.In the theory of ordinal numbers thus developed, we shall construct a model of Zermelo-Fraenkel's set theory by following Gödel's construction in [1]. Our intention is as follows: We shall define a relation α ∈ β as a primitive recursive predicate, which corresponds to F′ α ε F′ β in [1]; Gödel defined the constructible model Δ using the primitive notion ε in the universe or, in other words, using the whole set theory.

On deciding the truth of certain statements involving the notion of consistency

1976 ◽  
Vol 41 (4) ◽  
pp. 779-781 ◽  
Author(s):  
George Boolos
Keyword(s):  
Free Variable ◽  
Incompleteness Theorem ◽  
First Order ◽  
Order Arithmetic ◽  
Image Position

Friedman has posed (see [F, p. 117]) the following problem: “35. Define the set E of expressions by (i) Con is an expression; (ii) if A, B are expressions so are (~ A), (A&B), and Con(A). Each expression ϕ in E determines a sentence ϕ in PA [classical first-order arithmetic] by taking Con* to be “PA is consistent,” ( ~ A) * to be ~ (A*), (A&B)* to be A*&B*, and Con(A)* to be “PA + ‘A*’ is consistent.” The set of expressions ϕ ∈ E such that ϕ* is true is recursive.The formalized second incompleteness theorem readsIn order to simplify notation, we will reformulate Friedman's problem slightly. Let Con be the usual sentence of PA expressing the consistency of PA, ~ A the negation of A, (A&B) the conjunction of A and B, etc., and Bew(A) the result of substituting the numeral for the Gödel number of A for the free variable in the usual provability predicate for PA. Let Con(A) = ~ Bew(~ A). (Con(A) is equivalent in PA to the usual sentence expressing the consistency of PA + A.) And let the class of F-sentences be the smallest class which contains Con and which also contains ~ A, (A&B) and Con(A) whenever it contains A and B. Since ⊦PA Bew(A) ↔ Bew(B) if ⊦PAA ↔ B, Friedman's problem is then the question whether the class of true F-sentences is recursive.The answer is that it is recursive. To see why, we need a definition and a theorem.Definition. An atom is a sentence Conn for some n ≥ 1, where Cont = Con and Conn + 1 = Con(Conn).

On the definition of ‘formal deduction’

1956 ◽  
Vol 21 (2) ◽  
pp. 129-136 ◽  
Author(s):  
Richard Montague ◽  
Leon Henkin
Keyword(s):  
Functional Calculus ◽  
Modus Ponens ◽  
Formal Proof ◽  
Axiom Schema ◽  
First Order ◽  
Individual Variable ◽  
Individual Variables ◽  
Definition Of ◽  
Formal Rules

The following remarks apply to many functional calculi, each of which can be variously axiomatized, but for clarity of exposition we shall confine our attention to one particular system Σ. This system is to have the usual primitive symbols and formation rules of the pure first-order functional calculus, and the following formal axiom schemata and formal rules of inference.Axiom schema 1. Any tautologous wff (well-formed formula).Axiom schema 2. (a) A ⊃ B, where A is any wff, a and b are any individual variables, and B arises from A by replacing all free occurrences of a by free occurrences of b.Axiom schema 3. (a)(A ⊃ B)⊃(A⊃ (a)B). where A and B are any wffs, and a is any individual variable not free in A.Rule of Modus Ponens: applies to wffs A and A ⊃ B, and yields B.Rule of Generalization: applies to a wff A and yields (a)A, where a is any individual variable.A formal proof in Σ is a finite column of wffs each of whose lines is a formal axiom or arises from two preceding lines by the Rule of Modus Ponens or arises from a single preceding line by the Rule of Generalization. A formal theorem of Σ is a wff which occurs as the last line of some formal proof.

A theorem on deducibility for second-order functions

1939 ◽  
Vol 4 (2) ◽  
pp. 77-79 ◽  
Author(s):  
C. H. Langford
Keyword(s):  
Second Order ◽  
Order Function ◽  
Usual Definition ◽  
First Order ◽  
Free Variables ◽  
Usual Convention ◽  
Definition Of ◽  
Image Position

It is known that the usual definition of a dense series without extreme elements is complete with respect to first-order functions, in the sense that any first-order function on the base of a set of postulates defining such a series either is implied by the postulates or is inconsistent with them. It is here understood, in accordance with the usual convention, that when we speak of a function on the base , the function shall be such as to place restrictions only upon elements belonging to the class determined by f; or, more exactly, every variable with a universal prefix shall occur under the hypothesis that its values satisfy f, while every variable with an existential prefix shall have this condition categorically imposed upon it.Consider a set of postulates defining a dense series without extreme elements, and add to this set the condition of Dedekind section, to be formulated as follows. Let the conjunction of the three functions,be written H(ϕ), where the free variables f and g, being parameters throughout, are suppressed. This is the hypothesis of Dedekind's condition, and the conclusion iswhich may be written C(ϕ).

The McKinsey axiom is not canonical

1991 ◽  
Vol 56 (2) ◽  
pp. 554-562 ◽  
Author(s):  
Robert Goldblatt
Keyword(s):  
Relational Semantics ◽  
Binary Relations ◽  
Order Condition ◽  
Modal Formula ◽  
First Order ◽  
Canonical Frame ◽  
Historical Importance ◽  
Definition Of ◽  
Image Position ◽  
Normal Modal Logics

The logic KM is the smallest normal modal logic that includes the McKinsey axiomIt is shown here that this axiom is not valid in the canonical frame for KM, answering a question first posed in the Lemmon-Scott manuscript [Lemmon, 1966].The result is not just an esoteric counterexample: apart from interest generated by the long delay in a solution being found, the problem has been of historical importance in the development of our understanding of intensional model theory, and is of some conceptual significance, as will now be explained.The relational semantics for normal modal logics first appeared in [Kripke, 1963], where a number of well-known systems were shown to be characterised by simple first-order conditions on binary relations (frames). This phenomenon was systematically investigated in [Lemmon, 1966], which introduced the technique of associating with each logic L a canonical frame which invalidates every nontheorem of L. If, in addition, each L-theorem is valid in , then L is said to be canonical. The problem of showing that L is determined by some validating condition C, meaning that the L-theorems are precisely those formulae valid in all frames satisfying C, can be solved by showing that satisfies C—in which case canonicity is also established. Numerous cases were studied, leading to the definition of a first-order condition Cφ associated with each formula φ of the formwhere Ψ is a positive modal formula.

An intuitionistically plausible interpretation of intuitionistic logic

1977 ◽  
Vol 42 (4) ◽  
pp. 564-578 ◽  
Author(s):  
H. C. M. de Swart
Keyword(s):  
Intuitionistic Logic ◽  
Predicate Calculus ◽  
Mathematical Treatment ◽  
First Order ◽  
The Past ◽  
Definition Of ◽  
Image Position ◽  
Order Predicate Calculus ◽  
Made In

Let IPC be the intuitionistic first-order predicate calculus. From the definition of derivability in IPC the following is clear:(1) If A is derivable in IPC, denoted by “⊦IPCA”, then A is intuitively true, that means, true according to the intuitionistic interpretation of the logical symbols. To be able to settle the converse question: “if A is intuitively true, then ⊦IPCA”, one should make the notion of intuitionistic truth more easily amenable to mathematical treatment. So we have to look then for a definition of “A is valid”, denoted by “⊨A”, such that the following holds:(2) If A is intuitively true, then ⊨ A.Then one might hope to be able to prove(3) If ⊨ A, then ⊦IPCA.If one would succeed in finding a notion of “⊨ A”, such that all the conditions (1), (2) and (3) are satisfied, then the chain would be closed, i.e. all the arrows in the scheme below would hold.Several suggestions for ⊨ A have been made in the past: Topological and algebraic interpretations, see Rasiowa and Sikorski [1]; the intuitionistic models of Beth, see [2] and [3]; the interpretation of Grzegorczyk, see [4] and [5]; the models of Kripke, see [6] and [7]. In Thirty years of foundational studies, A. Mostowski [8] gives a review of the interpretations, proposed for intuitionistic logic, on pp. 90–98.

The substitution method

1965 ◽  
Vol 30 (2) ◽  
pp. 175-192 ◽  
Author(s):  
W. W. Tait
Keyword(s):  
Free Variable ◽  
Order System ◽  
Conservative Extension ◽  
Substitution Method ◽  
Recursive Definition ◽  
First Order ◽  
Variable Elimination ◽  
Primitive Recursion ◽  
Definition Of ◽  
Primitive Recursive

This paper deals with Hilbert's substitution method for eliminating bound variables from first order proofs. With a first order system S framed in the ε-calculus [2] the problem is to associate a system S' without bound variables and an effective procedure for transforming derivations in S into derivations in S′. The transform of a formula A derived in S is to be an “ε-substitution instance” of A, i.e. it is obtained by replacing terms εxB(x) in A by terms of S′. In general the choice of these terms will depend on the particular derivation of A, and not on A alone. Cf. [4]. The present formulation sharpens Hilbert's original statement of the problem, i.e. that the transform of A should be finitistically verifiable, by making explicit the methods of verification used, namely those formalized in S′; on the other hand, it generalizes Hilbert's formulation since S′ need not be restricted to finitist systems.The bound variable elimination procedure can always be taken to be primitive recursive in (the Gödel number of) the derivation of A. Constructions which transcend primitive recursion can simply be built into S′.In this paper we show that if S′ is taken to be a second order system with constants for functionals, then the existence of suitable ε-substitution instances can be expressed by the solvability of certain functional equations in S′. We deal with two cases here. If S is number theory without induction, i.e. essentially predicate calculus with identity, then we can solve the equations in question by taking for S′ the free variable part S* of S with an added rule of definition of functionals by cases (recursive definition on finite ordinals), which is a conservative extension of S*.

Forcing and reducibilities. III. Forcing in fragments of set theory

1983 ◽  
Vol 48 (4) ◽  
pp. 1013-1034
Author(s):  
Piergiorgio Odifreddi
Keyword(s):  
Set Theory ◽  
Recursion Theory ◽  
Second Order ◽  
Analytic Hierarchy ◽  
Second Order Arithmetic ◽  
First Order ◽  
Order Language ◽  
Order Arithmetic ◽  
Definition Of ◽  
Generic Set

We conclude here the treatment of forcing in recursion theory begun in Part I and continued in Part II of [31]. The numbering of sections is the continuation of the numbering of the first two parts. The bibliography is independent.In Part I our language was a first-order language: the only set we considered was the (set constant for the) generic set. In Part II a second-order language was introduced, and we had to interpret the second-order variables in some way. What we did was to consider the ramified analytic hierarchy, defined by induction as:A0 = {X ⊆ ω: X is arithmetic},Aα+1 = {X ⊆ ω: X is definable (in 2nd order arithmetic) over Aα},Aλ = ⋃α<λAα (λ limit),RA = ⋃αAα.We then used (a relativized version of) the fact that (Kleene [27]). The definition of RA is obviously modeled on the definition of the constructible hierarchy introduced by Gödel [14]. For this we no longer work in a language for second-order arithmetic, but in a language for (first-order) set theory with membership as the only nonlogical relation:L0 = ⊘,Lα+1 = {X: X is (first-order) definable over Lα},Lλ = ⋃α<λLα (λ limit),L = ⋃αLα.

Note on the fan theorem

1974 ◽  
Vol 39 (3) ◽  
pp. 584-596 ◽  
Author(s):  
A. S. Troelstra
Keyword(s):  
Consistency Proof ◽  
Conservative Extension ◽  
First Order ◽  
Fan Theorem ◽  
Elementary Analysis ◽  
Elementary Methods ◽  
Order Arithmetic ◽  
Image Position

The principal aim of this paper is to establish a theorem stating, roughly, that the addition of the fan theorem and the. continuity schema to an intuitionistic system of elementary analysis results in a conservative extension with respect to arithmetical statements.The result implies that the consistency of first order arithmetic cannot be proved by use of the fan theorem, in addition to standard elementary methods—although it was the opposite assumption which led Gentzen to withdraw the first version of his consistency proof for arithmetic (see [B]).We must presuppose acquaintance with notation and principal results of [K, T], and with §1.6, Chapter II, and Chapter III, §4-6 of [T1]. In one respect we shall deviate from the notation in [K, T]: We shall use (n)x (instead of g(n, x)) to indicate the xth component of the sequence coded by n, if x < lth(n), 0 otherwise.We also introduce abbreviations n ≤* m, a ≤ b which will be used frequently below:

On the first-order logic of terms

1973 ◽  
Vol 38 (2) ◽  
pp. 177-188
Author(s):  
Lars Svenonius
Keyword(s):  
Order Logic ◽  
First Order Logic ◽  
Identity Function ◽  
First Order ◽  
Elementary Condition ◽  
Combinatorial Function ◽  
The One ◽  
Definition Of ◽  
Image Position

By an elementary condition in the variablesx1, …, xn, we mean a conjunction of the form x1 ≤ i < j ≤ naij where each aij is one of the formulas xi = xj or xi ≠ xj. (We should add that the formula x1 = x1 should be regarded as an elementary condition in the one variable x1.)Clearly, according to this definition, some elementary conditions are inconsistent, some are consistent. For instance (in the variables x1, x2, x3) the conjunction x1 = x2 & x1 = x3 & x2 ≠ x3 is inconsistent.By an elementary combinatorial function (ex. function) we mean any function which can be given a definition of the formwhere E1(x1, …, xn), …, Ek(x1, …, xn) is an enumeration of all consistent elementary conditions in x1, …, xn, and all the numbers d1, …, dk are among 1, …, n.Examples. (1) The identity function is the only 1-ary e.c. function.(2) A useful 3-ary e.c. function will be called J. The definition is

Sign in / Sign up

Export Citation Format

Share Document