Formal Systems and Models
Bertil Ekdahl
AI seminar, February 19th, 2003
Abstract
Euclid is commonly regarded as the founder of the axiomatic
idea. However, he was not as rigorous as is usually believed. In his
proof he used a lot of intuitions that did not follow from the
axioms. Despite that, his methods were not really questioned for
almost 2000 years. It was in fact the dubious in Euclid's fifth axiom
that raised questions. When the postulate was changed, the need for
more rigorous proof machinery was called for. In the beginning of the
twenties, Hilbert gave Euclidean geometry a precise description; he
formalized mathematical reasoning. Geometry was made a purely formal
exercise in deducing certain conclusions from certain formal
premises. It was no longer about one single thing but about anything
that fitted its postulates. Bertrand Russell once said that
"mathematics is the subject in which we do not know what we are
talking about nor whether what we say is true".
The discovery of non-Euclidean geometry raised the question whether
there were several geometries and if so, the meaning of the different
geometries. During the twenties, the semantics was not on the tongue
of philosophers. Poland was an exception in this respect, but there is
no evidence that before Tarski the concept of truth belonged to
semantics. In the twenties, the philosophical prejudice was that the
concept of objective mathematical truth as opposed to demonstrability
was viewed with the greatest suspicion and widely rejected as
meaningless. In particular, Skolem had in fact all that was needed to
solve the completeness problem but did not do so because he was
constrained by his philosophical views on logic according to which
comparing truth and demonstrability was meaningless.
It was in that atmosphere that Tarski, in the beginning of the
thirties, gave a mathematical formulation of truth. The fundamental
idea was to include the concept of truth in its classical
interpretation, according to which "true" signifies the same as
"corresponding with reality". These ideas of Tarski were the origin of
model theory.