Talk:Law of excluded middle/Archive 3

From Wikipedia, the free encyclopedia

This is an archive of past discussions. Do not edit the contents of this page. If you wish to start a new discussion or revive an old one, please do so on the current talk page.

Contents 1 Brouwer examples 2 Reduction of Hilbert's 2nd negation 3 Equivalence of the generalization, versus generalization of the equivalence 4 Lambiam's exposition 5 Citations, comments etc on the above 5.1 W.S. Anglin’s exposition

Brouwer examples

He offers examples of failures that result from "...incorrect 'logical" mathematics of infinity ('logical' because it makes use of the princple of excluded middle)" (p. 337) One example that might be familar to students of analysis (the convergence of infinite series) (p. 339) he claims "rests on the Bolzano-Weierstrass theorem and must be rejected along with it" (p. 340).

. The thread is this: he claims "the Paris school" asserts that "every mathematical species is either finite or infinite" and in his footnote 4 to this asserts "For according to the principle of excluded middle a species s either is finite or cannot possibly be finite [etc]". From this derives what he calls the "extended disjunction principle" [union of two sets contains a "fundamental sequence of elements"], and when this fails, the Bolzano-Weierstrass theorem fails "which rests upon it and according to which every bounded infinite point species has a limit point" (p.337)

Reduction of Hilbert's 2nd negation

[What a mess -- just to see what is going on:

(A->B) -> {(~A -> B)-> B}

1 (A->B) -> {~(~A -> B) V B}

2 (A->B) -> {~(~(~A) V B) V B}

3 (A->B) -> {(~(~(~A)) & ~B) V B}

4 (A->B) -> {(~(~(~A)) V B) & (~B V B)}

If we believe that (~B V B) = ALWAYS TRUE, then we have:

5 (A->B) -> {(~(~(~A))V B) & (TRUE)}

We are asserting here that X & (TRUE) is X

6 (A->B) -> {(~(~(~A))V B)}

If we believe that ~(~A) <-> A then we have:

7 (A->B) -> {(~(A) V B)}

And the implication holds as a tautology. Observe that two assumptions are made. One regarding ~B V B)=ALWAYS TRUE and the other regarding ~(~A)<->A. Is his a source of Brouwer's retraction? Which one dominates? Are they really two issues?

If you assume intuitionistic logic, then excluded middle (for any proposition, either A or not-A) follows from double negation elimiation (for any proposition A, if not-not-A, then A), and vice versa. In particular, for any proposition A, ~(~(A v ~A)) is a theorem, in your notation. I'm not sure if that's what you were asking. -Dan 17:23, 5 June 2006 (UTC)

Not exaclty...On the article page I (well, actually, Bertrand Russell...) derived the double-negative from the LoEM. I wrote the above derivation before I (-as-Bertrand) wrote the stuff in the article. But actually the little derivation above is out of place. It used to be under a quote re Brouwer in the 1950's retracting [?, modifying?] his position relative to the "equivalence" of the LoEM and the double negative. But to read his paper and find out what he was up to--the collection of Brouwer's works is out of print and probably cost $100 or more if you can find one -- we will have to crawl deep dark recesses of moldy dusty stacks of a good math library. It probably isn't worth the resultant breaking out in hives or a sneazing fit. My guess is it has to do with definitions of truth and falsity and "testing" and "reducing to absurdity' [to quote Brouwer] and "correct or impossible [to quote Brouwer], and verifying and stuff that I, personally, am finding just too silly. Ferchrissake: "Marks is marks, 'n a mind -- or one o' them newfangled machines-- hasta be there to put meanin' to 'em. There ain't no such a thang as marks with intrinsic meanin'. They's just marks. There ain't no such thang as anythin' a-tall', not even that-there blue sky out yer window, not them number-thangs you fret about, no fancy law of exculpated middle, no nothin' a-tall, without a mind or a machine to be lookin' at it an' puttin' a meanin' to it."wvbaileyWvbailey 18:37, 5 June 2006 (UTC)

I am not aware of Brouwer's retraction... -Dan 20:44, 5 June 2006 (UTC)

Here 'tis:

The fourth insight comes from an earlier paper of Brouwer's (1927o) where, in a footnote he asserts, and then he partially retracts in 1953 (my boldface):

"...A second argument is the way in which Hilbert seeks to settle the question ...of the reliability of the principle of excluded middle is a vicious circle; for, if we wish to provide a foundation for the correctness of this principle by means of the proof of its consistency, this implicitly presupposes the principle of the reciprocity of the complementary species and hence the principle of excluded middle itself (see Brouwer 1923c. p. 252) [Brower (1953, p. 14, footnote 1) writes "the equivalence of the principles of the excluded third and of reciprocity of complementarity ... subsequently has been recognized as nonexistent. In fact, as was also shown in the present paper, the fields of validity of these two principles have turned out to be essentially different]"(p 460)

This is the paper I'm not willing to go sniffing after in the tombs: Brouwer, "Points and Spaces", Canadian Journal of Mathematics, 6 (1954), 1-17. Footnote #1.

