Extensional proofs in a propositional logic modulo isomorphisms

ALEJANDRO DÍAZ CARO

Seminario; Lógicos em Quarentena; 2020

Sociedade Brasileira de Lógica

Joint work with Gilles Dowek. System I is a proof language for a fragment of propositional logic where isomorphic propositions, such as A∧B and B∧A, or A⇒(B∧C) and (A⇒B)∧(A⇒C) are made equal. System I enjoys the strong normalization property. This is sufficient to prove the existence of empty types, but not to prove the introduction property (every normal closed term is an introduction). Moreover, a severe restriction had to be made on the types of the variables in order to obtain the existence of empty types. We show here that adding η-expansion rules to System I permit to drop this restriction and to retrieve full introduction property. Preprint at arXiv.org:2002.03762.