### 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.