Meaning via Proofs

Verificationism is the idea, popular amongst the logical positivists, that the meaning of a sentence is to be equated with the method used to establish it. That is, a statement is true if and only if we can, in principle, verify its truth or if it is analytic, which is to say that it is true by definition.

Now, suppose that we are working in classical logic and wish to assert some statement φ and pretend for the moment that we are all happy little verificationists. This means that in order to assert φ, we first need to give a method for determining whether or not it is true. That is, we need to determine whether or not it is present in our model. Being logicians first and foremost, we proceed via structural induction. If φ is an analytic statement, otherwise known as an atomic proposition, then we are done. If φ is of the form "ψ and δ" then we are done if both ψ and δ are in our model. Proceeding in this manner, we can verify whether or not φ is in our model by verifying that a certain collection of atomic propositions and negated atomic propositions are present in our model.

This sort of explanation seems to give the impression that semantics precedes syntax. That is, the meaning of a syntactic expression is determined by its semantic interpretation. Or is it? Let's have a closer look at what is going on here. Returning to our assertion "ψ and δ", we reduced the verification of its presence in the model to the verification that ψ is in the model and the verification that δ is in the model. We can be somewhat facetious and invert this procedure. That is, suppose we already know that both ψ and δ are present in the model. Then we may assert "ψ and δ". Carrying on this inversion process, we can say that a statement is in the model if it is either analytic or can be constructed from the analytic statements via certain inference rules. In other words, what we have discovered is that our model of classical logic is nothing but the free boolean algebra generated by the analytic statements. But we can summarise the situation in a far more snappy manner:

Verification is dual to construction
An even more catchy war cry is:

Models are dual to proofs.
So, the inversion process that we followed allows us to say that syntax precedes semantics. This latter view is encompassed in what is known as proof theoretic semantics whereas the former view is, naturally, known as model theoretic semantics. Since, to a large extent, these theories are dual to one another both warrant serious attention. The latter has, however, had the lion's share of attention historically. Nevertheless, an intrepid group of researchers has been flying the flag of proof theoretic semantics. Its modern culmination is evident in both computational and mathematical logic in such places as interactive theorem proving and categorical semantics of linear logic. On the philosophical front, there has been a resurgence of interest lately, including a special issue of Synthese devoted to the subject. A good discussion of the sorts of things mentioned in this post is provided by the following paper from the volume (unfortunately, I cannot find a free version of the paper):

Meaning approached via proofs; Dag Prawitz

In the next post, I'll write a little about what categorical algebra has to do with this stuff.

Goedelian Memoirs

I have just finished a charming little book by Gaisi Takeuti:

Memoirs of a Proof Theorist; Mariko Yasugi and Nicholas Passell

The book is a translation of "Goedel'', written in Japanese by Takeuti and translated bu Mariko Yasugi and Nicholas Passell. The book consists, predominantly, of a series of articles about Goedel's life and work. Takeuti offers several personal insights into Goedel, having worked with him at IAS in Princeton.

In proof theoretic circles, Takeuti's name is inextricably linked to his fundamental conjecture' of a cut elimiantion theorem for second order logic, about which I have written previously. Since this conjecture was such a dominating aspect of Takeuti's work at the time of his friendship with Goedel, it is a thread which repeats throughout the book. In this english translation, an appendix has been added in which Takeuti very quickly takes the reader from the definition of a sequent, via Gentzen's consistency proof of arithmetic, to the statement of the fundamental conjecture in a mere 14 pages. It is a testament to Takeuti's deep understanding of this subject that he is able to illuminate all of these results in so brief an exposition.

Takeuti writes of how he managed to arouse Goedel's interest in the conjecture, saying:

His view of my fundamental conjecture was that counter-examples would be discovered by the method of his Incompleteness Theorem or by nonstandard methods'

This comment came back to haunt Takeuti, who relays an exerpt from a referee's report of a paper on the conjecture:

The author claims that the consistency of number theory can be derived from the fundamental conjecture, but this is obvioously inconsistent with Goedel's incompleteness theorem.'

The belief that one cannot establish cut elimination for second order logic was, perhaps, forgiveable given the close temporal proximity with the proof of the incompleteness theorem. The controversy arises since second order logic is the proof theoretic incarnation of set theory. The reason is that, just as first order predicates are equivalent to sets, so second order predicates allow one to state properties of sets. Second order quantification then means, of course, that one can quantify over sets.

Since one can express set theory in second order logic, it is certainly possible to formalise Peano Arithmetic, hence the controversy. However, Gentzen's consistency proof of arithmetic shows that it is equivalent to the accessibility of the first epsilon number, which is the ordinal corresponding to an exponential stack of omega's, of height omega. Here, accessibility means that any strictly decreasing chain of ordinals below this ordinal is finite. This claim, which is justifiable on semantic grounds is, nevertheless, not provable in peano arithmetic. So, there is no clash with the Incompleteness Theorem - we are using an extension of arithmetic in order to prove the consistency of arithmetic.

The book is filled with descriptions both of Goedel's work and his professional relationships. Takeuti is remarkably candid at times when discussing Goedel's work, particularly his early result of the completeness of first order logic and offers many fascinating insights. The choice of title for the english translation is somewhat unfortunate. It is the memoirs of neither Goedel nor Takeuti. But perhaps this complaint is a tad glib - one could, perhaps, see it as the memoirs of Goedel's proof theoretic life.

On an administrative note, I have regular internet access over the next two weeks and have several posts lined up for this period.