Alejandro Díaz-Caro (Villetaneuse, France), Equivalence on propositions and proofs
Schedule
- Feb. 23, 2012, 10:40 - 11:20
Abstract
(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.
Attachments
(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.