axiom system for first order logic

Let FO(Σ) be a first order language over signaturePlanetmathPlanetmathPlanetmath Σ. Furthermore, let V be a countably infiniteMathworldPlanetmath set of variables and V(Σ) the set extending V to include the constants in Σ. Before describing the axiom system for FO(Σ), we need the following definition:

Definition. Let A be a wff. A generalization of A is a wff having the form x1x2xnA, for any n0. Thus, A is a generalization of itself.

The axiom system of FO(Σ) consists of any wff that is a generalization of a wff belonging to any one of the following six schemas:

  1. 1.


  2. 2.


  3. 3.


  4. 4.

    x(AB)(xAxB), where xV

  5. 5.

    AxA, where xV is not free in A

  6. 6.

    xAA[a/x], where xV, aV(Σ), and a is free for x in A

and modus ponensMathworldPlanetmath (from A and AB we may infer B) as its only rule of inferenceMathworldPlanetmath.

In schema 6, the wff A[a/x] is obtained by replacing all free occurrences of x in A by a.

Logical symbols ,, and are derived: AB:=¬AB; AB:=¬(¬A¬B); and xA:=¬x¬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 y(x<y). Then A[y/x] is 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 xA is x(x=0), which is not true in any model with at least two elements.

The concepts of deductionsMathworldPlanetmathPlanetmath and theoremsMathworldPlanetmath are exactly the same as those found in propositional logicPlanetmathPlanetmath. Here is an example: if A, then 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 xA, so that 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 BA via modus ponens. Since the deduction of B and BA are at most n, by inductionMathworldPlanetmath, we have xB and x(BA). Since x(BA)(xBxA) is an axiom, we have xBxA by modus ponens, and then xA by modus ponens again.

Remark. Another popular axiom system for first order logic has 1, 2, 3, 6 above as its axiom schemasMathworldPlanetmath, plus the following schema

  • x(AB)(AxB), where xV is not free in A

and two rules of inferences: modus ponens, and universal generalization:

  • from A we may infer xA, where xV

Note the similarity between the rule of generalization and axiom schema 5 above. However, the important differencePlanetmathPlanetmath 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 Γ of wff’s, if there is a finite sequencePlanetmathPlanetmath


where A=An, such that for each i, i=1,,n

  1. 1.

    Ai is either an axiom or in Γ

  2. 2.

    Ai is obtained by an application of modus ponens

  3. 3.

    Ai is obtained by an application of generalization: Ai is xAj 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