On the rules of proof in the pure functional calculus of the first order

1951 ◽  
Vol 16 (2) ◽  
pp. 107-111 ◽  
Author(s):  
Andrzej Mostowski
Keyword(s):  
Functional Calculus ◽  
Free Variable ◽  
Propositional Function ◽  
Cartesian Power ◽  
First Order ◽  
A Value ◽  
Free Variables ◽  
Individual Variables ◽  
Definition Of

We consider here the pure functional calculus of first order as formulated by Church.Church, l.c., p. 79, gives the definition of the validity of a formula in a given set I of individuals and shows that a formula is provable in if and only if it is valid in every non-empty set I. The definition of validity is preceded by the definition of a value of a formula; the notion of a value is the basic “semantical” notion in terms of which all other semantical notions are definable.The notion of a value of a formula retains its meaning also in the case when the set I is empty. We have only to remember that if I is empty, then an m-ary propositional function (i.e. a function from the m-th cartesian power Im to the set {f, t}) is the empty set. It then follows easily that the value of each well-formed formula with free individual variables is the empty set. The values of wffs without free variables are on the contrary either f or t. Indeed, if B has the unique free variable c and ϕ is the value of B, then the value of (c)B according to the definition given by Church is the propositional constant f or t according as ϕ(j) is f for at least one j in I or not. Since, however, there is no j in I, the condition ϕ(j) = t for all j in I is vacuously satisfied and hence the value of (c)B is t.

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

Completeness in the theory of types

1950 ◽  
Vol 15 (2) ◽  
pp. 81-91 ◽  
Author(s):  
Leon Henkin
Keyword(s):  
Functional Calculus ◽  
Formal System ◽  
Axiom System ◽  
Second Order ◽  
True Proposition ◽  
Arbitrary Domain ◽  
Individual Variables ◽  
Definition Of ◽  
The Individual ◽  
Positive Integers

The first order functional calculus was proved complete by Gödel in 1930. Roughly speaking, this proof demonstrates that each formula of the calculus is a formal theorem which becomes a true sentence under every one of a certain intended class of interpretations of the formal system.For the functional calculus of second order, in which predicate variables may be bound, a very different kind of result is known: no matter what (recursive) set of axioms are chosen, the system will contain a formula which is valid but not a formal theorem. This follows from results of Gödel concerning systems containing a theory of natural numbers, because a finite categorical set of axioms for the positive integers can be formulated within a second order calculus to which a functional constant has been added.By a valid formula of the second order calculus is meant one which expresses a true proposition whenever the individual variables are interpreted as ranging over an (arbitrary) domain of elements while the functional variables of degree n range over all sets of ordered n-tuples of individuals. Under this definition of validity, we must conclude from Gödel's results that the calculus is essentially incomplete.It happens, however, that there is a wider class of models which furnish an interpretation for the symbolism of the calculus consistent with the usual axioms and formal rules of inference. Roughly, these models consist of an arbitrary domain of individuals, as before, but now an arbitrary class of sets of ordered n-tuples of individuals as the range for functional variables of degree n. If we redefine the notion of valid formula to mean one which expresses a true proposition with respect to every one of these models, we can then prove that the usual axiom system for the second order calculus is complete: a formula is valid if and only if it is a formal theorem.

A relative consistency proof

1954 ◽  
Vol 19 (1) ◽  
pp. 21-28 ◽  
Author(s):  
Joseph R. Shoenfield
Keyword(s):  
Set Theory ◽  
Functional Calculus ◽  
Direct Method ◽  
Axiom System ◽  
Similar Process ◽  
Consistency Proof ◽  
First Order ◽  
Definition Of ◽  
A Direct Method ◽  
Exact Definition

LetCbe an axiom system formalized within the first order functional calculus, and letC′ be related toCas the Bernays-Gödel set theory is related to the Zermelo-Fraenkel set theory. (An exact definition ofC′ will be given later.) Ilse Novak [5] and Mostowski [8] have shown that, ifCis consistent, thenC′ is consistent. (The converse is obvious.) Mostowski has also proved the stronger result that any theorem ofC′ which can be formalized inCis a theorem ofC.The proofs of Novak and Mostowski do not provide a direct method for obtaining a contradiction inCfrom a contradiction inC′. We could, of course, obtain such a contradiction by proving the theorems ofCone by one; the above result assures us that we must eventually obtain a contradiction. A similar process is necessary to obtain the proof of a theorem inCfrom its proof inC′. The purpose of this paper is to give a new proof of these theorems which provides a direct method of obtaining the desired contradiction or proof.The advantage of the proof may be stated more specifically by arithmetizing the syntax ofCandC′.

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

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

A note on direct products

1958 ◽  
Vol 23 (1) ◽  
pp. 1-6 ◽  
Author(s):  
L. Novak Gál
Keyword(s):  
Binary Relation ◽  
Direct Product ◽  
Functional Calculus ◽  
Ordered Set ◽  
Infinite Sequence ◽  
Direct Products ◽  
First Order ◽  
Individual Variables ◽  
The Individual ◽  
Infinite Sequences

By an algebra is meant an ordered set Γ = 〈V,R1, …, Rn, O1, …, Om〉, where V is a class, Ri (1 ≤ i ≤, n) is a relation on nj elements of V (i.e. Ri ⊆ Vni), and Oj (1 ≤ i ≤ n) is an operation on elements of V such that Oj(x1, … xmj) ∈ V) for all x1, …, xmj ∈ V). A sentence S of the first-order functional calculus is valid in Γ, if it contains just individual variables x1, x2, …, relation variables ϱ1, …,ϱn, where ϱi,- is nj-ary (1 ≤ i ≤ n), and operation variables σ1, …, σm, where σj is mj-ary (1 ≤, j ≤ m), and S holds if the individual variables are interpreted as ranging over V, ϱi is interpreted as Ri, and σi as Oj. If {Γi}i≤α is a (finite or infinite) sequence of algebras Γi, where Γi = 〈Vi, Ri〉 and Ri, is a binary relation, then by the direct productΓ = Πi<αΓi is meant the algebra Γ = 〈V, R〉, where V consists of all (finite or infinite) sequences x = 〈x1, x2, …, xi, …〉 with Xi ∈ Vi and where R is a binary relation such that two elements x and y of V are in the relation R if and only if xi and yi- are in the relation Ri for each i < α.

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

scholarly journals An elimination theorem of uniqueness conditions in the intuitionistic predicate calculus

1982 ◽  
Vol 85 ◽  
pp. 223-230 ◽  
Author(s):  
Nobuyoshi Motohashi
Keyword(s):  
Free Variable ◽  
The Other ◽  
Predicate Calculus ◽  
First Order ◽  
Free Variables ◽  
Classical Predicate

This paper is a sequel to Motohashi [4]. In [4], a series of theorems named “elimination theorems of uniqueness conditions” was shown to hold in the classical predicate calculus LK. But, these results have the following two defects : one is that they do not hold in the intuitionistic predicate calculus LJ, and the other is that they give no nice axiomatizations of some sets of sentences concerned. In order to explain these facts more explicitly, let us introduce some necessary notations and definitions. Let L be a first order classical predicate calculus LK or a first order intuitionistic predicate calculus LJ. n-ary formulas in L are formulas F(ā) in L with a sequence ā of distinct free variables of length n such that every free variable in F occurs in ā.

Sign in / Sign up

Export Citation Format

Share Document