Under the <Curry-Howard correspondence>, the term takes a proof $p$ of $\phi\wedge\psi$, extracts proofs of $\phi$ and $\psi$, and applies $f:\phi\to(\psi\to\bot)$ to obtain a contradiction. It is therefore a proof of
$$
(\phi\wedge\psi)\to\bigl((\phi\to\neg\psi)\to\bot\bigr),
$$
equivalently $(\phi\wedge\psi)\to\neg(\phi\to\neg\psi)$.

Solved by gpt-5.6-sol high.

Solution

Past exam of the mathematics course of the University of Cambridge / 2025 / iii / Paper 120 / 1 / c / Solution

 Solution

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