I'm with Dan here. As I wrote earlier on the "retraction": "They [LoEM and double-negative elimination] are not equivalent at a propositional level, but they are equivalent as principles of proof: It is easy to show that if you accept one the other follows, using entirely constructive reasoning as would have been acceptable to Brouwer. So I don't understand what this refers to; it must be a different interpretation of the principles than I have in mind. I'd need to see the paper to understand what is going on here." --Lambiam^Talk 23:58, 5 June 2006 (UTC)

I agree with you that one can be derived from the other, at least in bivalent logic; see the tiny proofs on the article page under the PM heading.

FYI: here's the entire quote: Note that it is a flea on a flea: it is in a note to a footnote to a paper mentioned in a footnote (something like that):

"Now, if the relations employed in any given proof can be decomposed into basic relations its 'canonical' form (that is the one decomposed into elemetntary inferences [^8]) employs only basic relations..."[I can't copy the rest of this its just a mass of subscripted F's](p. 460)

"^8 Just as, in general, well ordered species are produced by means of the two generating operations from primitive species (Brouwer 1926, p 451), so, in particular, mathematical proofs are produced by means of the two generating operations from null elements and elementary inferences that are immediatly given in intuition (albeit subject to the restriction that there always occurs a last elementary inference.) These mental [his italics] mathematical proofs that in general contain infinitely many terms must not be confused with their linguistic accompaniments, which are finite and necessarily inadequte, hence do not belong to mathematics.

" The preceding remark contains my main argument against the claims of Hilbert's metamathematics. A second argument is that the way in which Hilbert seeks to settle the question (which, incidentally, was taken over from intuitionism) of the reliability of the principle of excluded middle is a vicious circle; for if we wish to provide a foundation for the correctness of this principle by means of the proof of its consistency, this implicitly presupposes the pinciple of the reciprocity of the complementary species and hence the principle fo excluded middle itself (see Brouwer 1923c p. 252)[| Concerning this passage, Brouwer (1953, p.14. footnote 1) writes: "The equivalence of the principles of the excluded third and of reciprocity of complementarity mentioned there in a footnote by way of remark, subsequently has been recognized as nonexistent. In fact, as was also shown in the present paper the fields of validity of these two principles have turned out to be essentially different".|]." (van Heijenoort p. 460)

The way you read these quotes is the following:

(i) the first part is the "context" from van Heijenoort's reprint of Brouwer's paper: On the Domains of Defintion of Functions (1927)

(ii) the second part is the footnote ^8 at the bottom of van Heijenoort's page 460.

(iii) the third part [| Concerning this passage...|] is a parenthetic comment tacked onto Brouwer's footnote ^8 by someone, probably van Heijenoort or perhaps his translator Stefan Bauer-Mengleberg. Note that it references the 1953 paper and in this paper page 14 there's a "footnote 1" where Brouwer makes his comment (observation, retraction, whatever it is).

Interesting to note that this paper is so difficult that van Heijenoort takes 11 1/2 pges to preface it and the paper itself is only 6 pages long! I have no idea what the paper is saying. Brouwer is reinventing set theory, apparently. Here is the lead paragraph of van Heijenoort's introduction/explication:

"In a series of papers published from 1918 onward, Brouwer set forth an intuitionistic "set theory" and on this basis an intuitionistic reconstruction of point-set topology and analysis. The text below [is part of a paper published in 1927...and contains the proof that every function that is (in the intuitionistic sense) everywhere defined on the closed interval [0,1] of the continuum is uniformly continuous (Theorem 3). In the course of the argument Brouwer proves the fundamental theorem on "sets" that he later (1953) called the bar theorm, as well as its corollary , the fan theorem (Theorem 2)"(p. 446)

I checked the errata page (errata between 1st and 2nd editions) but none were pertaining to the footnote quotes. I hope this helps you folks make some sense out of this. wvbaileyWvbailey 01:17, 6 June 2006 (UTC)

I still can't make anything out of this. The equivalence of the two principles does not depend in any way on the assumption of bivalence. Under that assumption you get classical logic and then both hold, making equivalence completely trivial. If I saw the 1953 paper I don't remember it. Perhaps it might clarify the cryptic remark in the footnote, because Brouwer writes: "as was also shown in the present paper". But Brouwer's expository style is not always the most lucid. Some things he wrote are particularly unclear, and it is entirely possible that perusal of the paper will leave the question unanswered. In the absence of a clear understanding, it would appear best just not to refer to this "retraction" in the article. --Lambiam^Talk 08:12, 6 June 2006 (UTC)

I agree with you all the way. Until we see the paper we are at a loss, and I'm afraid that, as it is a mere parenthetic remark inside a footnote, the question will go unanswered. So to quote you: "In the absence of a clear understanding, it would appear best just not to refer to this "retraction" in the article".wvbaileyWvbailey 13:47, 6 June 2006 (UTC)

Equivalence of the generalization, versus generalization of the equivalence

