Past exam of the mathematics course of the University of Cambridge / 2023 / iii / Paper 120 / 1 / d

Both sequents follow directly from the introduction and elimination rules of the implication-free fragment of intuitionistic propositional logic. From a proof of $\varphi \wedge (\psi \vee \chi )$, eliminate the conjunction to obtain $\varphi$ and $\psi \vee \chi$. Eliminate the disjunction: in the $\psi$ branch introduce $\varphi \wedge \psi$ and then the left disjunct; in the $\chi$ branch introduce $\varphi \wedge \chi$ and then the right disjunct. This yieldsConversely, eliminate the outer disjunction. From $\varphi \wedge \psi$, obtain $\varphi$ and introduce the left side of $\psi \vee \chi$; from $\varphi \wedge \chi$, obtain $\varphi$ and introduce its right side. In either branch, conjunction introduction produces $\varphi \wedge (\psi \vee \chi )$. HenceThis is the proof-theoretic form of the distributive law for lattices.