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

Abstract

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 I m 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 .