0

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.

  • But we don't need a proof of $ B $ since it is not in the conclusion, right? Do you understand the general method of the proof? (also lambda calculus might be a little bit more than just interesting in this particular field, you should try to learn it beforehand) – Josselin Poiret Nov 02 '16 at 22:45
  • "Do you understand the general method of the proof?" Perhaps, not. –  Nov 02 '16 at 22:52
  • Have you ever had any experience with typed languages or programming in general? Otherwise this paper might be a little too quick on the basics. – Josselin Poiret Nov 02 '16 at 22:54
  • Yes, I am programmer. –  Nov 02 '16 at 23:01

1 Answers1

0

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.

Mitchell Spector
  • 9,917
  • 3
  • 16
  • 34
  • Thanks! Especially for Turing's context. Now, I understand why it is common writing a "constructive procedure" as lambda expression! –  Nov 03 '16 at 19:49