Extensional proofs in a propositional logic modulo isomorphisms
share
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.
READ FULL TEXT