Talk:Intuitionistic logic

From Wikipedia, the free encyclopedia

Mathematics Portal

This article is within the scope of WikiProject Mathematics, which collaborates on articles related to mathematics.

Mathematics rating:

Start Class

High Priority

Field: Foundations, logic, and set theory

Please update this rating as the article progresses, or if the rating is inaccurate. Click to show/hide comments.
Please add to or update the comments to suggest improvements to the article.
A better lead (overview), more references, and greater accessibility would help. Geometry guy 23:07, 22 June 2007 (UTC)

Philosophy Portal

This article is within the scope of the WikiProject Philosophy, which collaborates on articles related to philosophy. To participate, you can edit this article or visit the project page for more details.

Start

This article has been rated as Start-Class on the quality scale.

Low

This article has been rated as low-importance on the importance scale.

Additional information:

Related task forces (core areas):
	Logic

1 comment by Charles Matthews
2 my take
3 I don't get it. How is this an example?
4 There is no "third, indeterminate truth value"
5 Help me please
6 Not Not Not-p = Not-p?
7 Paradox of entailment
8 WikiProject class rating
9 Something wrong?
10 Heyting algebra of open subsets of R
11 Can't read it

[edit] comment by Charles Matthews

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)

[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 2$ 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 $\{(x,y) : y\le0\}$ . 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 2

, 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 2 - 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 $X\vee\not X = R^2$ 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?) —Preceding unsigned comment added by 71.232.7.49 (talk • contribs) 00:41, July 23, 2006 (UTC)

[edit] Paradox of entailment

In the mathematical proof of the paradox of entailment I've seen, the axiom "if not not a then a" is used. Since this axiom doesn't exist in intuitionist logic, does that mean an inconsistency can arise without allowing every possible theorem, consistent or not, to be proved? If so, wouldn't this greatly decrease the problem in such a circumstance? Allowing some contradictions would allow certain metamathematical theorems such as Gödel's incompleteness theorems to be avoided. — Daniel 01:36, 5 June 2007 (UTC)

The logic that is usually called "intuitionistic logic" does have that property. Intuitionistic logic has an extra symbol $\bot$ which means false, and inference rules:

$\phi \land \lnot \phi \rightarrow \bot$

$\bot \rightarrow \psi$

From these, it follows immediately that if you have already shown $\phi \land \lnot \phi$ then you can infer

ψ

Another way of looking at the paradox of entailment is that it follows from the fact that $\phi \rightarrow (\lnot \phi \rightarrow \psi)$ is a tautology. That identity is also valid in intuitionistic logic, using the above inference rules. — Carl (CBM · talk) 01:50, 5 June 2007 (UTC)

Why'd they do that? They could have had a sufficiently complex complete logical system, but they just couldn't stand a contradiction. I don't see how it could do any good. It's better to have one contradiction then every one that could possibly be stated. By the way, why even have $\bot$ ? Why not just use

ψ

? It looks to me like they're equivalent and both mean "everything is true". I don't see how $\bot$ could mean false. You wouldn't say, "if false, Elvis is alive"; you would say, "if everything is true, Elvis is alive"… assuming you're the kind of guy who likes to state the obvious. Besides, I'm pretty sure $\bot$ means perpendicular. — Daniel 04:00, 5 June 2007 (UTC)

[edit] WikiProject class rating

This article was automatically assessed because at least one WikiProject had rated the article as start, and the rating on other projects was brought up to start class. BetacommandBot 04:08, 10 November 2007 (UTC)

[edit] Something wrong?

In the Heyting algebra section, it is stated that the values of intuitionist logic can be taken to be open sets, and later that negation is taking the exterior of the set. But then, the exterior of the exterior of an open set A is A itself; with the obvious muddle about negatives. —Preceding unsigned comment added by 92.50.68.238 (talk) 19:05, 10 March 2008 (UTC)

Your claim that ext(ext(S)) = S is mistaken. One can only show that ext(ext(S)) is a subset of S, but not conversely. Consider the set S = R - {(0,0)}. This is an open set. Then the exterior of S is empty, and the exterior of the empty set is not S but R. So we have a counterexample for $\neg\neg x \rightarrow x$ . But because ext(ext(S)) is contained in S one can show that $x \rightarrow\neg\neg x$ does hold. -- Dominus (talk) 19:19, 10 March 2008 (UTC)

Actually it's the other way round (as your example shows): every open S is contained in ext(ext(S)), but ext(ext(S)) may be strictly larger than S. Indeed, ext(ext(S)) = S holds if and only if S is a regular open set. For a general open set S, ext(ext(S)) is its regularization. -- EJ (talk) 13:55, 11 March 2008 (UTC)

Ok, my mistake. Is there a logic that corresponds to regular open sets? —Preceding unsigned comment added by 81.210.250.222 (talk) 19:29, 28 March 2008 (UTC)

Yes, it is classical logic. -- EJ (talk) 10:54, 31 March 2008 (UTC)

