Editing Deduction theorem (section)

==The deduction theorem in predicate logic==
The deduction theorem is also valid in [[first-order logic]] in the following form:

*If ''T'' is a [[Theory (mathematical logic)|theory]] and ''F'', ''G'' are formulas with ''F'' [[Well-formed formula#Closed formulas|closed]], and <math>T \cup \{ F \} \vdash G</math>, then <math>T \vdash F \rightarrow G</math>.

Here, the symbol <math>\vdash</math> means "is a syntactical consequence of." We indicate below how the proof of this deduction theorem differs from that of the deduction theorem in propositional calculus.

In the most common versions of the notion of formal proof, there are, in addition to the axiom schemes
of propositional calculus (or the understanding that all tautologies of propositional calculus are to
be taken as axiom schemes in their own right), [[First-order logic#Quantifier axioms|quantifier axioms]], and in addition to [[modus ponens]], one additional [[rule of inference]], known as the rule of [[Generalization (logic)|''generalization'']]: "From ''K'', infer ∀''vK''."

In order to convert a proof of ''G'' from ''T''∪{''F''} to one of ''F''→''G'' from ''T'', one deals 
with steps of the proof of ''G'' that are axioms or result from application of modus ponens in the 
same way as for proofs in propositional logic. Steps that result from application of the rule of
generalization are dealt with via the following quantifier axiom (valid whenever the variable
''v'' is not free in formula ''H''):

*(∀''v''(''H''→''K''))→(''H''→∀''vK'').

Since in our case ''F'' is assumed to be closed, we can take ''H'' to be ''F''. This axiom allows
one to deduce ''F''→∀''vK'' from ''F''→''K'' and generalization, which is just what is needed whenever
the rule of generalization is applied to some ''K'' in the proof of ''G''.

In first-order logic, the restriction of that F be a closed formula can be relaxed given that the free variables in F has not been varied in the deduction of G from <math>T \cup \{ F \}</math>. In the case that a free variable v in F has been varied in the deduction, we write <math>T \cup \{ F \} \vdash^v G</math> (the superscript in the turnstile indicating that v has been varied) and the corresponding form of the deduction theorem is <math>T \vdash (\forall vF) \rightarrow G</math>.{{sfn|Kleene|1980|pp=102–106}}