View source for Minimal functional calculus

{{TEX|done}}
''minimal predicate calculus''

The calculus of predicates given by all axiom schemes of the [[Minimal propositional calculus|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|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====
<table><TR><TD valign="top">[1]</TD> <TD valign="top">  A. Church,   "Introduction to mathematical logic" , '''1''' , Princeton Univ. Press  (1956)</TD></TR></table>