A generalization of the concept of ω-completeness

1957 ◽  
Vol 22 (1) ◽  
pp. 1-14 ◽  
Author(s):  
Leon Henkin
Keyword(s):  
Number Theory ◽  
Functional Calculus ◽  
General Setting ◽  
Con A ◽  
Formal Systems ◽  
Individual Variable ◽  
Free Variables

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.

A derivation of number theory from ancestral theory

1952 ◽  
Vol 17 (3) ◽  
pp. 192-197 ◽  
Author(s):  
John Myhill
Keyword(s):  
Number Theory ◽  
Functional Calculus ◽  
Natural Numbers ◽  
Class Inclusion ◽  
First Order ◽  
Free Variables

Martin has shown that the notions of ancestral and class-inclusion are sufficient to develop the theory of natural numbers in a system containing variables of only one type.The purpose of the present paper is to show that an analogous construction is possible in a system containing, beyond the quantificational level, only the ancestral and the ordered pair.The formulae of our system comprise quantificational schemata and anything which can be obtained therefrom by writing pairs (e.g. (x; y), ((x; y); (x; (y; y))) etc.) for free variables, or by writing ancestral abstracts (e.g. (*xyFxy) etc.) for schematic letters, or both.The ancestral abstract (*xyFxy) means what is usually meant by ; and the formula (*xyFxy)zw answers to Martin's (zw; xy)(Fxy).The system presupposes a non-simple applied functional calculus of the first order, with a rule of substitution for predicate letters; over and above this it has three axioms for the ancestral and two for the ordered pair.

Solution of a problem of Leon Henkin

1955 ◽  
Vol 20 (2) ◽  
pp. 115-118 ◽  
Author(s):  
M. H. Löb
Keyword(s):  
Number Theory ◽  
Recursive Function ◽  
Formal System ◽  
Free Variable ◽  
Formal Proof ◽  
Predicate Calculus ◽  
First Order ◽  
Free Variables ◽  
Order Predicate Calculus

If Σ is any standard formal system adequate for recursive number theory, a formula (having a certain integer q as its Gödel number) can be constructed which expresses the proposition that the formula with Gödel number q is provable in Σ. Is this formula provable or independent in Σ? [2].One approach to this problem is discussed by Kreisel in [4]. However, he still leaves open the question whether the formula (Ex)(x, a), with Gödel-number a, is provable or not. Here (x, y) is the number-theoretic predicate which expresses the proposition that x is the number of a formal proof of the formula with Gödel-number y.In this note we present a solution of the previous problem with respect to the system Zμ [3] pp. 289–294, and, more generally, with respect to any system whose set of theorems is closed under the rules of inference of the first order predicate calculus, and satisfies the subsequent five conditions, and in which the function (k, l) used below is definable.The notation and terminology is in the main that of [3] pp. 306–326, viz. if is a formula of Zμ containing no free variables, whose Gödel number is a, then ({}) stands for (Ex)(x, a) (read: the formula with Gödel number a is provable in Zμ); if is a formula of Zμ containing a free variable, y say, ({}) stands for (Ex)(x, g(y)}, where g(y) is a recursive function such that for an arbitrary numeral the value of g() is the Gödel number of the formula obtained from by substituting for y in throughout. We shall, however, depart trivially from [3] in writing (), where is an arbitrary numeral, for (Ex){x, ).

The completeness of the first-order functional calculus

1949 ◽  
Vol 14 (3) ◽  
pp. 159-166 ◽  
Author(s):  
Leon Henkin
Keyword(s):  
Functional Calculus ◽  
Propositional Calculus ◽  
Higher Order ◽  
New Method ◽  
Completeness Proof ◽  
New Approach ◽  
First Order ◽  
Formal Systems ◽  
The Subject ◽  
Image Position

Although several proofs have been published showing the completeness of the propositional calculus (cf. Quine (1)), for the first-order functional calculus only the original completeness proof of Gödel (2) and a variant due to Hilbert and Bernays have appeared. Aside from novelty and the fact that it requires less formal development of the system from the axioms, the new method of proof which is the subject of this paper possesses two advantages. In the first place an important property of formal systems which is associated with completeness can now be generalized to systems containing a non-denumerable infinity of primitive symbols. While this is not of especial interest when formal systems are considered as logics—i.e., as means for analyzing the structure of languages—it leads to interesting applications in the field of abstract algebra. In the second place the proof suggests a new approach to the problem of completeness for functional calculi of higher order. Both of these matters will be taken up in future papers.The system with which we shall deal here will contain as primitive symbolsand certain sets of symbols as follows:(i) propositional symbols (some of which may be classed as variables, others as constants), and among which the symbol “f” above is to be included as a constant;(ii) for each number n = 1, 2, … a set of functional symbols of degree n (which again may be separated into variables and constants); and(iii) individual symbols among which variables must be distinguished from constants. The set of variables must be infinite.

Systems of transfinite types involving λ-conversion

