Goodbye Syntax?

I am now settled in, so can resume posting again. My goal is to average one post a week from now on, so there should be a bit more activity on this little piece of cyberspace.

Onto more interesting things. There are many different methods for performing proofs in logic. For instance, sequent calculi, natural deduction and related systems. However, they all have one thing in common: they manipulate syntax. This is fair enough, since a proof is a syntactic object, right? Well, yes. However, when we work in, say, propositional logic, we have access to a particularly perspicuous semantics and we know that the syntax matches up with the semantics very nicely. And, so, why not perform proofs in the semantics. Of course, the problem is that in order to find a tautology, we pretty much have to try out all possible valuations (barring something obscene like P=NP). Well, now there is a third way: combinatorics and, in particular, graph theory.

Proofs Without Syntax - Dominic Hughes

The above paper does a good job of explaining the necessary background, so I will only dwell on it briefly. The crux of the paper is in defining a "combinatorial" proof to be a special sort of graph homomorphism (map between graphs that preserves edges) between very special graphs. The main result is a soundness and completeness type of afair: if a proposition is a tautology, it has a combinatorial proof and vice versa. In other words, we have a bit more structure for performing "semantic" proofs. It remains to be seen whether this can be done reasonably efficiently.