May I go back to something that was said earlier: there is a difference between equivalence of the excluded middle and double negations as general rules on the one hand, and equivalence of individual assertions of each rule -- or, if you like, between equivalence of the generalization of each instance and generalization of the equivalence of each instance. So for instance "the law of the excluded middle can not lead to contradicton" might be written ~~(p v ~p), but (to abuse some second-order notation) are we really talking about ? Or are we actually talking about ?? Unfortunately it is not always made clear. I am not entirely sure I have made anything clearer either, or if this is worth mentioning at all...

For what it's worth, the latter is, to me, correct. In fact some "anti-classical" assumptions are defensible from intuitionist and indeed other constructivist points of view, and we would have families of propositions such that , even though we also have ! Or, if you like, the general law of excluded middle would actually be contradictory, even if there is no "specific-use" of it which is contradictory, because we can't go from not-all-are to some-are-not. Although from other (constructive) points of view, no anti-classical assumptions are necessary, even if not all classical assumptions are necessary. -Dan 15:28, 6 June 2006 (UTC)

If you have a cc of van Heijenoort's From Frege to Godel maybe there may be something of use in Kolmogorov page 431ff (esp p. 432). Whether this is the latest thinking I dunno. But there are lots of little quantifier formulas with "for alls" and 'does not exist" and etc etc. At the bottom of page 431 he writes something very cryptic (my bold-face):

§2. Generally, the propostions that we do not know how to prove without an illegitimate use of the principle of excluded middle ordinarily rest directly, not upon the principle of excluded middle of the logic of judgments, but upon another principle that bears the same name. In fact, from the principle of excluded middle in the form peculiar to the logic of judgments namely, "Every judgment is either true or false", we can obtain further conclusions by following the schema that corresponds to Hilbert's formula: if B follows from A as well as from ~A, then B is true. But in the case that interests us, that of transfinite judgments, it is difficult to obtain any positive conclusion B from the pure negation ~A; for that we must first transform the judgment ~A into some other (p. 432)

He then launches into "The following type of transfinite judgment is the most customary ...etc. etc." Here's where the fromulas similar to what you are writing appear here (the double negative gets mentioned re his formula (59)). If you want I can cc the rest tonight (it'll be a bit of a slog), right now I am supposed to be outside mowing the lawn. wvbaileyWvbailey

I wouldn't make you do that! Mowing the lawn is probably less unpleasant than all that copying. I dug up a copy, and yes, this is what I was talking about with not-all-are to some-are-not. Although "Not upon X but another principle that bears the same name" sounds almost like how Murphy's Law was not propounded by Murphy, but by another man of the same name.

He states that Hilbert believes that certain other principles "justify the application of the principle of excluded middle to infinite collections". In modern notation, these might be: (forward direction is his formula 59, reverse is 60), and: (forward 61, reverse 62).

He then goes on to prove, formally from even more basic principles, the second equivalence, as well as the reverse direction of the first equivalence. He only invokes double negation to prove the forward direction of the first equivalence (59). He asserts that any proof of that direction requires some such invocation. We might say: all X are not Y if and only if there is no X which is Y. We might also say: if some X is not Y, then not all X are Y. All these are proven by contradiction. (For instance for 60, a rough proof might be: assume that some X is not Y, and that all X are Y. Then some X is both Y and not Y! Impossible! Therefore, it follows that if some X is not Y, then not all X are Y -- and conversely he could also have deduced that if all X are Y, then there is no X which is not Y). But it is "illegitimate" for "transfinite judgement" to say if not all X are Y, then some X is not Y.

