understanding intuitionistic logic

Question

Just started a chapter on Intuitionism, and already I'm kinda confused on how to structure a proof in favor of intuitionistic logic. Here are the following definitions I am supposed to use:

Intuitionistic logic definitions:

And so I made an attempt at the two following practice exercises from my textbook. They are classically valid but I am two show that they are also intuitionistically valid.

Exercise 1. ¬X v ¬Y => ¬(X & Y)

Attempt for 1: If we have a proof of the premise, then we have either a proof of ¬X or a proof of ¬Y. Assume now that we are given a proof of X. It follows that our first proof could not have been a proof of ¬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 ¬X and the other a proof of ¬Y.

Exercise 2:

Attempt for 2: Assume we are given a proof of its premise, then we have a proof that for some n, ¬Fn and for every n, we have either a proof of Fx or ¬Fx. Using (9)(vi), we have a proof of a particular substitution, say ¬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 ¬Fk, yields a proof of 0 = 1.

I am expecting for my attempts to make no sense at all as I did what I could to try to explain them intuitionistically. All help is greatly appreciated!

Answer 1

An interesting thing to point out is that the "rules" you have correspond to what we call BHK Interpretation.

Exercice 1

The main problem is that you don't use the new meaning given to the negation ¬ (different from the classical logic).

• First, you should understand the implication A ⇒ B as a "transformer" from a proof of A to a proof of B. When you work with implications as A ⇒ B, first suppose A then prove B.

• The negation ¬A is A ⇒ 0. You should make use of that.

Intuition : Suppose that we have a proof of (X & Y) and take 0 as your new "goal". Use "function application" to solve the problem.

Exercice 2

Hum...I don't understand why you wrote the first part of your attempt. It doesn't seem to be related to the question you suggest later. It seems to me that (c) is an inference rule. That is, given the top part you can infer the bottom part (forward reasoning).

There's also an alternative reading from bottom to top : if you want to prove the bottom part you have to prove the top part (backward reasoning).

For your last question, it seems that you're using the principle of explosion. But in my opinion the right thing to do is to see (∀x.Fx) as a transformer : given an object x, it gives a proof of Fx (you can produce any Fx, including 0 = 1, with the inference rule (c) you have).

I may be wrong since I'm not sure to be right about my interpretation for your second exercise.