Combinatorial Proofs and Decomposition Theorems for First-order Logic

Dominic Hughes, Lutz Straßburger, Jui-Hsuan Wu

We uncover a close relationship between combinatorial and syntactic proofs for first-order logic (without equality). Whereas syntactic proofs are formalized in a deductive proof sy…