I had wanted to write about this too somewhere, probably under intuitionistic logic. -Dan 13:42, 8 June 2006 (UTC

I can't do this without examples, that's why I'm an engineer and not a mathematician. Last night I was mulling this over when I should have been sleeping:

We have the universes known and unknown with pigs p in them. One by one we examine these pigs p: We ask propose the proposition P(p) of each instance of our subjects p: "this pig p flies". To test our hypothesis we pick each pig up, one by one, and throw it. (Not very far: no animals are harmed in this experiment). After a while we begin to form a set/collection called "the universe of examined pigs". This collection is a subset of "all pigs seen and unseen throughout this and all other universes known and unknown". We find our subset/collection partitioned into two categories: "proposition p is true for subject p" i.e. P(p) and "proposition is not-true for subject p", i.e. ~P(p)". After a while (a really really long while) we believe that there is not a single instance of a pig anywhere in the universe that we have not examined, and not a single flying pig has been found (how do we arrive at this? I guess we ask an oracle I dunno). The "universe of examined pigs (all p):P(p)" has now the über-set (all p) i.e. it is identical to the transfinite set of "all pigs seen and unseen throughout this and all other universes known and unknown".

~[(all p):P(p)] =?: NO (all p):~P(p)

Had we found one, just one, we could assert that

(Exists a p):P(p)

But we didn't find a single flying pig p. So the proposition P that there exists a pig p and p flies (E p):P(p) is false=not-true. So does it make sense that:

~[(all p):P(p)] =? ~[(E p):P(p)] ?

I think it does <= Bill is wrong, see below

The right-most assertion ~[(E p):P(p)] asserts that "It's NOT TRUE that 'There exists a pig p that satisfies the proposition P(p) 'this pig p flies.' Does this imply that "there exists a pig that does does not fly?"

~[(E p):P(p)] -> (E p):~P(p)

I would think so. Altho the above form on the left seems to assert much more than the one on the right (it goes from the general (infinity) to the specific(an instance).

~[(all p):P(p]) -> (E p):~P(p)

ditto for the above form. [I need to mull this over more with my partitioned set].

What about the double negative?

"This assertion is not true: That after examinations of all pigs its not true that 'This pig flies'."

~[~[(all p):P(p)]] =? ~[(all p):~P(p)]

Something's wrong here: maybe between assertions "This [instance of] pig flies" and the generalizaton we are inclined to move to: "Pigs fly".

My mind is fried, I'll have to come back to this. wvbaileyWvbailey 19:35, 8 June 2006 (UTC)

Eh. In your notation ~[(all p):P(p)] means "It's not true that all pigs fly". This is VERY different from (all p):~P(p) which means "All pigs don't fly" -- they are different even in classical logic, or if you prefer, even in the finite world. This has nothing to do with the law of the excluded middle. I think you need to draw this out. Actually, I was very much thinking of drawing this out for intuitionistic logic... For the finite world (or, according to classical mathematics, in all cases), we can say:

1. There is no pig which doesn't fly = All pigs fly;
2. Not all pigs fly = There is (at least) one pig which doesn't fly;
3. Not all pigs don't fly = There is (at least) one pig which flies;
4. There is no pig which flies = All pigs don't fly.

In the transfinite world, the first three equivalences don't hold (the one on the right is a stronger statement), and the fourth equivalence still holds. We can make inferences from one line to another (e.g. [4] All pigs don't fly -> [2] not all pigs fly), but again, these inferences are also valid in the finite world/classical logic, and having nothing to do with LEM (and also, incidentally, [4] -> [2] depends on the assumption that there is at least one pig --- which is true for this example -- but that also has nothing to do with LEM). -Dan 20:21, 8 June 2006 (UTC)

I need to peruse your explanation when I'm fresher than I am now. But with regards to my bacon-on-the-wing example: Yes you are right: ~[(all p):P(p)] means that not all are flying but some or even none may be flying. Suppose we have a tiny finite set of three oinkers. Not all three are fliers:

~(P(p1) & P(p2) & P(p3)) = ~P(p1) V ~P(p2) V ~P(p3)

(I assume this equivalence is okay with the intuitionists because it is finite?)

~(a & b)= ~a V ~b

For the right side to be True only one of the terms ~P(pn) must be true.

~(P(p1) & P(p2) & P(p3)) = ~P(p1)=true V ~P(p2)=true V ~P(p3)=true

And for any one of these ~P(pj) to be true their respective P(pj) must be false.

~(P(p1) & P(p2) & P(p3)) = P(p1)=false V P(p2)=false V P(p3)=false

Thus any or all of the "P(pj)=false" must be true (!) and this means that there may be 0, 1, or 2 instances of flying pigs but not three instances of them.

The other case (all p):~P(p) means:

~P(p1) & ~P(p2) & ~P(p3) = ~(P(p1) V P(p2) V P(p3))

which means there is no instance whatever of a flyig pig, ie no instance of P(pj)=true.

Did I do this right? My question is: how do you draw this so it makes sense to anyone other than an expert? I agree this doesn't seem to have anything to do with LoEM but am not sure when relative to the double negative. My mind is still fried, will come back to it.wvbaileyWvbailey 23:53, 8 June 2006 (UTC)

Looks like you got it right, and just to be clear: yes, the equivalence is okay, because it is finite, i.e. the set of pigs is finite, and there is a finite decision procedure to definitely tell if any one of them flies (throw it). Both conditions are important.

How to draw it, even for the finite case? Good question. Maybe

| draw 3 pigs | 2 with wings, | 1 with,   | 3 without |
|  with wings |  1 without    | 2 without |           |
|                                                     |
|<---(1)----->|                                       |
|             |<---------------(2)------------------->|
|<----------------(3)-------------------->|           |
|                                         |<--(4)---->|

Corresponding to the 4 numbered equivalences above. Transfinite case? Haven't figured it out. My infinite drafting set got busted when I tried to draw ω^ω (no, seriously, that's really something I want to draw. The page has one for ω²). -Dan 02:34, 9 June 2006 (UTC)

The equivalence ~(a & b)= ~a V ~b is not an intuitionistic tautology. Here is a counterexample using Heyting algebra semantics. Take for the value of a the open half-plane {y : y > 0} and for b the open half-plane {y : y < 0}. Then a&b corresponds to the interior of the intersection of these two, which is empty and therefore already open. Its negation is the interior of the complement, which is the full plane and therefore already open. This is the value of "true". For ~a we need the interior of the complement of {y : y > 0}, that is, the interior of {y : y <= 0}, which is {y : y < 0} -- which happens to be the value of b. Symmetrically, ~b = a. Then ~a V ~b corresponds to the union of these two open half-planes, which is {y : y /= 0}. This is not the same as the full plane. At an intuitive level, knowing that a and b contradict each other, we have no way to point at one of the two and say: this one is false. --Lambiam^Talk 10:51, 9 June 2006 (UTC)

