5 ms·

Careful! Here is LEM: ⊢. ~p ∨ p (one of either p or p's inverse must be true -- and thus the other false -- with no third (truth) value allowed), hence also c

Careful! Here is LEM: ⊢. ~p ∨ p (one of either p or p's inverse must be true -- and thus the other false -- with no third (truth) value allowed), hence also called principle of bivalence. What you wrote is the principle of double negation. In general: (~p ∨ p) ⇒ (¬¬p ⇔ p) but not the other way around if I not mistaken? Please correct me if I am wrong.

igravious 11y ago
In other words, what you wrote is that every value when negated twice returns to itself. Here's a truth table of 3 values for the negation operator v | 0 | 1 | 2 -------------- ¬v | 1 | 0 | 2 So ¬¬0 ⇔ 0 and ¬¬1 ⇔ 1 and ¬¬2 ⇔ 2 which satisfies the principle of double negation but not LEM. Correct?
- IngoBlechschmid 11y ago
  Your counterexample could work, but it is not obvious that it does so. This is because you also have to give definitions of ∧, v, and ==>, and then check that your definitions satisfy the axioms of intuitionistic logic. As stated, your example only shows that one can define a function f on a set which contains more than two elements such that f . f = id. But this by itself is a trivial statement.
  - igravious 11y ago
    Once those definitions are given then my trivial example holds though, correct? Which are you saying; that it is, or, it is not possible to give those definitions?
    - IngoBlechschmid 11y ago
      I didn't check it. If you want to do it (the key step being to verify that the axioms of intuitionistic logic holds for your definitions of AND and OR), you can check Wikipedia for the list of axioms to verify: https://en.wikipedia.org/wiki/Heyting_algebra https://en.wikipedia.org/wiki/Heyting_algebra
IngoBlechschmid 11y ago
You are right that for a particular formula p, the implication (~p ∨ p) ⇒ (¬¬p ⇔ p) is an intuitionistic tautology and that the reverse implication is not (in general). However the situation is different when you quantify over all formulas. If you have (¬¬p ⇔ p) for _any_ formula p, you also have (~q ∨ q) for any formula q (written with a different letter to not get lost in variable capturing issues). This is because, for any formula q, we have the intuitionistic tautology ~~(~q v q). (Proving this is a fun exercise. If you get stuck, see page 26 of https://github.com/iblech/talk-constructive-mathematics/raw/master/negneg-translation-notes.pdf https://github.com/iblech/talk-constructive-mathematics/raw/... or elsewhere on the Internet.) So, if you assume the principle of double negation for all formulas, then in particular you assume that, for any formula q, the implication ~~(~q v q) ⇒ (~q v q) holds. Since the antecedent is unconditionally valid, the consequent is as well. Thus you have the law of excluded middle for q. I highly recommend Andrej Bauer's blog for such matters. The post http://math.andrej.com/2008/08/13/intuitionistic-mathematics-for-physics/ http://math.andrej.com/2008/08/13/intuitionistic-mathematics... is a good starting point.
- igravious 11y ago
  You melted my brain. What does “quantify over all formulas” mean? From the way you state it, that's an interesting perspective. But it seems to be from a perspective of totality which I'm wary of. Not saying you're wrong, going to check out those links. Andrej Bauer was very kind to answer an out-of-the-blue email query of mine once :) Seriously appreciative of your response, a thousand thanks! EDIT: Ok, I've read your paper/slides. Very interesting. Don't you show that for specific constructions you can make LEM work for classical proofs with continuation monads? How does that show that _in general_ in constructive mathematics that the implication (~p ∨ p) ⇒ (¬¬p ⇔ p) holds but not its inverse? Also, your bit about rewinding time makes complete sense imho because classical logic is atemporal and continuation monads inject the idea of flowing time into those proofs in a controlled manner. EDIT 2: I _highly_ reccommend Dennis E. Hesseling's Gnomes in the Fog: The Reception of Brouwer's Intuitionism in the 1920s which I think gives a different slant on what Brouwer actually claimed than what you might imagine if you go with Andrej Bauer's interpretation. I can shoot you a copy if you can't lay your hands on it online :)
leoc 11y ago
Careful: https://en.wikipedia.org/wiki/Principle_of_bivalence#Relationship_with_the_law_of_the_excluded_middle https://en.wikipedia.org/wiki/Principle_of_bivalence#Relatio...

igravious 11y ago

In other words, what you wrote is that every value when negated twice returns to itself. Here's a truth table of 3 values for the negation operator v | 0 | 1 | 2 -------------- ¬v | 1 | 0 | 2 So ¬¬0 ⇔ 0 and ¬¬1 ⇔ 1 and ¬¬2 ⇔ 2 which satisfies the principle of double negation but not LEM. Correct?

IngoBlechschmid 11y ago
Your counterexample could work, but it is not obvious that it does so. This is because you also have to give definitions of ∧, v, and ==>, and then check that your definitions satisfy the axioms of intuitionistic logic. As stated, your example only shows that one can define a function f on a set which contains more than two elements such that f . f = id. But this by itself is a trivial statement.
- igravious 11y ago
  Once those definitions are given then my trivial example holds though, correct? Which are you saying; that it is, or, it is not possible to give those definitions?
  - IngoBlechschmid 11y ago
    I didn't check it. If you want to do it (the key step being to verify that the axioms of intuitionistic logic holds for your definitions of AND and OR), you can check Wikipedia for the list of axioms to verify: https://en.wikipedia.org/wiki/Heyting_algebra https://en.wikipedia.org/wiki/Heyting_algebra

IngoBlechschmid 11y ago

You are right that for a particular formula p, the implication (~p ∨ p) ⇒ (¬¬p ⇔ p) is an intuitionistic tautology and that the reverse implication is not (in general). However the situation is different when you quantify over all formulas. If you have (¬¬p ⇔ p) for _any_ formula p, you also have (~q ∨ q) for any formula q (written with a different letter to not get lost in variable capturing issues). This is because, for any formula q, we have the intuitionistic tautology ~~(~q v q). (Proving this is a fun exercise. If you get stuck, see page 26 of https://github.com/iblech/talk-constructive-mathematics/raw/master/negneg-translation-notes.pdf https://github.com/iblech/talk-constructive-mathematics/raw/... or elsewhere on the Internet.) So, if you assume the principle of double negation for all formulas, then in particular you assume that, for any formula q, the implication ~~(~q v q) ⇒ (~q v q) holds. Since the antecedent is unconditionally valid, the consequent is as well. Thus you have the law of excluded middle for q. I highly recommend Andrej Bauer's blog for such matters. The post http://math.andrej.com/2008/08/13/intuitionistic-mathematics-for-physics/ http://math.andrej.com/2008/08/13/intuitionistic-mathematics... is a good starting point.

igravious 11y ago
You melted my brain. What does “quantify over all formulas” mean? From the way you state it, that's an interesting perspective. But it seems to be from a perspective of totality which I'm wary of. Not saying you're wrong, going to check out those links. Andrej Bauer was very kind to answer an out-of-the-blue email query of mine once :) Seriously appreciative of your response, a thousand thanks! EDIT: Ok, I've read your paper/slides. Very interesting. Don't you show that for specific constructions you can make LEM work for classical proofs with continuation monads? How does that show that _in general_ in constructive mathematics that the implication (~p ∨ p) ⇒ (¬¬p ⇔ p) holds but not its inverse? Also, your bit about rewinding time makes complete sense imho because classical logic is atemporal and continuation monads inject the idea of flowing time into those proofs in a controlled manner. EDIT 2: I _highly_ reccommend Dennis E. Hesseling's Gnomes in the Fog: The Reception of Brouwer's Intuitionism in the 1920s which I think gives a different slant on what Brouwer actually claimed than what you might imagine if you go with Andrej Bauer's interpretation. I can shoot you a copy if you can't lay your hands on it online :)

leoc 11y ago

Careful: https://en.wikipedia.org/wiki/Principle_of_bivalence#Relationship_with_the_law_of_the_excluded_middle https://en.wikipedia.org/wiki/Principle_of_bivalence#Relatio...