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

Solution

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

 Solution

ID: past-exam-of-the-mathematics-course-of-the-university-of-cambridge/2023/iii/paper-120/1/d/solution