That is absolutely right. It is not valid in general. But these are necessarily infinite examples. For a finite example, in Heyting arithmetic, is a theorem. The reasoning is alright in this case because a) we are quanitifying over a finite set, and b) there is a finite decision procedure for each instance. Another way to think about the same thing is: assuming LEM, we have ~(a&b) <-> (~a v ~b); but with a finite decision procedure for a and b we don't need to assume LEM, we can prove the specific instances of it that we need (so I guess from that perspective, it is still related to LEM after all). -Dan 13:50, 9 June 2006 (UTC)

I see what Dan is up to and I think it's good. One thought I had relative to the one piggy that flies, is to draw a Karnaugh map (or Venn diagram) of { P, ~P }. Put one dot on the "P" side of the map for the piggy that flies, then color the "~P" side completely black except for the dot that is missing. Now, if we "go to infinity"-- that is, test all piggies in universes known and unknown, the dot gets smaller and smaller and eventually disappears into the page when the ink smears. Per Russell the role of induction in transfinite cases is -- to draw inferences based on probability:

(all days on earth):"on this day on earth sun rises in the east"

is only "true" in the probabilistic sense.

Which brings me to the role of induction in all this [?], and the fact that the LoEM seems to devolve into "philosophy" and into "semantics" or "meaning/definition".

Does anyone know what impredicate means? My dictionary doesn't have it and Google only pulled up 39 instances of drivel.

Lambiam's example above reminds me of my example of the logistic function:

Y = 1/(1+exp^(k*X))

This always has a center point Y=0.5 for X=0 no matter how large the value of k. So we see as k goes to infinity, the weird case of (infinity x 0) = 0.5. The derivative has a maximum or minimum at this point too.

An engineer-as-philosoper would argue that such a function as Lambiam has defined is perverse and unusable bcause it is undefined throughout the plane:

{y:y<0} U {y:y>0} <> whole plane

{y:y=0} is undefined

therefore {y:y<0} & {y:y>0} is undefined

The complement of the union is the value exactly at 0 which is undefined. So it cannot be used in a construction in which the undefined point becomes defined by accident. End of philospher's discussion. Me, being the devil's advocate here (the pay is lousy by the way), I am agnostic: Hence my question about what impredicate means. This was Godel's complaint (cf a quotation above).

To Lambiam's point about the equivalence, now that I am not so tired I see that: By PM's definition, a->~b =def ~aV~b . Ditto by PM's definition, a->a =def ~aVa, the LoEM. So if we don't accept ~aVa then we cannot accept a->a [is this true?] nor a->~b nor ~aV~b nor ~(a&b), all of which follow. Correct?

Does this all devolve into a problem with the definition of implication? Bear with me for a second: I remember when I first encountered "implication" I was stunned to see people defining "an operation of thought-as-logic" based on this definition. We are expected to accept both implications as true based on the assertion of a falsehood:

"The sun rises in the west" implies "my pig flies" OR

"The sun rises in the west" implies "my pig does not fly"

therefore: "The sun rises in the west" implies P(p) OR ~P(p) [LoEM ?]

which I don't have any trouble with, myself (the pig either flies or it doesn't). But:

"The sun rises in the west" implies "my pig flies" AND

"The sun rises in the west" implies "my pig does not fly"

therefore: "The sun rises in the west" implies P(p) AND ~P(p)

seems different. Once asserted the falsehood can "lead to" both a truth and a falsehood on/of the same propostion, simultaneously. [yikes where does this go?]

Interesting that one name for "implication" is "the conditional". My old college test (John Kemeny et. al. Finite Mathematical Structures, Prentice-Hall, Englewood Cliffs NJ 1958-59) defines it this way (his italics):

"Suppose we did not wish to make an outright assertion but rather an assertion containing a condition....[he gives examples here e.g. "If the weather is nice I will take a walk"]... Each of these statements is of the form "if p then q." The conditional is then a new connective which is symbolized by the arrow -->.

In figure 11a he shows a truth table, and the 2 cases (F, T) and (F, F) are filled in with question marks.

"Therefore we make the completely arbitrary decision that the conditional, p-->q, is true whenever p is false, regardless of the truth value of q... we give the conditional p-->q the "benefit of the doubt" and consider it true (see Exercise 1)" (p. 9: I underlined this with wiggly lines, way back in 1966)

Exercise 1 asks the student to fill in the question-marks and observe that no matter how they are filled in we end up with another connective's truth table, or our original propositions p, q etc. In other words, we have no choice but to fill in both of the condtional's question-marks with "true". There are only 16 possible truth tables, and this and its converse q-->p constitute "the last two remaining" truth tables.

But... Kolmogorov does not agree [?] with the "formalistic definition" (p. 420) of implication:

