I am at the very beginning of this intuitionistic_logic theory and would appreciate any help if someone could give me concerning the following.
Namely, I am supposed to prove that conjunction is associative by deriving a proof of the formula $(A \wedge B) \wedge C \to A \wedge (B \wedge C)$.
Okay, from the left hand side I know that if $(A \wedge B) \wedge C$ holds, then I may denote, for example, with $p$ to be the proof of conjunction $A \wedge B$ and denote by $q$ the proof of $C$.
Furthermore, $p$ can be written in ordered pair form such that $p=(p_1,p_2)$ where both $p_1$ and $p_2$ denote component proves of $A$ and $B$ respectively.
But here I get stuck and don't know where to go next.
Thanks in advance for any help
A proof of $(A \land B) \land C)$ is a pair $(p, q)$ where $p$ is a proof of $A \land B$ and $q$ is a proof of $C$. Since $p$ is a proof of $A \land B$, $p$ is $(p_1, p_2)$ where $p_1$ is a proof of $A$ and $p_2$ is a proof of $B$.
Then, indeed, we can specify a method for turning a proof of the proposed antecedent $(A \land B) \land C$ to a proof of the proposed consequent $A \land (B \land C)$. We have a function from a proof of the antecedent to a proof of the consequent. This is what it means to have a proof of a conditional $\to$ in the BHK interpretation.
Map $((p_1, p_2), q)$ to $(p_1, (p_2, q))$. Then we have a pair that is a proof of $A$ and a proof of $B \land C$. So we have a proof of $(A \land B) \land C \to A \land (B \land C)$.
There shouldn't be much more to it than that. I'm not sure which formalism (and how loose I can be with the notion of "function" / "method" / "map") the book you're using endorses, but this doesn't seem too objectionable.