# How much of the current logic is about syntax?

The basic logic course in school gives the impression that logic has both the syntax and the semantics aspects. Recently, I wonder whether the syntax part still plays an essential role in the current studies. Below are some of my observations, I hope the idea from the community can make them more complete.

Model theory: Even though model theory is stated in the language of logic, it can be viewed as the study of local isomorphism (see Poizat's "A course in Model Theory"). The syntax part is therefore a natural (though might be uncomfortable for some) way to view the theory rather than a necessity.

Recursion theory: The object of study is the notion of computability in different context. If we believe in Church-Turing Thesis, then these concept are independent of the formalism chosen.

Set theory: The intimate relationship between large cardinal and determinacy perhaps can suggest that this is a universal phenomenon. Will this phenomenon disappear if we change the language of mathematics to, for example, category theory?

Proof theory: I know too little to say anything.

If the observation is true, is it justified to demand that Turing degrees, and large cardinals receive the same mathematical status as, for example, prime numbers?

-
Could you explain what you mean by your last sentence? –  Joel David Hamkins Jan 13 '10 at 13:26
Side remark: I admit being linguistically confused by the usage of the word “syntax” here. To me, syntax is merely the question of whether formulas are well formed and how they are parsed, which is a necessary but uninteresting part of logic (in the sense that it is easily decidable). Isn't this question more about formal proofs versus model theory? True, a formal proof is an instance of syntactic manipulation, but I don't usually call it syntax for that reason. –  Harald Hanche-Olsen Jan 13 '10 at 14:25
@ Harald Hanche-Olsen: I don't really like the title formal proof vs model theory because I want to talk about other branches of logic as well. Do you have some suggestion? I don't know how to change it. @ Joel David Hamkins: I just heard that from a few people, I don't claim that is a universal. But it seems that even logicians are divided within themselves whether some question are correct one. See for example Solomon Feferman's "Does mathematics need new axiom?". I think you are right criticizing my remark. Their resemblance has little mathematical significance. –  Tran Chieu Minh Jan 13 '10 at 15:45
I apology to those who find the comment offensive. @ Joel David Hamkins: For the resemblance between prime numbers, Turing degrees, Large cardinal, they are all object that can not be reached from below by certain operation. This resemblance is rather superficial, but I think we can argue that it seems like the latter might be just as interesting as the former. This point is, however, beside the main one. The point main point is that if Turing degrees and large cardinal has some universal characteristic and not merely artifacts of the language, they should be considered a natural maths object. –  Tran Chieu Minh Jan 13 '10 at 16:41
@Tran Chieu Minh: Don't bother to change the title. I don't really have a better suggestion. I just wanted to find out if my understanding of what syntax is is off. (It may be coloured by too much computer programming.) –  Harald Hanche-Olsen Jan 13 '10 at 17:18

I think your observation is a very good one, but this phenomenon is limited to classical logic and does not continue to hold when we move to intuitionistic or substructural logics.

One way of understanding the role of syntax is to take the connectives of logic as explaining what counts as a legitimate proof of that proposition. So a conjunction $A \land B$ can be proven with a proof of $A$ and a proof of $B$, and an implication $A \implies B$ can be can be proven with a proof of $B$, assuming a hypothetical proof of $A$, and so on. Conversely, we also give rules explaining how to use true propositions -- e.g., from $A \land B$, we can re-derive $A$, and we can also rederive $B$.

If you work this out formally, you get Gentzen's system of natural deduction. The natural deduction systems for good logics admit a normal form theorem for proofs. The normalization procedure also gives us an equivalence relation on proofs (two proofs are equivalent if they have the same normal form), and it so happens that for classical logic, all proofs are equivalent. (This is a small lie: we can give more refined accounts of equivalence of classical proofs which don't equate everything, but the right answer here is still not entirely settled....)

The equivalence of proofs means that we can take the view that the meaning of a classical proposition is its truth value -- i.e., its provability -- and so algebraic models of classical logic contain all the information contained in a classical proposition. We don't need the proofs, and so syntax takes a secondary role.

But in intuitionistic and substructural logics like linear logic, not all proofs are equated. This means that we can't take the view that all the relevant information about a proposition is contained in its truth value, and so syntax retains a more important role.

-

We don't know how to abstract away from syntax in proof theory. If we say there are three main branches in proof theory:

1. Axiomatics seem to be necessarily syntactic: formulae are what it is about;
2. Relative consistency & ordinal analysis, which are ultimately about characterising provability strength in various ways: these are maybe as syntactic as recursion theory;
3. Structural proof theory, where we care about analytic proofs: there are programs to try to abstract away from syntax, such as categorical proof theory, but too much of proof theory doesn't yield to these kinds of analysis, so we can't say that these are successful yet.
-

To elaborate slightly on Neel's post: the fact that not all proofs in intuitionist and substructural logics are identified is a strength and not a weakness when viewed through the lens of the Curry-Howard isomorphism which shows that logic has computational content.

Basically the Curry-Howard isomorphism states that propositions in intuitionist logic can be identified with types in a programming language and proofs can be identified with programs. In classical logic all proofs of a given proposition are identified so classical logic is too impoverished to serve as a model for computation. In other words, the fact that there are multiple proofs of the same proposition in intuitionist logic is what allows us to have multiple programs with the same type.

-