Show formulas which are valid according to Brouwer-Heyting-Kolmogorov interpretation

Question

How can I show, that the following formulae are valid according to Brouwer-Heyting-Kolmogorov interpretation?

$(A \land B) \to (B \land A)$

$\neg (A \lor B) \to (\neg A \land \neg B)$

$A \land (B \lor C) \to ((A \land B) \lor (A \land C))$

Answer 1

The BHK interpretation says that given formulae $\phi$ and $\psi$ a proof of:

• $\phi \land \psi$ is a proof of $\phi$ concatened with a proof of $\psi$;
• $\phi \lor \psi$ is a proof of $\phi$ or a proof of $\psi$;
• $\phi\to \psi$ is a 'method' that transforms a proof of $\phi$ in a proof for $\psi$;
• $\neg \phi$ is 'method' that transforms any proof of $\phi$ in a proof of $\bot$;
• There is no proof of $\bot$.

Informally it goes something like this:

$\boxed{(A\land B)\to (B\land A)}$

Here you have a conditional statement, so you need to find a method that takes a proof of $A\land B$ to a proof of $B\land A$. A proof of $A\land B$ is a proof of $A$ concatenated with a proof of $B$, so 'swapping' the proofs gives a concatenation of a proof of $B$ concatenated with a proof of $A$, that is, a proof of $B\land A$. The swapping of the proofs is your 'method'.

$\boxed{\neg (A\lor B)\to (\neg A\land \neg B)}$

Given a method$\large_1$ that transforms any proof of $A\lor B$ in a proof of $\bot$, the goal is to find a proof of $\neg A$ and a proof of $\neg B$. To find a proof of $\neg A$ is to find a method$\large_2$ that transforms any proof of $A$ in a proof of $\bot$. Given a proof of $A$, there is a proof of $A\lor B$, therefore method$\large _1$ gives you a proof of $\bot$. Letting method$\large _2$ be the method described in the previous sentence, gives you a method that transforms a proof of $A$ in a proof of $\bot$, thus yielding a proof of $\neg A$. Similarly for $\neg B$. Concatenating the proofs of $\neg A$ and $\neg B$ yields a proof of $\neg A\land \neg B$.

$\boxed{A \land (B \lor C) \to ((A \land B) \lor (A \land C))}$

Given a proof of $A\land (B\lor C)$, you have a proof of $A$ and a proof of $B\lor C$. The goal is to find a proof of $A\land B$ or a proof of $A\land C$. Since you have a proof of $B\lor C$, you either have a proof of $B$ or a proof of $C$. But since you have a proof of $A$, you'll have a proof of $A$ and $B$ or a proof of $A$ and $C$, i.e., you'll have a proof of $A\land B$ or a proof of $A\land C$, thus getting a proof of $(A\land B)\lor (A\land C)$. The method implied here is the concatenation of the proof of $A$ with either the proof of $B$ or the proof of $C$.