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

作者：Carbone Alessandra^*

来源：Information and Computation, 2010, 208(5): 500-509.

DOI：10.1016/j.ic.2009.01.007

• Combinatorial proof
• Proof homomorphism
• Skew fibration
• Sequent calculus
• Propositional logic

Combinatorial proofs are abstract invariants for sequent calculus proofs, similarly to homotopy 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 propositional 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.

• 出版日期2010-5