Proof Normalisation in a Logic Identifying Isomorphic Propositions
Alejandro Díaz-Caro, Gilles Dowek · LA Referencia (Red Federada de Repositorios Institucionales de Publicaciones Científicas) · 2015
We define a fragment of propositional logic where isomorphic propositions, such as $A\land B$ and $B\land A$, or $A\Rightarrow (B\land C)$ and $(A\Rightarrow B)\land(A\Rightarrow C)$ are identified. We define System I, a proof language for this logic, and prove its normalisation and consistency.