Published online by Cambridge University Press: 12 March 2014
In previous papers we developed two functional calculi of first order based on strict implication which we called S2 and S4. In the present paper, these systems will be extended to include a functional calculus of second order with the purpose of introducing the relation of identity of individuals.
Primitive symbols. ̂ {the abstraction operator, the blank space to be replaced by an appropriate variable}.
1 Barcan, R. C., A functional calculus of first order based on strict implication, this Journal, vol. 11 (1946), pp. 1–16Google Scholar and The deduction theorem in a functional calculus of first order based on strict implication, this Journal, vol. 11 (1946), pp. 115–118. The reader is asked to make the following changes in the enumeration of the axioms and theorems appearing in these papers: Place “1.” before the number of each theorem, e.g., axiom 1 will be referred to as 1.1 etc.
2 Part of this paper was included in a dissertation written in partial fulfillment of the requirements for the Ph.D. degree in Philosophy at Yale University. I am indebted to Professor Frederic B. Fitch for his criticisms and suggestions.
3 1.8, extended over propositional variables is a special case of 2.1. 1.8, extended over functional variables is a special case of 2.2.
4 The following condition should be added to Rule IV on p. 2 of A functional calculus of first order etc.: α should not occur freely in A at a place where β would be bound.
5 To prove the converse of such a theorem as 2.25 requires some principle such as □A ⊰ (B ⊰ □ A). That this principle is not provable in S22 can be shown by the Group I matrix on p. 493 of Lewis and Langford's Symbolic Logic, where this matrix has been appropriately interpreted for quantification.