You are here
Homeaxiom system for first order logic
Primary tabs
axiom system for first order logic
Let FO$(\Sigma)$ be a first order language over signature $\Sigma$. Furthermore, let $V$ be a countably infinite set of variables and $V(\Sigma)$ the set extending $V$ to include the constants in $\Sigma$. Before describing the axiom system for FO$(\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}\cdots\forall x_{n}A$, for any $n\geq 0$. Thus, $A$ is a generalization of itself.
The axiom system of FO$(\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. $\neg\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(\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 $\land,\lor$, and $\exists$ are derived: $A\lor B:=\neg A\to B$; $A\land B:=\neg(\neg A\lor\neg B)$; and $\exists xA:=\neg\forall x\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 $\forall y(x<y)$. Then $A[y/x]$ is $\forall y(y<y)$. 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 $\vdash A$, then $\vdash\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 $\vdash\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 $\vdash\forall xB$ and $\vdash\forall x(B\to A)$. Since $\forall x(B\to A)\to(\forall xB\to\forall xA)$ is an axiom, we have $\vdash\forall xB\to\forall xA$ by modus ponens, and then $\vdash\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 $\Gamma$ of wff’s, if there is a finite sequence
$A_{1},\ldots,A_{n}$ 
where $A=A_{n}$, such that for each $i$, $i=1,\ldots,n$
1. $A_{i}$ is either an axiom or in $\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 xA_{j}$ for some $j<i$.
Mathematics Subject Classification
03B10 no label found Forums
 Planetary Bugs
 HS/Secondary
 University/Tertiary
 Graduate/Advanced
 Industry/Practice
 Research Topics
 LaTeX help
 Math Comptetitions
 Math History
 Math Humor
 PlanetMath Comments
 PlanetMath System Updates and News
 PlanetMath help
 PlanetMath.ORG
 Strategic Communications Development
 The Math Pub
 Testing messages (ignore)
 Other useful stuff
 Corrections