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. 1.

$A\to(B\to A)$

2. 2.

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

3. 3.

$\neg\neg A\to A$

4. 4.

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

5. 5.

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

6. 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. Then $A[y/x]$ is $\forall 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. 1.

$A_{i}$ is either an axiom or in $\Gamma$

2. 2.

$A_{i}$ is obtained by an application of modus ponens

3. 3.

$A_{i}$ is obtained by an application of generalization: $A_{i}$ is $\forall xA_{j}$ for some $j.

Title axiom system for first order logic AxiomSystemForFirstOrderLogic 2013-03-22 19:32:22 2013-03-22 19:32:22 CWoo (3771) CWoo (3771) 24 CWoo (3771) Definition msc 03B10 universal generalization generalization