Leon Henkin. The completeness of the first-order functional calculus. The journal of symbolic logic, Bd. 14 (1949), 159–166.

1950 ◽  
Vol 15 (1) ◽  
pp. 68-68 ◽  
Author(s):  
W. Ackermann
Keyword(s):  
Functional Calculus ◽  
Symbolic Logic ◽  
First Order

The deduction theorem in a functional calculus of first order based on strict implication

1946 ◽  
Vol 11 (4) ◽  
pp. 115-118 ◽  
Author(s):  
Ruth C. Barcan
Keyword(s):  
Functional Calculus ◽  
Symbolic Logic ◽  
Deduction Theorem ◽  
Strict Implication ◽  
First Order ◽  
Fundamental Theorems

In a previous paper, a functional calculus based on strict implication was developed. That system will be referred to as S2. The system resulting from the addition of Becker's axiom will be referred to as S4. In the present paper we will shw that a restricted deduction theorem is provable in S4 or more precisely in a system equivalent to S4. We will also show that such a deduction theorem is not provable in S2.The following theorems not derived in Symbolic logic will be required for the fundamental theorems XXVIII* and XXIX* of this paper. We will state most of them without proofs.

On Theses of the First-Order Functional Calculus

1961 ◽  
Vol 7 (11-14) ◽  
pp. 175-184
Author(s):  
Juliusz Reichbach
Keyword(s):  
Functional Calculus ◽  
First Order

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.

Sign in / Sign up

Export Citation Format

Share Document