Event Detail
Fri Oct 17, 2014 60 Evans Hall, 4–6 PM |
Logic Colloquium Dominic Hughes (Stanford University) First-order proofs without syntax |
Proofs of first-order logic are traditionally syntactic, built inductively from symbolic inference rules. This talk reformulates classical first-order logic (predicate calculus) with proofs which are combinatorial rather than syntactic. A combinatorial proof is defined by graph-theoretic conditions which can be verified easily (linear time complexity). To be accessible to a broad audience (mathematicians, computer scientists, logicians and philosophers—including undergraduates) the lecture uses many colorful pictorial examples. Niche technicalities (such as relationships with Gentzen’s sharpened Hauptsatz for LK and Herbrandâ€™s theorem) are deferred to the end. The work extends ‘Proofs Without Syntax’ [Annals of Mathematics, 2006], which treated the propositional case.