5
$\begingroup$

Just started a chapter on Intuitionism, and already I'm kinda confused on how to structure a proof in favor of intuitionistic logic.

And so I made an attempt at the two following practice exercises:

  1. $\neg X \lor ¬Y \implies \neg(X \land Y)$

Attempt for 1: If we have a proof of the premise, then we have either a proof of $\neg X$ or a proof of $\neg Y$. Assume now that we are given a proof of $X$. It follows that our first proof could not have been a proof of $\neg X$: for that would be a proof that $X$ cannot be proved, and we are assuming that we have just been given a proof of $X$. So our first proof must in fact been a proof of $\neg X$ and the other a proof of $\neg Y$.

  1. $\cfrac{\neg\exists x\neg F x \quad \forall x(Fx \lor \neg F x)}{\forall x Fx}$

Attempt for 2: Assume we are given a proof of its premise, then we have a proof that for some $n$, $\neg F n$ and for every $n$, we have either a proof of $Fx$ or $\neg Fx$. Using (9)(vi), we have a proof of a particular substitution, say $\neg Fk$. The question is whether there is an operation that transforms every proof of for all $x$, $F(x)$ into a proof of $0 = 1$. There is: given a proof of the universal quantification, apply it to generate a proof of $Fk$; this, together with the proof of $\neg Fk$, yields a proof of $0 = 1$.

All help is greatly appreciated!

$\endgroup$
2
  • $\begingroup$ The images are not loading. Can you try to upload them again? $\endgroup$ Commented Feb 28, 2017 at 17:48
  • $\begingroup$ No these links are not working on my computer. If they are pages from a book maybe you can tell me the name of the book? $\endgroup$ Commented Feb 28, 2017 at 18:00

1 Answer 1

Reset to default
4
$\begingroup$

The BHK (Brouwer-Heyting-Kolmogorov) interpretation (the one you describe) sees statements as proofs of these statement. So the way you need to reason is the following: If I want to show that from a statement $X$ I can conclude statement $Y$, then I need to show that if I have a proof of statement $X$ I can describe a proof for statement $Y$.

Let's start from an easy example. I want to show $P\to P\lor Q$. So I want to show that I can find a proof of $P\to P\lor Q$. By definition, I need to come up with an operation that takes a proof of $P$ and transforms it into a proof of $P\lor Q$. A proof of $P\lor Q$ is either a proof of $P$ or a proof of $Q$. So what would that operation be? In this case it's quite simple, the operation does nothing. It takes a proof of $P$ and gives me back the same proof. Now this proof of $P$ is also a proof of $P\lor Q$ (by the definition of the proof of $P\lor Q$).

Now let's look at the derivations that you have in your question. Assuming $\lnot X\lor\lnot Y$ I want to conclude $\lnot(X\land Y)$ (that is, assuming that I have a proof of $\lnot X\lor\lnot Y$) to find a proof of $\lnot(X\land Y)$).

So first of all think of what it is that you need to come up with: A proof for $\lnot(X\land Y)$ is by definition of proof of $X\land Y\to 0=1$, or (again using the definition) an operation that takes a proof of $X\land Y$ and gives a proof of $0=1$.

Now let's look at what we have. We have a proof of $\lnot X\lor\lnot Y$, that is either a proof of $\lnot X$ or a proof of $\lnot Y$.

Let's assume that we have a proof of $\lnot X$. This means that we have an operation $O_x$ that takes a proof of $X$ and gives us a proof of $0=1$. Can we use this operation to produce an operation that takes a proof of $X\land Y$ and produces a proof of $0=1$? Sure, a proof of $X\land Y$ is a proof of $X$ and a proof of $Y$. So if I have a proof of $X$ and a proof of $Y$ I can use operation $O_x$ on the proof of $X$ to find a proof $0=1$. What I just described is an operation that takes a proof of $X\land Y$ and gives a proof of $0=1$.

So now let's assume that we have a proof of $\lnot Y$. Can you come up with an operation that takes a proof of $X\land Y$ and gives you a proof of $0=1$?

The second example should be similar:

We assume that we have a proof of $\lnot\exists x\lnot Fx$ (what does that mean? try to break this down) and a proof of $\forall x(Fx\lor\lnot Fx)$ and we need to find a proof of $\forall x Fx$ (that is an operation that takes every element $n$ and and gives a proof of $Fn$.

I hope this will help you understand a little better the BHK interpretation. If things are unclear let me know and I will try to provide more details.

$\endgroup$
3
  • $\begingroup$ @M.Alexander There is no major difference, the answer would be quite symmetric (but not exactly the same, because now you don't have an operation that yields a proof of $0=1$ from a proof of $X$ but rather from a proof of $Y$). $\endgroup$ Commented Feb 28, 2017 at 20:17
  • $\begingroup$ @M.Alexander I don't understand why you assume that we have a proof of $Y$. You have a proof of $\lnot Y$. That means by the definition that you have an operation that takes a proof of $Y$ and gives a proof of $0=1$. Can you now find an operation that takes a proof of $X\land Y$ and gives a proof of $0=1$? This is what you need to do. $\endgroup$ Commented Feb 28, 2017 at 21:31
  • $\begingroup$ @M.Alexander Yes this is correct. $\endgroup$ Commented Mar 1, 2017 at 9:51

You must log in to answer this question.

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.