Minimal functional calculus

minimal predicate calculus

The calculus of predicates given by all axiom schemes of the minimal propositional calculus and by the usual quantifier axiom schemes and deduction rules, that is,

$$\forall xA(x)\supset A(t),\quad A(t)\supset\exists xA(x)$$

($t$ an arbitrary term), modus ponens and

$$\frac{C\supset A(a)}{C\supset\forall xA(x)},\quad\frac{A(a)\supset C}{\exists xA(x)\supset C}$$

(provided the variable $a$ does not occur in $A(x)$ and $C$).

References

[1]	A. Church, "Introduction to mathematical logic" , 1 , Princeton Univ. Press (1956)