Microsoft Word goedel-duzi rtf

 

9

Now we have to choose some rules of derivation, which will produce new logical truths 

from the axioms (1)–(5). They are, for instance

13

: 

i)

 

modus ponens: from formulas 

ϕ and (ϕ → ψ) derive ψ; denoted ϕ, (ϕ → ψ) |– ψ 

ii)

 

generalization: from a formula 

ϕ derive ∀x ϕ; denoted ϕ |– ∀x ϕ 

The modus ponens rule is truth preserving: indeed, if 

ψ is true on the assumption that ϕ, 

and 

ϕ is true, then ψ must be true as well. The generalization rule is, however, obviously not 

truth preserving; but it preserves logical truth: if 

ϕ is logically valid, then it is satisfied by any 

structure and for any valuation of variables; hence 

∀x ϕ is logically valid as well.  

To make the notion of a finite inference method perfectly precise, we define a proof:  

A sequence of formulas 

ϕ

1

,…,

ϕ

n 

is a proof, if each formula 

ϕ

i

 is either  

•

 

an axiom or  

•

 

is derived from some previous members of the sequence 

ϕ

1

,…,

ϕ

i-1

 using a 

derivation rule i) or ii).  

A formula 

ϕ is provable in the calculus (or theorem of the calculus, denoted |– ϕ) if it is the 

last member of a proof. 

Since the axioms are logically valid (logical truths), and since modus ponens is a truth-

preserving rule and generalization is a logical-truth-preserving rule, it is obvious that each 

ϕ

i

 

of a proof 

ϕ

1

,…,

ϕ

n 

is a logically valid formula. Hence each provable formula, theorem of the 

calculus, is logically valid. We have defined a sound proof calculus (if |– 

ϕ, then |= ϕ).  

In 1928 Hilbert and Ackermann published a concise small book Grundzüge der 

theoretischen Logik, in which they arrived at exactly this point: they had defined axioms and 

derivation rules of predicate logic (slightly distinct from the above), and formulated the 

problem of completeness. They raised a question whether such a proof calculus is complete in 

the sense that each logical truth is provable within the calculus; in other words, whether the 

calculus proves exactly all the logically valid FOPL formulas. 

Gödel’s  Completeness theorem gives a positive answer to this question: the 1

st

-order 

predicate proof calculus (with appropriate axioms and rules, like those (1)

⎯(5), i) and ii) 

above) is a complete calculus, i.e., all the FOPL logical truths are provable (if |= 

ϕ, then  

|– 

ϕ).  

In FOPL syntactic provability is equivalent to being logically true: |= 

ϕ ⇔ |– ϕ. 

There is even a stronger version of the Completeness theorem that Gödel formulated as 

well. We derive consequences not only from logically valid sentences but also from other 

sentences true under some interpretation. For instance, from the fact that all the even numbers 

are divisible by 2 and the number 6 is even we can derive that the number 6 is divisible by 2. 

In FOPL notation we have:  

∀x [P(x) → Q(x,a)], P(b) |– Q(b,a).   

But none of these formulas is a logical truth. Yet this derivation is correct, since the 

conclusion is logically entailed by the premises: whenever the premises are true, the 

conclusion must be true as well. In other words, the conclusion is true in all the models of the 

premises.  

                                                 

13

 More exactly, the above are schemes of axioms and rules. The system we demonstrate here is nowadays 

known as Hilbert calculus. There are other possibilities of choosing axioms and rules, of course. For instance, 

sequent (Gentzen) calculus or natural deduction have even fewer axioms (usually just one) and rather more 

natural rules of deduction. 

 

---

 

10

To formulate the strong version of the Completeness theorem, we have to define the 

notion of a theory and a proof in a theory. In mathematics we often need to characterise some 

common features of particular distinct structures. For instance, the structure 

N 

= 

〈

N

, 

≤  〉, 

where 

N

  is the set of natural numbers and 

≤ its usual linear ordering, can be characterised by 

a set O of the following formulas: 

∀x P(x,x) 

 

 

 

 

 

 

ϕ

1 

∀x∀y [(P(x,y) & P(y,x)) → x=y] 

   

ϕ

2 

∀x∀y∀z [(P(x,y) & P(y,z)) → P(x,z)] 

   

ϕ

3 

We say that the set O of formulas 

ϕ

1

, 

ϕ

2

, 

ϕ

3

 is a theory  of  partial ordering. Particular 

formulas 

ϕ

1

, 

ϕ

2

, 

ϕ

3 

are special axioms of the theory O and they characterize reflexivity, anti-

symmetry and transitivity, respectively, of a partial ordering relation.  

If the binary relation 

≤ is assigned to the symbol P (and variables x, y, z range over 

N

), 

each of these formulas is valid in the structure 

N

. We also say that this structure is a model of 

the theory O.  

Moreover, for any set S the structure 

S

 = 

〈

P(S)

, 

⊆〉, where 

P(S)

 is the power set of 

S 

and 

⊆ is the relation of the set-theoretical inclusion, is a model of the theory O as well.

 

  

Both the structures are also a model of {

ϕ

1

, 

ϕ

2

, 

ϕ

3

, 

ϕ

4

}, where    

∃x∀y P(x,y)   

 

 

 

 

 

ϕ

4

  

claims that among the elements of the universe at least one element exists such that it is in a 

relation P with all the elements of the universe. The formula   

 

 

 

 

∀x∀y [P(x,y) ∨ P(y,x)] 

 

 

 

 

ϕ

5 

is satisfied by 

N

, but not satisfied by 

S

. We say that the set LO {

ϕ

1

, 

ϕ

2

, 

ϕ

3

, 

ϕ

5

} is a theory of 

linear ordering, and LO 

∪ {ϕ

4

,} is the theory of linear ordering with the least element. The 

power set of a set S is not ordered linearly.  

Now we can define: a (FOPL) theory is given by a (possibly infinite) set of FOPL 

formulas, the special axioms.  

A proof in a theory T is a sequence of formulas 

ϕ

1

,…,

ϕ

n

 such that each 

ϕ

i

 is either  

•

 

a logical axiom or  

•

 

a special axiom of T, or  

•

 

is derived from some previous members of the sequence 

ϕ

1

,…,

ϕ

i-1

 using a 

derivation rule i) or ii).  

A formula 

ϕ is provable in T iff it is the last member of a proof in T; we also say that the 

theory T proves 

ϕ, and the formula ϕ is a theorem of the theory (denoted T |– ϕ). A structure 

M 

is a model of the theory T, denoted 

M 

|= T, iff each special axiom of T is valid in 

M

.  

You may wonder whether the calculus is sound even in the stronger sense: whether each 

theorem of a theory, i.e., a formula provable in the theory, is logically entailed by the special 

axioms (denoted T |= 

ϕ); in other words, whether each theorem is valid in all the models of 

the theory.  As said above, the generalization rule is not truth-preserving. From the fact that, 

e.g., an x is even, we cannot correctly derive that all the x’s are even. However, generalization 

of the form 

ϕ(x) |– ∀x ϕ, where x is free in ϕ, is intuitively correct in case that the x in ϕ is 

any element of the universe. Indeed, if 

ϕ is true in a model 

M

 of the theory for any x, 

∀x ϕ is 

true in the model 

M

 as well. In other words, the generalization rule preserves the validity of a 

formula in a model. For this reason not only formulas satisfied but also valid in the intended 

---