Proof Normalisation in a Logic Identifying Isomorphic Propositions

Abstract

We define a fragment of propositional logic where isomorphic propositions, such as $A\wedge B$ and $B\wedge A$, or $A\Rightarrow (B\wedge C)$ and $(A\Rightarrow B)\wedge (A\Rightarrow C)$ are identified. We define System I, a proof language for this logic, and prove its normalisation and consistency.