Proving that formulas are BHK-valid

Question

I have been studying Brouwer-Heyting-Kolmogorov (BHK) interpretation lately, and I want to prove that the formulas below are BHK-valid.

1. $(A \vee B) \supset (B \vee A)$
2. $A \supset (B \supset A)$
3. $(A \supset (B \supset C)) \supset ((A \wedge B) \supset C)$
4. $((A \wedge B) \vee (A \wedge C)) \supset (A \wedge (B \vee C))$

I tried to the following for (1), though I don't know whether it is correct.

$\delta$ is a pair $(v, \eta)$ where $v$ is either left and $\eta \rhd \{A\}$ or right and $\eta \rhd \{B\}$.

$\gamma$ waits for input $\delta$ and returns as output the procedure $\pi$. Input for $\pi$ is $\eta$, where $\eta \rhd \{A\}$ or $\eta \rhd \{B\}$. And output of $\pi$ is a proof of $B$ or $A$.

Answer 1

Hint

For (1), I think that, having a proof $\gamma$ of $A \lor B$, i.e.

$\gamma = \langle \nu, \gamma_0 \rangle$, where either $\nu = \text {left}$ and $\gamma_0$ proves $A$ or $\nu = \text {right}$ and $\gamma_0$ proves $B$,

we have a procedure transforming $\gamma$ into

$\gamma' = \langle \nu', \gamma_0 \rangle$, where either $\nu' = \text {left}$ and $\gamma_0$ proves $B$ or $\nu' = \text {right}$ and $\gamma_0$ proves $A$.

Thus, informally, the "procedure" exchanges "left" and "right" from $\nu$ to $\nu'$.

For (2), having a proof $\gamma_0$ of $A$, we can define a procedure $\gamma$ transforming this proof into a proof of $B \supset A$, i.e. into a procedure that, given a proof $\gamma_1$ of $B$, produce the previous proof $\gamma_0$ of $A$.