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.
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!