First-order Proofs Without Syntax: Summary of Work in Progress

ABSTRACT. "...mathematicians care no more for logic than logicians for mathematics." - Augustus de Morgan, 1868

Formal proofs are traditionally syntactic, build inductively from symbolic inference rules. This paper reformulates classical first-order logic with proofs which are combinatorial rather than syntactic. A combinatorial proof of a formula F is a graph on a variant formula F′ which satisfies geometric properties. For example, an edge between the two Ps in ∀xPx ⇒ ∀yPy constitutes a combinatorial proof o ∃x(P ⇒∀yPy).

Combinatorial proofs provide a canonical abstraction of Gentzen’s sequent calculus LK: the correctness of a combinatorial proof can be verified in polynomial time (conjectured linear), and there is a function from LK proofs to combinatorial proofs which identifies many LK proof.

This paper summarizes ongoing work on a sequel to Proofs Without Syntax [Annals of Mathematics, 2006], which introduced propositional combinatorial proofs.