"Or, in the formalistic interpretation: if formula A is written down, we can also write down formula B [footnote 6 has a thing that looks like "G, G->F|F" written in German script that he attributes to Hilbert and to Sigwart]. Thus, the relation of implication between two judgments does not establish any connection between their contents.

" Hilbert's first axiom of implication, which means that "the truth follows from anything" results from such a formalistic interpretation of implication: once B is true by itself, then after having accepted A we also have to regard B as true. [etc] Kolmogorov in von Heijenoort p. 420)

Once again I am left more confused than when I started, e.g. was Kemeny expressing an intuitionist definition of implication? What is Kolmogorov trying to say? Is he for or against the formalist definition of implication? But if he accepts it doesn't he have to accept the LoEM? Under what conditions won't he accept the LoEM? Does "impredicate" have anything to do with this? (Maybe this confusion is okay: it shows what befalls semi-literate Wiki readers like myself when they confront :intuitionism", the LoEM, implication, etc).wvbaileyWvbailey 13:21, 9 June 2006 (UTC)

"Impredicate" might be impredicative. That's a whole other issue related to constructivism. And yes, I highly suspect a lot of people look at constructivism and go, what the **** is this ****? What's more I think I might have confused you with my comments. I am sorry. What I really meant to say before was: that sort of "truth table" thing worked only because we were in the finite pig pen. NO, a->b is NOT equivalent to ~a v b to an intuitionist. The latter is a stronger statement. Maybe it might help to have a look at BHK interpretation. Or maybe that just confuses things further.

a->a is ok (it is easy to go from a to a: you're already there), but a v ~a is not (which one is it?). I am starting to think we need a completely separate presentation of intuitionistic logic. It is clearly not good enough for that page to sort of refer back to classical logic and say "well, you know, kind of the same, but remove the law of the excluded middle..." -Dan 14:19, 9 June 2006 (UTC)

I found this on the web, this definition of "impredicative"

Torkel Franzen wrote:

"The Model-Based Mind" by Kercel, VanHoozer, and VanHoozer, citing Kleene, presents it as:

""An impredicative property, P(x), of an object x in X, is the property such that X is the set of objects possessing property P(x). In other words, an impredicative property participates in its own definition. Mathematicians do not deny the existence of impredicativities, [sic] but regard them as a necessary evil. Impredicativite [sic] processes, closed loops of causality and bizarre systems are equivalent concepts."

"" I guess it's inevitable that the logical term "impredicative" should inspire all sorts of extended or analogous uses. The above, however, is not at all correct applied to the use of "impredicative" in logic. An impredicative definition, in logic, is one that defines an object -typically a set - by means of quantification over a totality to which that object itself belongs."

What the hell is the difference between the two "definitions"? What kind of word is this "impredicativities"? Are angels dancing on pin-heds here? Is this just Russell's paradox in the buff? wvbaileyWvbailey 14:28, 9 June 2006 (UTC)

It's defining something in terms of a collection that it's supposed to belong to. Rather than defining objects before trying to define the collections which contain them. I'm not sure it's really relevant here... Maybe we can split that discussion to Talk:Impredicative to preserve at least a little bit of sanity. -Dan 14:45, 9 June 2006 (UTC)

After seeing the definitions I agree it isn't relevant to the LoEM, at least per my superficial level of understanding. wvbaileyWvbailey 16:56, 9 June 2006 (UTC)

The definitions of PM are irrelevant to the question whether something is an acceptable proof principle in intuitionistic mathematics, or a tautology in intuitionistic logic. The usual intuitionistic interpretation of implication, due to Kolmogorov, is: When we assert a → b, it means that we have a method to produce a proof of b, given a proof of a. Under this interpretation, whatever the statement a, it is trivially the case that a → a. Likewise, a V b means: we have a proof of (at least one of) a and b. It is clearly not the case that for every mathematical statement a we have a proof of a or a proof of not a, so an intuitionist is not in a position to assert a V ~a. In conclusion, a → a and a V ~a are in general very different statements.

PM is an attempt to reduce the notion of mathematical truth to a formal system of symbols. An important part of Brouwer's criticism was that even attempting such a reduction is completely unwarranted: (formal) logic is a branch of mathematics, just like arithmetic, algebra and geometry, and as such is not suitable to serve as a foundation of mathematics; any attempt to do so is circular wishful thinking. A principle of proof can not be justified by inventing a game with symbols in which it is one of the rules. This is putting the cart before the horse. Only after we have justified a proof principle should we include it in the rules of the formal game, if that game is supposed to model valid proof methods. --Lambiam^Talk 15:26, 9 June 2006 (UTC)

I think we're all on the same page now. Dan's explanations forced me to think with examples. And Lambiam's two paragraphs above explains what is going on very well. This is the best exposition I've seen of this: succinct and clear. Perhaps the should be embedded into the article? The only thing that is missing is the why with respect to transfinite proofs and the double negative (which sort of falls out once you understand that a-->a is not a V ~a for an intuitionist).

The following is a summary of my understanding so far:

IF we are intuitionists THEN:

We do accept a-->a AND/BUT we do NOT accept PM's LoEM "~a V a" and "a V ~a" for the reasons given below;

THEREFORE we do not accept either the PM derivation ~(~a)-->a from ~a V a (and vice versa) nor the derivation ~a --> ~a and a --> a from a V ~a (and vice versa) BECAUSE the derivations require use of (and thus imply) the rejected LoEM.[correct?]

Reasons for not accepting the LoEM:

The first reason: "It is clearly not the case that for every mathematical statement a we have a proof of a or a proof of not a, so an intuitionist is not in a position to assert a V ~a." This problem occurs [only? usually? primarily? always?] in transfinite proofs because of the following ...[need succinct explanation here re reasoning that draws a truth from a negative/false outcome[?] ].

The second reason: "PM is an attempt to reduce the notion of mathematical truth to a formal system of symbols. An important part of Brouwer's criticism was that even attempting such a reduction is completely unwarranted...etc"

AND finally: an intuitionist's cure for this state of affairs is the following:

[I draw a blank here: is it Kolmogorov's restated axioms? New definitions of what constitutes "a proof?" Unresolved?]

wvbaileyWvbailey 15:12, 10 June 2006 (UTC)

For Lambiam: I owe you some input on what you've written; I like it and think it is excellent. It probably does belong in intuitionism, but on the other hand the LoEM and intuitionism are so intertwined that a person reading about intuitionism would need some grounding in what the LoEM fuss is all about. Probably the LoEM article could then be trimmed.

With reference to citation/attribution and support: I need to learn more about Brouwer et. al. I will have to go hunting for his biography or whatever is written about him (Do you know of one? Any good historical reading re the development of intuitionist logic? By the way, how did you come to learn so much about Brouwer and intuitionism?). I want to probe backward and learn what caused Brouwer's philosophy to diverge so much from that of Hilbert + Russell-Whitehead. Something like this with more links drawn:

? --> Kummer --> Kronecker --> Brouwer --> Weyl, Kolmogorov -->?

? --> ? Leibniz --> Boole --> Peirce --> Frege + Peano + Whitehead --> Hilbert, Poincare --> Russell --> PM

? --> "analysis" --> ?

? --> Cantor --> ?

In fact as I am sitting here typing this I have been thumbing through Dawson's chapter III Excursus (p. 37ff) that gives a brief history of the development of logic; he starts it with: (lo and behold!) Aristotle and the LoEM! His exposition parallels the little chart above that I gleaned from the references in the back of van Heijenoort.

I did find some support of what you've written in Encyclopedia Britannica in the article titled "Analysis". I'll paste this into a section following your exposition. And other support as I find it. wvbaileyWvbailey 12:53, 15 June 2006 (UTC)

Lambiam's exposition

What counts as an acceptable proof method to intuitionists will necessarily always remain a bit vague, as these issues precede any attempts at formalization. In fact, not all intuitionists agreed or agree on all aspects; see for example the article on Ultrafinitism. Most would agree, though, that intuitionistic logic faithfully internalizes the propositional aspect of intuitionistically acceptable mathematical reasoning, and so will accept a valid theorem in that logic as being also a valid theorem schema in mathematics itself. In many ways intuitionistic type theory has gone further, extending the scope of the formal-logical approach. In general, the methods of constructive mathematics are also acceptable to intuitionists, and some people even identify intuitionism with constructivism in mathematics.

Intuitionists accept P V ~P for any specific proposition P whose truth or falsehood has been demonstrated. Furthermore, they accept this for classes of propositions for which an effective method is known for testing whether they hold. For example, consider the class in which P takes the form X = Y in which X and Y are arithmetic formulas involving only numerals and the familiar arithmetic operations. To test the validity of such a P, just evaluate the two sides of the equation and check whether they are the same. If such a test is not (known to be) available, usually the problem involves, so to speak, to test an infinity of cases, and no known reasoning allowing us to reduce this infinity to a finite number of effectively testable cases. A well-known example is Goldbach's conjecture. For many classes of formally infinite problems an effective (and therefore finite) test procedure is known, however, and then intuitionists will gladly assert P V ~P for these classes. What counts as effective to intuitionists, and which effective procedures count as true tests, will necessarily always remain a bit vague; see above.

Intuitionists can look at PM derivations in two ways. One is that the logician is playing a game with self-invented rules, like peg solitaire but more complicated, and then they can look at the process and verify that the logician is not cheating. Just as for peg solitaire, this has nothing to do with notions of truth. They can also look at this game, bearing in mind that the logician claims the symbols mean something and allow the game player to express truths. Then there are many potential problems, some having to do with what counts as an acceptable definition (for example of notions like function and real number), some with the range of quantifications, some with the validity of inference rules, and some with the axioms. What these objections have in common is that intuitionists believe that the use of unreliable definitional approaches, unreliable inference rules and unreliable axioms does not offer a reliable way for examining the truth of mathematical claims. Clearly, derivations assuming LoEM or using double negative elimination are not considered kosher. Intuitionists will consider a PM derivation of a → a from a V ~a as a good example of how you can occasionally and accidentally reach correct conclusions using unreliable methods.

The "cure" intuitionists would prescribe to the mathematical ailment of unreliability is: Use only methods whose reliability has been established. What is reliable and what not, is open to discussion, as is the question what constitutes sufficient evidence or justification. But if, in order to justify a principle, you need to resort to a circular argument, you have failed to establish reliability. Also, the argument that something has a respectable pedigree harking back to Aristotle, is believed to be sound by more than five million mathematicians, and has not failed thus far in any case where it was applied, is unacceptable.

I'm not sure how much detail of this (assuming proper citations) should be presented in the article Law of excluded middle. If it should be presented at all, then the article Intuitionism may be a better place. --Lambiam^Talk 18:16, 12 June 2006 (UTC)

Citations, comments etc on the above

References:

"analysis." Encyclopædia Britannica. 2006. Encyclopædia Britannica 2006 Ultimate Reference Suite DVD 15 June 2006, "Constructive analysis" (Ian Stewart, author)

Goldstein, Rebecca, Incompleteness: The Proof and Paradox of Kurt Godel, Atlas Books, W.W. Norton, New York, 2005.

Rosenbloom. Paul C., The Elements of Mathematical Logic, Dover Publications Inc, Mineola, New York, 1950.

Anglin, W. S., Mathematics: A Concise history and Philosophy, Springer-Verlag, New York, 1994.

Encyclopedia Britannica:

Stewart's reference in E.B.:

"Errett Bishop and Douglas Bridges, Constructive Analysis (1985), offers a fairly accessible introduction to the ideas and methods of constructive analysis."

"Constructive analysis

"One philosophical feature of traditional analysis, which worries mathematicians whose outlook is especially concrete, is that many basic theorems assert the existence of various numbers or functions but do not specify what those numbers or functions are. For instance, the completeness property of the real numbers tells us that every Cauchy sequence converges, but not what it converges to. A school of analysis initiated by the American mathematician Errett Bishop .... This philosophy has its origins in the earlier work of the Dutch mathematician-logician L.E.J. Brouwer, who criticized “mainstream” mathematical logicians for accepting proofs that mathematical objects exist without there being any specific construction of them (for example, a proof that some series converges without any specification of the limit which it converges to). Brouwer founded an entire school of mathematical logic, known as intuitionism, to advance his views [italics and boldface added]

"However, constructive analysis remains on the fringes of the mathematical mainstream... Nevertheless, constructive analysis is very much in the same algorithmic spirit as computer science, and in the future there may be some fruitful interaction with this area" (Britannica Analysis/Constructive Analysis)

wvbaileyWvbailey 13:10, 15 June 2006 (UTC)

W.S. Anglin’s exposition

In his Chapter 39. Foundations, Anglin has three sections titled “Platonism”, “Formalism” and “Intuitionism”. I will quote most of “Intuitionism”. Anglin begins each as follows:

”Platonism

”Platonists, such as Kurt Gödel, hold that numbers are abstract, necessarily existing objects, independent of the human mind” (p. 218)

”Formaism

“Formalists, such as David Hilbert (1862-1943), hold that mathematics is no more or less than mathematical language. It is simply a series of games...” (p. 218)

”Intuitionism

”Intuitionists, such as L. E. J. Brouwer (1882-1966), hold that mathematics is a creation of the human mind. Numbers, like fairy tale characters, are merely mental entities, which would not exist if there were never any human minds to think about them.

”Intuitionism is a philosophy in the tradition of Kantian subjectivism where, at least for all practical purposes, there are not externally existing objects at all: everything, including mathematics, is just in our minds. Since, in this tradition, a statement p does not acquire its truth or falsity from a correspondence or noncorrespondence with an objective reality, it may fail to be ‘true or false’. Thus intuitionists can, and do, deny that, for any mathematical statement p, it is a logical truth that ‘either p or not p’.

”Since intuitionists reject objective existence in mathematics, they are not necessarily convinced by the reasoning of the form:

”If there is not mathematical object A, then there is a contradiction; hence there is an A.

[I found this confusing. Does he mean: There exists B: (~A -> ~B) & B -> A [?]]

"If the details of the reasoning provide a way of imagining or conceiving an A, in a way open to ordinary human beings by, say, calculating it in a finite number of steps), then the intuitionist will agree that there is, indeed, an A. However, if the details of the reasoning do not provide this, the intuitionist will remain skeptical. For a Platonist, it is of interest that there is an A even if it is only God who can conceive it. For an intuitionist, however, a mathematical object is meaningless unless it can be somehow ‘constructed’ and ‘intuited’ by a human being.

"For the intuitionist, the human mind is basically finite, and Cantor’s hierarchy of infinites is just so much fantasy. Intuitionists thus reject any mathematics which is based on it, including most of calculus and most of topology.

"... To ... objections, the intuitionist can replay: (1) it does not make sense for human minds to try to conceive a world without human minds, and (2) it is better to have a small amount of mathematics all of which is solid and reliable than to have a large amount of mathematics, most of which is nonsense”(p. 219)