Show formulas which are valid according to Brouwer-Heyting-Kolmogorov interpretation 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))$
 A: 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$.
