Proof interpretation for: The citation comes from: http://aleteya.cs.buap.mx/~jlavalle/papers/van%20Dalen/Intuitionistic%20Logic.pdf
$$ A \implies (B \implies A) $$ We want an operation $p$ that turns a proof $a : A$ into a proof of $B \implies A $. But if we already have a proof $a : A$ then there is a simple transformation that turns a proof $q : B$ into a proof of $A$, i.e. the consant mapping $q \to a $ which is denoted $\lambda q \dot a$
I cannot grasp it. We can skip lambda expressions because I don't know lamda calculus. Especially, where from we know that there is a proof $a$ for $B$.
In this way we can prove:
$ A \to B $. Let $a $ is a proof for $A$ and $b$ is a proof for $B$. Now, let $p$ will be a simple map $p: a \to b $. And that is.
This is actually quite simple in principle, but the details end up looking elaborate. The basic idea is that if you have a proof of $A,$ then you can turn any proof of $B$ into a proof of $A$ by just ignoring the proof of $B$ and writing down the proof of $A$ which you have.
Here are the details:
In intuitionistic logic, a proof of $"\!P\implies Q\!"$ is a constructive procedure (read "Turing machine") $T$ together with a proof of the following:
If we run the Turing machine $T$ with an input string that happens to be a proof of $P,$ then $T$ will eventually halt and the string on the tape will be a proof of $Q.$
So a proof of $"\!A\implies (B\implies A)\!"$ is a Turing machine $T$ together with a proof of the following:
If we run the Turing machine $T$ with an input string that happens to be a proof of $A,$ then $T$ will eventually halt and the string on the tape will be a proof of $"\!B\implies A\!".$
Expanding inside here what a proof of $"\!B\implies A\!"$ is, this means that a proof of $"\!A\implies (B\implies A)\!"$ is a Turing machine $T$ together with a proof of the following:
If we run the Turing machine $T$ with an input string that happens to be a proof of $A,$ then $T$ will eventually halt and the string on the tape will be:
A representation of a Turing machine $U$ together with a proof that shows that if we feed any proof of $B$ as input to $U,$ then $U$ will halt with its tape showing a proof of $A.$
This is true; here's a Turing machine $T$ that satisfies the above criterion:
For any input string $x,$ $T$ outputs a representation of a Turing machine $U_x$ and possibly also a string $p$ that happens to be a proof. Here's what $U_x$ does: it deletes its input string from the tape and writes $x$ to the tape. To determine $p,$ $T$ also checks to see whether $x$ is a valid proof of $A$ (by checking to see whether $x$ meets the formal criteria for a proof and ends in $A)$ and, if so, spells out a proof $p$ that this particular machine $U_x$ always outputs $x$ and that $x$ is a proof of $A.$
Proving the italicized statement above is a bit unwieldy, but it's just unravelling the definitions.