Saturday, 4 August 2007

lo.logic - How much of the current logic is about syntax?

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.

No comments:

Post a Comment