How much of the current logic is about syntax?

Question

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?

Answer 1

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.

Answer 2

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.

Answer 3

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.

Answer 4

I would posit that proof theory is exactly the syntactical part of logic, and the other three branches (set theory, model theory, and recursion theory) are what's left when you get rid of the syntax. Which is probably why those three branches get more attention nowadays.