Event Detail

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.