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

Title	axiom system for first order logic
Canonical name	AxiomSystemForFirstOrderLogic
Date of creation	2013-03-22 19:32:22
Last modified on	2013-03-22 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