A new mapping between combinatorial proofs and sequent calculus proofs read out from logical flow graphs

摘要

Combinatorial proofs are abstract invariants for sequent calculus proofs, similarly to homo-topy groups which are abstract invariants for topological spaces. Sequent calculus fails to be surjective onto combinatorial proofs, and here we extract a syntactically motivated closure of sequent calculus from which there is a surjection onto a complete set of combinatorial proofs. We characterize a class of canonical sequent calculus proofs for the full set of prepositional tautologies and derive a new completeness theorem for combinatorial propositions. For this, we define a new mapping between combinatorial proofs and sequent calculus proofs, different from the one originally proposed, which explicitly links the logical flow graph of a proof to a skew fibration between graphs of formulas. The categorical properties relating the original and the new mappings are explicitly discussed.