Alejandro Díaz-Caro (Villetaneuse, France), Equivalence on propositions and proofs


  • Feb. 23, 2012, 10:40 - 11:20


(Joint work with Gilles Dowek)

We know that the propositions A∧B and B∧A are equiprovable: one is provable if and only if the other is, but they do not have the same proofs. Here we design a proof system such that they have the same proofs, i.e. we take the quotient of the set of propositions by the relation generated by the commutativity of conjunction, and define proofs for elements in this quotient. The calculus obtained is similar to the additive fragment of the algebraic lambda-calculi plus a non-deterministic projector.