axiom system for first order logic (original) (raw)

Definition. Let A be a wff. A generalization of A is a wff having the form ∀x1⁢∀x2⁢⋯⁢∀xn⁢A, for any n≥0. 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. A→(B→A)
2. 1. (A→(B→C))→((A→B)→(A→C))
3. 1. ¬⁢¬⁢A→A
4. 1. ∀x(A→B)→(∀xA→∀xB), where x∈V
5. 1. A→∀x⁢A, where x∈V is not free in A
6. 1. ∀x⁢A→A⁢[a/x], where x∈V, a∈V⁢(Σ), and a is free for x in A

and modus ponens (from A and A→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 ∧,∨, and ∃ are derived: A∨B:=¬⁢A→B; A∧B:=¬⁡(¬⁢A∨¬⁢B); and ∃x⁢A:=¬⁢∀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 ∀x⁢A is ∀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 ⊢A, then ⊢∀x⁢A. 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 ∀x⁢A, so that ⊢∀x⁢A. 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→A via modus ponens. Since the deduction of B and B→A are at most n, by induction, we have ⊢∀x⁢B and ⊢∀x(B→A). Since ∀x(B→A)→(∀xB→∀xA) is an axiom, we have ⊢∀x⁢B→∀x⁢A by modus ponens, and then ⊢∀x⁢A 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

• •
  ∀x(A→B)→(A→∀xB), where x∈V is not free in A

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

• •
  from A we may infer ∀x⁢A, where x∈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 Γ of wff’s, if there is a finite sequence

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

1. 1. Ai is either an axiom or in Γ
2. 1. Ai is obtained by an application of modus ponens
3. 1. Ai is obtained by an application of generalization: Ai is ∀x⁢Aj for some j<i.