I mean, a "logic that corresponds to regular open sets" can be understood in two different ways:

The logic of the algebra of regular open sets in a topological space. This is classical logic, as the algebra is Boolean. The join in this algebra is $A\lor B={\rm int}(\overline{A\cup B})={\rm ext}({\rm ext}(A\cup B))$ .
The "logic" obtained by evaluating propositional variables by regular open sets, but evaluating connectives as in intuitionistic logic. In this case, compound formulas may have nonregular sets as their value. This "logic" is not a logic at all, as it is not closed under substitution. It is the propositional intuitionistic theory axiomatized (over Int) by the formulas ¬¬p → p for all variables p. Equivalently, it can be described as the set of all formulas A(p₁,…,p_n) such that A(¬p₁,…,¬p_n) is an intuitionistic tautology. The logic of this theory (i.e., the set of formulas whose all substitution instances are theorems) is just intuitionistic logic. -- EJ (talk) 15:43, 31 March 2008 (UTC)

[edit] Heyting algebra of open subsets of R

What is a reference for the statement that the Heyting algebra of open subsets of R suffices for characterizing validity? --Lambiam 14:04, 13 March 2008 (UTC)

The original paper is apparently

Alfred Tarski, Der Aussagenkalkül und die Topologie, Fundamenta Mathematicae 31 (1938), 103–134. [1]

In fact, he shows that intuitionistic logic is complete with respect to any second countable T₄ dense-in-itself space. I am not able to find an English reference ATM; there is a chance that it is in Rasiowa's and Sikorski's "Mathematics of Metamathematics". The more general result of completeness of S4 wrt the reals can be found here[2] for instance. -- EJ (talk) 15:00, 13 March 2008 (UTC)

Funny than you should ask this just now: I was going to add a cite for this yesterday, but then I got distracted while I was looking at [[3] and didn't finish. The fact can be supported with Sørensen and Urzyczyn's "Lectures on the Curry-Howard Isomorphism". I will try to hunt this up and add a reference today. -- Dominus (talk) 15:19, 13 March 2008 (UTC)

This is theorem 2.4.8 on page 33 of the lecture note version of Sørensen and Urzyczyn. A remark higher up on the same page asserts that "there is no single finite Heyting algebra [that is a sufficient model for intuitionistic logic]". Presumably the same assertions appear in ^[1] but I don't have it handy just now. I will see if I can find a copy. -- Dominus (talk) 15:37, 13 March 2008 (UTC)

Sørensen and Urzyczyn cite Rasiowa and Sikorski.^[2] -- Dominus (talk) 15:40, 13 March 2008 (UTC)

The Penn library has ^[2] but not ^[1]. I've ordered the second from interlibrary services, and the first to be extracted from storage. I should be able to provide references some time next week. -- Dominus (talk) 15:54, 13 March 2008 (UTC)

I added an English reference, but, strangely, I was not able to find where it proved that no finite Heyting algebra is a model for the intuitionistic validity of all sentences. -- Dominus (talk) 17:06, 14 March 2008 (UTC)

In addition to the Tarski paper cited above, ^[2] also cites the earlier paper ^[3]. -- Dominus (talk) 17:02, 14 March 2008 (UTC)

The whole thing is now cited up down and backwards. -- Dominus (talk) 19:18, 18 March 2008 (UTC)

^ ^a ^b Sørensen, Morten Heine B; Pawel Urzyczyn (2006). Lectures on the Curry-Howard Isomorphism. Elsevier. ISBN 0444520775.
^ ^a ^b ^c Rasiowa, Helena; Roman Sikorski (1963). The Mathematics of Metamathematics, Monografie matematyczne. Warsaw: Państwowe Wydawn. Naukowe.
^ Stone, M. H. (1937). "Topological representation of distributive lattices and Brouwerian logics". Čas. Mat. Fys. 67.

[edit] Can't read it

My browser is showing the syntax section as '... it is customary to use →, ∧, ∨, ⊥ as the basic connectives ...' and so on through the article. Never happened to me on Wikipedia before. Obviously, this makes the article completely unreadable. Any chance of fixing it? —Preceding unsigned comment added by 195.224.69.116 (talk) 16:07, 14 March 2008 (UTC)

Do you mean that you see little boxes instead of the actual symbols? — Carl (CBM · talk) 16:56, 14 March 2008 (UTC)

Yes —Preceding unsigned comment added by 195.224.69.116 (talk) 15:47, 9 April 2008 (UTC)

Which of these work for you:

$\land$ - ∧ - ∧

φ

- φ - φ

— Carl (CBM · talk) 19:52, 10 April 2008 (UTC)

In the HTML produced for the page, the first wedge comes out as a png image, while the other two are both utf8 for Unicode Character 'LOGICAL AND' (U+2227). This should be the same for any viewer who has not set their Math rendering preference to "HTML if possible". The inability to see this should imply that also Logical connective#Order of precedence, for example, is totally unreadable. --Lambiam 21:07, 11 April 2008 (UTC)