Talk:Intuitionistic logic

From Wikipedia, the free encyclopedia

Very nice start to the article. A bit POV, though, it's kind of obvious it's written by an advocate of intuitionism. But still good start.

Ummm ... isn't it a bit narrow-based around the assumption of that old chestnut, intuitionism as one of the three main philosophies of mathematics? The Kolmogorov interpretation may have been the first step clear of that. Certainly the Brouwer not not not = not result needs a mention, too. Goedel used IL at one juncture, and after that, historically speaking, wasn't IL respectable in a technical sense? What happened then in relation to Markov was perhaps confusing.

Anyway, there are several strands to disentangle here: this is a bit ahistorical for me.

Charles Matthews 10:36, 15 Oct 2003 (UTC)

Agree on the history issue. For those into completeness, note that the Modal Logic "B" was intended to be a system matching Brouwer's intuition on "not". And that there are direct mappings between Intuitionist PC and the Modal Logic "S4" Nahaj 01:11:29, 2005-09-08 (UTC) And Ian Hacking pointed out in an early paper that there are validity preserving mappings between Intuitionist PC and the Modal Logic "S3" (A weaker system than S4). Nahaj 13:50, 26 October 2005 (UTC)

Contents 1 my take 2 I don't get it. How is this an example? 3 There is no "third, indeterminate truth value" 4 Help me please 5 Not Not Not-p = Not-p?

[edit] my take

Terms should not be equivocated. Speakers end up suggesting that not isn't not, so classical logicians should use a term meaning the exact opposite: un. lysdexia 00:16, 13 Nov 2004 (UTC)

[edit] I don't get it. How is this an example?

In the "law of the excluded middle" example under "Heyting algebra", R² is divvied up into a set A and its complement, the first comprising {(x,y):y > 0}. Now, it would seem to me that the complement of A would be . However, it's given as {(x,y):y < 0}, which is then used to show that the y = 0 plane isn't included in the union of A and not-A. How can this be? grendel|khan 03:45, 2005 Jan 14 (UTC)

It's really badly explained. But the idea is that if you consider subsets of R², they form a Heyting algebra if you consider "or" and "and" to be set union and intersection, and (this is they key point) the complement of X to be the interior of R² − X. Then the complement of the open upper half-plane is the open lower half-plane. The axioms of the Heyting algebra are satisfied in this case, but the law that doesn't hold. -- Dominus 12:30, 14 Jan 2005 (UTC)

I've expanded the explanation (which I think still needs some more work) and included detailed examples of both a valid and and invalid formula. -- Dominus 16:19, 21 September 2005 (UTC)

[edit] There is no "third, indeterminate truth value"

The "Intuitionistic logic as a paradigm for logical reasoning" section presents a reasonably good overview of Intuitionism until we get to the third paragraph. Here we read a common misconception that, because Intuitionism rejects the law of the excluded middle, Intuitionistic logic supports a "third, indeterminate truth value".

Intuitionistic logic does not include any notion of a third truth value. Intuitionists do not believe that there is a formula P such that neither P nor ¬P is true. The reason why Intuitionistic logic rejects the law of the excluded middle has to do with their emphasis on provability. In Intuitionistic logic, the formula A ∨ B asserts that there is a either a proof of A, or there is a proof of B (or both). The law of the excluded middle, in Intuitionic terms, would therefore imply that there is a method by which, for any given formula P, we can generate a proof of either P or a proof of ¬P. Gödel's work dashed any hopes for such a method.

In short, the reason why Intuitionists reject the law of the excluded middle is not because there is a formula P which is neither true nor false. Intuitionists reject this law because there is no general algorithm which can determine which of the two truth values P has.

I move that we either replace or remove the third paragraph of "Intuitionistic logic as a paradigm for logical reasoning". -- Fatherbrain

I agree. I have removed that sentence, which was in the original revision of the article.

I would also like to remove the sentence that says "the validity of a mental construct is dependent upon its coherence with its context (the mind)." I've read this many times and I can't understand what is meant by it. -- Dominus 15:15, 21 September 2005 (UTC)

A similar oddity appears in the truth value article, which says:

A simple intuitionistic logic has truth values of true, false, and unknown

What does that mean? Should it also be removed? -- Dominus 13:26, 22 September 2005 (UTC)

Yes it should. Another correction to be made on this page is when Intuitionist formal logical calculus is contrasted with the "classical, two-valued case". In place of "two-valued", it should say "deterministic". -- FatherBrain 14:28, 22 September 2005 (UTC)

[edit] Help me please

I am doing an assignment at the moment and it is very important that I do well. Can anybody give me a hand with it? I can email the questions otherwise can discuss them one at time here.

Cheers,

Does it say anywhere this is a wiki site, so obviously we help you cheat on your homework? Charles Matthews 07:16, 22 October 2005 (UTC)

And does it say anywhere in my request that I want someone else to do it for me? Sorry if I am not a naturally gifted legend like yourself Charles. You may be shocked to know that some of us have to work hard to get just an average grade and understanding doesn't just happen.

So if there is anyone who can assist me then I would be grateful.

Requests to deal privately by email are pretty suspect, you know. Charles Matthews 21:43, 22 October 2005 (UTC)

The only reason I suggested that was because then both parties would be looking at the same page and be able to discuss the questions much easier. Here is one for you then; I need to prove a theorem in intuitionistic propositional calculus, the question ask that you "indicate what axioms and inference rules" are used. I was under the impression that modus ponens was the only inference rule of intuitionistic calculus, however to procede with this proof "and elimination" would be handy. As the question refers to "inference rules" I was hoping I had missed something and there were more available to use.

Your thoughts?

Substitution is a rule of Intuitionist calculus (although not normally called an inference rule). While Modus Ponens is the basic inference rule of most calculi, most have a number of "derived rules" such as adjunction and substitution of equivalents. What counts as a rule needing to be given in your assignment depends on what your instructor has already given and what he has said. Obviously we don't know this. You could find therefore that an answer you get here (while in some sense "correct") is wrong for your assignment. Nahaj 21:03, 25 October 2005 (UTC)

There is an alternative to this: instead of a number of explicit axioms together with a substitution rule, one gives axiom schemes that determine an infinite set of individual axiom instances. Having a substitution rule is usual in modal logic, having axiom schemes seems most common elsewhere. --- Charles Stewart 21:22, 25 October 2005 (UTC)

Postscript: IIRC, Hilbert and Ackermann's Principles of Theoretical Logic uses axiom schemes. --- Charles Stewart 21:24, 25 October 2005 (UTC)

In the early days of Modal Logic, Axiom Schemata were VERY common. (And also rules like Adjunction, that were later proved to be derived rules in most systems of interest.) But by about the 1960's or so substitution had become more common in that field. In automated theorem proving substitution is more common, although a lot of recent automated work has used Condensed Detachment, which can be looked at as a (constrained) substitution followed by Modus Ponens. -- Nahaj 02:11, 30 October 2005 (UTC)

[edit] Not Not Not-p = Not-p?

Somebody mentioned aboved that this was a very fruitful result of Brouwer's. Which paper of Brouwer's discusses the importance of this fact in relation to intuitionist logic? (How does he argue it?)