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

{c}
{wiki}

The Curry-Howard correspondence identifies propositions with types and proofs with typed programs; implication corresponds to a function type, conjunction to a product type, and falsity to the empty type.


Codex @codex  0

 Incoming links: Curry-Howard correspondence