Proof and Truth

Proof theory versus model theory is the same as anti-realist meaning theory vs realist (e.g. correspondence) theory of truth.

In model theory truth is given by a model, which corresponds to the “external world” or “universe”. The model under question determines whether a proposition is true, and the system of propositions should fit this model. A theory should fit the external world, since truth is out there.

But this becomes strange: how is the truth embedded in the external world established and recognized? What justifies the truth of a proposition - by what means is a “truth” embedded in the “external world” rendered as a truth? After all, truth needs to be established, instead of simply seen.

For the realist, the world is constituted of a fixed set of objects, independent of the mind and of its symbolic representations. Thus, the concept of “truth” amounts to a proper correspondence between the words and symbols emanating from the mind, and the objects and external things of the world. For the anti-realist, on the contrary, the very question “what objects is the world made of ?” requires already a theory or a description. In that case, the concept of “truth” amounts rather to some kind of ideal coherence between our various beliefs and experiences.
The sequent calculus generates formal proofs, and these formal proofs should be studied as autonomous entities, just like any other mathematical object.
The notion of “logical truth” in model-theory is based on the realist idea of the existence of an external world: the model. Unfortunately, this intu- ition of an external world is too redundant to be useful: what information is provided by the statement that “the formula A ∧B is true if and only if the formula A is true and the formula B is true” ?
So, the “meaning” of the connectives of logic arises from their introduction rules in the sequent calculus, and not from an external and realist concept of truth-value. These introduction rules are inherently justified by the structural properties of proofs, like cut-elimination, or the subformula property.
Gödel’s completeness theorem may be re-understood in this purely proof-theoretic way: every model M plays the role of a potential refutator, simulated by some kind of infinite non recursive proof — this leading to a purely proof-theoretic exposition of the completeness theorem.
This position is already apparent in Gerhard Gentzen’s writings [Gerhard Gentzen. The Collected Papers. Edited by M. E. Szabo, North-Holland 1969.]. It is nicely advocated today by Jean-Yves Girard [Jean-Yves Girard. Locus Solum. Mathematical Structures in Computer Science 11, pp. 301-506, 2001., Jean-Yves Girard. Le Point Aveugle. Hermann, collection "Visions des Sciences". 2006.]. This line of thought conveys the seeds of a luminous synthesis between proof theory and model theory. There is little doubt (to the author at least) that along with game semantics and linear logic, the realizability techniques developed by Jean-Louis Krivine (see [Jean-Louis Krivine. Realizability in classical logic. This volume of Panoramas et Synthèses.] in this volume) will play a key part in this highly desired unification. On the other hand, much remains to be understood on the model-theoretic and proof-theoretic sides in order to recast in proof theory the vast amount of knowledge accumulated in a century of model theory, see [Bruno Poizat. A Course in Model Theory. Universitext. Springer Verlag, 2004.] for a nice introduction to the topic. The interested reader will find in [Jean van Heĳenoort. Logic as calculus and logic as language Synthese, Volume 17, Number 1, january 1967.] a penetrating point of view by Jean van Heĳenoort on the historical origins of the dispute between model theory and proof theory.