1953 ◽  
Vol 18 (3) ◽  
pp. 209-224 ◽  
Author(s):  
Maurice L'Abbé
Keyword(s):  
Functional Calculus ◽  
The Other ◽  
Formal Systems ◽  
Other Hand ◽  
Main Ideas ◽  
Hierarchy Of Systems

The problem of constructing formal systems involving transfinite types was briefly suggested many times in the literature. Actually few attempts have been made to develop such systems. In particular, there exists a system based on a set of axioms and rules of inference suggested by Church and worked out in detail by E. Bustamante in his dissertation. Recently, John Kemeny has reformulated this system in a simplified way and has obtained an interesting hierarchy of systems. It so happens that all these systems considered by Kemeny may be regarded as successive extensions of a particular formulation of the theory of finite types, namely a certain monadic functional calculus of order ω whose main ideas are due to Tarski.There exists on the other hand a quite different formulation of the theory of finite types which is due to Church. It is a formulation which incorporates certain features of the calculus of λ-conversion, and which has revealed itself quite advantageous for certain purposes. The formulation of the theory of transfinite types which we are going to introduce in this paper may be considered as an attempt to generalize Church's formulation of the theory of finite types.

A generalization of the concept of ω-consistency

1954 ◽  
Vol 19 (3) ◽  
pp. 183-196 ◽  
Author(s):  
Leon Henkin
Keyword(s):  
Functional Calculus ◽  
Free Variable ◽  
Natural Numbers ◽  
Deductive Systems ◽  
Individual Variable ◽  
Special Cases ◽  
Definition Of ◽  
The Individual ◽  
Formal Properties ◽  
Use Of Models

In this paper we consider certain formal properties of deductive systems which, in special cases, reduce to the property of ω-consistency; and we then seek to understand the significance of these properties by relating them to the use of models in providing interpretations of the deductive systems.The notion of ω-consistency arises in connection with deductive systems of arithmetic. For definiteness, let us suppose that the system is a functional calculus whose domain of individuals is construed as the set of natural numbers, and that the system possesses individual constants ν0, ν1, ν2, … such that νi functions as a name for the number i. Such a system is called ω-consistent, if there is no well-formed formula A(x) (in which x is the only free variable) such that A(ν0), A(ν1), A(ν2), … and ∼(x)A(x) are all formal theorems of the system, where A(νi) is the formula resulting from A(x) by substituting the constant νi for each free occurrence of the individual variable x.Now consider an arbitrary applied functional calculus F, and let Γ be any non-empty set of its individual constants. In imitation of the definition of ω-consistency, we may say that the system F is Γ-consistent, if it contains no formula A(x) (in which x is the only free variable) such that ⊦ A (α) for every constant α in Γ, and also ⊦ ∼(x)A(x) (where an occurrence of “⊦” indicates that the formula which it precedes is a formal theorem). We easily see that the condition of Γ-consistency is equivalent to the condition that the system F contain no formula B(x) such that ⊦ ∼ B(α) for each α in Γ, and also ⊦ (∃x)B(x).

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.

Arithmetic with creative definitions by induction

1953 ◽  
Vol 18 (2) ◽  
pp. 115-118 ◽  
Author(s):  
John Myhill
Keyword(s):  
Functional Calculus ◽  
The Other ◽  
Central Feature ◽  
Natural Numbers ◽  
Free Variables ◽  
Image Position

The purpose of this paper is to present a system of arithmetic stronger than those usually employed, and to prove some syntactical theorems concerning it.We presuppose the lower functional calculus with identity and functions, and we start with three of Peano's axioms.The other two (0 ϵ N and x ϵ N .⊃. x′ ϵ N) we do not need since our variables are anyhow restricted to natural numbers. Sometimes in the interest of a uniform notation for functions, we write Sx instead of x′.Next we have two axioms for μ (the smallest number such that) as follows.A third axiom for μ must wait until we have defined ≤.Now we introduce the central feature of the system, the following rule of definition.RD. Let Φ be a previously unused symbol. Then we can introduce it by a pair of definitions of the following form (n ≥ 0),where F(x1, …, xn) is a wff in which no symbol occurs which was not previously defined (in particular, not Φ), and in which no free variables occur other than x1, …, xn (and possibly not all of these), and G(x1, …, xn, y) is a wff in which no free variables occur other than x1, …, xn, y (and possibly not all of these), and in which no symbol occurs which was not previously defined, except that Φ may occur but only if its last argument is y.

Disjunction and existence under implication in elementary intuitionistic formalisms

1962 ◽  
Vol 27 (1) ◽  
pp. 11-18 ◽  
Author(s):  
S. C. Kleene
Keyword(s):  
Number Theory ◽  
Predicate Calculus ◽  
Elementary Number Theory ◽  
Formal Systems ◽  
Elementary Number

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).

Some concepts concerning formal systems of number theory

1952 ◽  
Vol 57 (1) ◽  
pp. 1-12 ◽  
Author(s):  
Georg Kreisel
Keyword(s):  
Number Theory ◽  
Formal Systems
Sign in / Sign up

Export Citation Format

Share Document