axiom system for first order logic
Let FO$(\mathrm{\Sigma})$ be a first order language over signature^{} $\mathrm{\Sigma}$. Furthermore, let $V$ be a countably infinite^{} set of variables and $V(\mathrm{\Sigma})$ the set extending $V$ to include the constants in $\mathrm{\Sigma}$. Before describing the axiom system for FO$(\mathrm{\Sigma})$, we need the following definition:
Definition. Let $A$ be a wff. A generalization of $A$ is a wff having the form $\forall {x}_{1}\forall {x}_{2}\mathrm{\cdots}\forall {x}_{n}A$, for any $n\ge 0$. Thus, $A$ is a generalization of itself.
The axiom system of FO$(\mathrm{\Sigma})$ consists of any wff that is a generalization of a wff belonging to any one of the following six schemas:

1.
$A\to (B\to A)$

2.
$(A\to (B\to C))\to ((A\to B)\to (A\to C))$

3.
$\mathrm{\neg}\mathrm{\neg}A\to A$

4.
$\forall x(A\to B)\to (\forall xA\to \forall xB)$, where $x\in V$

5.
$A\to \forall xA$, where $x\in V$ is not free in $A$

6.
$\forall xA\to A[a/x]$, where $x\in V$, $a\in V(\mathrm{\Sigma})$, and $a$ is free for $x$ in $A$
and modus ponens^{} (from $A$ and $A\to B$ we may infer $B$) as its only rule of inference^{}.
In schema 6, the wff $A[a/x]$ is obtained by replacing all free occurrences of $x$ in $A$ by $a$.
Logical symbols $\wedge ,\vee $, and $\exists $ are derived: $A\vee B:=\mathrm{\neg}A\to B$; $A\wedge B:=\mathrm{\neg}(\mathrm{\neg}A\vee \mathrm{\neg}B)$; and $\exists xA:=\mathrm{\neg}\forall x\mathrm{\neg}A$.
Remark. Again, in schema 6, the reason why we want $a$ free for $x$ in $A$ is to keep the “intended meaning” of $A$ intact. For example, suppose $A$ is $$. Then $A[y/x]$ is $$. Obviously the two do not have the same “intended meaning”. In fact, $A[y/x]$ is not valid in any model. Similarly, in the schema 5, we want $x$ not occur free in $A$ to maintain its “intended meaning”. For example, if $A$ is the formula $x=0$, then $\forall xA$ is $\forall x(x=0)$, which is not true in any model with at least two elements.
The concepts of deductions^{} and theorems^{} are exactly the same as those found in propositional logic^{}. Here is an example: if $\u22a2A$, then $\u22a2\forall xA$. To see this, we induct on the length $n$ of the deduction of $A$. If $n=1$, then $A$ is an axiom, and therefore so is its generalization $\forall xA$, so that $\u22a2\forall xA$. Suppose now that the length is $n+1$. If $A$ is an axiom, we are back to the previous argument. Otherwise, $A$ is obtained from earlier formulas $B$ and $B\to A$ via modus ponens. Since the deduction of $B$ and $B\to A$ are at most $n$, by induction^{}, we have $\u22a2\forall xB$ and $\u22a2\forall x(B\to A)$. Since $\forall x(B\to A)\to (\forall xB\to \forall xA)$ is an axiom, we have $\u22a2\forall xB\to \forall xA$ by modus ponens, and then $\u22a2\forall xA$ by modus ponens again.
Remark. Another popular axiom system for first order logic has 1, 2, 3, 6 above as its axiom schemas^{}, plus the following schema

•
$\forall x(A\to B)\to (A\to \forall xB)$, where $x\in V$ is not free in $A$
and two rules of inferences: modus ponens, and universal generalization:

•
from $A$ we may infer $\forall xA$, where $x\in V$
Note the similarity between the rule of generalization and axiom schema 5 above. However, the important difference^{} is that $x$ is not permitted to be free in $A$ in the axiom schema.
With this change, the concept of deductions needs to be modified: we say that a wff $A$ is deducible from a set $\mathrm{\Gamma}$ of wff’s, if there is a finite sequence^{}
$${A}_{1},\mathrm{\dots},{A}_{n}$$ 
where $A={A}_{n}$, such that for each $i$, $i=1,\mathrm{\dots},n$

1.
${A}_{i}$ is either an axiom or in $\mathrm{\Gamma}$

2.
${A}_{i}$ is obtained by an application of modus ponens

3.
${A}_{i}$ is obtained by an application of generalization: ${A}_{i}$ is $\forall x{A}_{j}$ for some $$.
Title  axiom system for first order logic 

Canonical name  AxiomSystemForFirstOrderLogic 
Date of creation  20130322 19:32:22 
Last modified on  20130322 19:32:22 
Owner  CWoo (3771) 
Last modified by  CWoo (3771) 
Numerical id  24 
Author  CWoo (3771) 
Entry type  Definition 
Classification  msc 03B10 
Synonym  universal generalization 
Defines  generalization 