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.