Timeline for Adding nonconstructive disjunction to intuitionistic logic
Current License: CC BY-SA 3.0
30 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Nov 23, 2022 at 10:27 | comment | added | Gro-Tsen | The claim that “we always have $A\dot{\small\vee} \neg A$” (made in the Sep. 1, 2017 update), is incorrect: in fact, $A\dot{\small\vee} \neg A$ meaning $((¬A)⇒A)⇒A \land (A⇒¬A)⇒¬A$ is equivalent to $(¬¬A)⇒A$ (just like for the other candidate connector proposed in this answer, although the two are not generally equivalent). | |
| Sep 2, 2017 at 7:44 | comment | added | Franka Waaldijk | Yes, dependence on MP also crossed my mind. Well, enough from me... and wishing you good progress, Frank | |
| Sep 1, 2017 at 23:44 | comment | added | Dmytro Taranovsky | If realizability is interpretable, then so is $A⅋B$, but I do not think you can interpret $A⅋B$ in terms of other connectives without looking inside $A$ and $B$. However (inspired by your characterizations), if $r⊩A$ and $r⊩B$ are both $Π^0_2$, then under certain basic assumptions, $A⅋B$ is equivalent to $∃a,b∈ℝ[ab∉ℚ∧(a∉ℚ→A)∧(b∉ℚ→B)]$. This can be proved for both recursive-code realizability and continuous realizability using $Π^0_2$-completeness of $a∉ℚ$; I did not check other possible realizability notions (and possible dependence on MP). | |
| Sep 1, 2017 at 10:49 | comment | added | Franka Waaldijk | @მამუკაჯიბლაძე: well, all those implications confuse me too :-). And in the end you are even more right than you thought me to be, because (see update above) we always have $A\dot{\small\vee}\neg A$...which distinguishes $\dot{\small\vee}$ from $⅋$ too much. | |
| Sep 1, 2017 at 10:42 | history | edited | Franka Waaldijk | CC BY-SA 3.0 |
improved presentation
|
| Sep 1, 2017 at 10:02 | history | edited | Franka Waaldijk | CC BY-SA 3.0 |
typos
|
| Sep 1, 2017 at 9:46 | history | edited | Franka Waaldijk | CC BY-SA 3.0 |
another large update....
|
| Aug 30, 2017 at 7:20 | comment | added | მამუკა ჯიბლაძე | Sorry you are right, I became confused | |
| Aug 29, 2017 at 21:23 | comment | added | Franka Waaldijk | I've really enjoyed this question, I voted for Andrej's answer (better than mine :-) ) and appreciated the comments. But I have to other things to do, this puzzle has cost me more time than I can spare... so please forgive me for not responding to any comments very soon. | |
| Aug 29, 2017 at 21:20 | comment | added | Franka Waaldijk | @მამუკაჯიბლაძე : do you mean "in KC $A⅋A\Leftrightarrow A$ is true?". $A⅋A$ cannot be true for all $A$. Still I agree that they are not equivalent when we don't know more about the realizability context. It (still) seems to me that it will be difficult to find a concrete realizability context where, as I wrote above, $A⅋B$ is weaker than $A\vee B$ and yet stronger than $(\neg A\rightarrow B)\wedge (\neg B\rightarrow A)$. This I believe holds even stronger for $A\dot{\small\vee} B$, that was my meaning. | |
| Aug 29, 2017 at 17:36 | comment | added | მამუკა ჯიბლაძე | What do you mean by "more difficult to distinguish"? In $\bf IPC$, $(A\dot{\small\lor}A)\iff A$ is true, while in $\bf KC$ (i. e. in ${\bf IPC}+\neg p\lor\neg\neg p$), $A\par A$ is true. So $(A\dot{\small\lor}A)$ and $A\par A$ cannot be equivalent. | |
| Aug 28, 2017 at 16:45 | comment | added | Dmytro Taranovsky | Your definition of $A⅋B$ in terms of realizers appears correct. I think $a⊩A$ can be treated like a Harrop formula with ∃a∈R giving the constructive aspect of $A$. One example of realizability is number realizability in Heyting arithmetic. Another is realizability by real numbers coding continuous functions, with constructive validity requiring a recursive realizer for the closure of $A$. (Also, except in special cases, $(B→A)→A)$ would not give us a witness for $A$.) | |
| Aug 28, 2017 at 13:21 | history | edited | Franka Waaldijk | CC BY-SA 3.0 |
added extra math observation
|
| Aug 28, 2017 at 13:14 | history | edited | Franka Waaldijk | CC BY-SA 3.0 |
large update, hopefully imporvement...
|
| Aug 22, 2017 at 18:34 | comment | added | მამუკა ჯიბლაძე | No, wrong, $(\neg\neg A\to B)\land(\neg A\to A)$ is equivalent to $B\land\neg\neg A$. Still, it does not hold in general. | |
| Aug 22, 2017 at 18:23 | comment | added | მამუკა ჯიბლაძე | Specifically, I cannot complete the last argument (if we know $(*)$, then we can take $A$, $B$ as our candidate witnesses for $A\par B$): if $A$ would work as a witness then we should have, depending on how we substitute, either $(\neg A\to B)\land(\neg\neg A\to A)$, or $(\neg\neg A\to B)\land(\neg A\to A)$. In presence of $(*)$, the first one gives $\neg\neg A\to A$, which does not need to hold. As for the second one, without any further assumptions it is just equivalent to $B$. The same thing happens if we try $B$ for a witness. | |
| Aug 21, 2017 at 20:54 | comment | added | მამუკა ჯიბლაძე | More generally, take open sets of an extremally disconnected non-discrete space. In such space every regular open is closed, so that $\neg C\lor\neg\neg C$ gives the whole space for every open $C$. On the other hand if the space is not discrete then there is a nontrivial dense open $A$, i. e. $A$ is not the whole space but $\neg\neg A$ is. | |
| Aug 21, 2017 at 20:50 | comment | added | მამუკა ჯიბლაძე | Here is an example: let $P=\{0<1\}$ and let the valuation of $A$ be $\{1\}$. Then $\neg\neg A$ holds but there is no $C$ with $(\neg C\lor\neg\neg C)\to A$ since every $\neg C\lor\neg\neg C$ holds too. | |
| Aug 21, 2017 at 20:47 | comment | added | მამუკა ჯიბლაძე | I believe $A\par B$ is not equivalent to $(\neg A\to B)\land(\neg B\to A)$. Take $A=B$, then $(\neg A\to B)\land(\neg B\to A)$ is equivalent to $\neg\neg A$, while if $A\par A$ holds then there is a $C$ with $(\neg C\lor\neg\neg C)\to A$. Now take as a model some finite poset $P$, with propositions valuated as upper sets of $P$. Then $\neg\neg A$ holds if valuation of $A$ contains $\max P$, while if there is a $C$ such that $(\neg C\lor\neg\neg C)\to A$ holds then valuation of $A$ also contains every element $x$ with the property that ${\uparrow}x\cap\max(P)$ is a singleton. | |
| Aug 21, 2017 at 20:08 | comment | added | Dmytro Taranovsky | @FrankWaaldijk Good question. I added a note to that effect in my update. | |
| Aug 21, 2017 at 16:09 | comment | added | Franka Waaldijk | The second part of the comment is also not quite right (sigh). I mean: I don't think you can give a concrete example of a situation where (i) $(\neg A\rightarrow B)\wedge (\neg B\rightarrow A)$ holds (ii) we do not know $A\vee B$ (iii) we do not have $A⅋B$ (iv) $A⅋B$ does not imply $A\vee C$. So the situation where $A⅋B$ is stronger than $(\neg A\rightarrow B)\wedge (\neg B\rightarrow A)$ and yet weaker than $A\vee B$ does not occur, if you ask me. | |
| Aug 21, 2017 at 15:46 | comment | added | Franka Waaldijk | Sorry, the first part of the comment above is the wrong way round (logic with double negation and arrows sometimes does that to me). Please disregard. I mean: Let $A$ be as above. Can you give me a concrete example for $P$ such that we have $A⅋A$ and yet we do not have $A$? I don't think so. So the situation where $A⅋A$ is stronger than $\neg A\rightarrow A$ and yet weaker than $A$ does not occur, if you ask me. | |
| Aug 21, 2017 at 15:25 | comment | added | Franka Waaldijk | Let $A$ be $\forall n [P(n) ∨ \neg P(n)]$ and assume $\neg\neg A$ as you say. You say that a witness for $\neg A\rightarrow A$ gives us nothing, but I disagree. Can you give me a concrete example for $P$ such that we have $\neg A\rightarrow A$, and yet we do not have $A$? I don't think so, which is what the gist of my answer is. My answer was not given as a constructivist, I just think that you cannot give any concrete example of a situation where $(\neg A\rightarrow B)\wedge (\neg B\rightarrow A$) holds (not hypothetically as in your case, but really!) and yet we cannot show $A⅋B$. | |
| Aug 21, 2017 at 12:21 | comment | added | Dmytro Taranovsky | Thank you for the suggestion. For a constructivist, $(¬A⇒B)∧(¬B⇒A)$ may be a close approximation to $A⅋B$. However, assume we are using recursive realizability, and let $A$ be $∀n (P(n)∨¬P(n))$ for negative $P$ and assume $¬¬A$. A witness for $A$ would be a decision procedure for $P$, while a witness for $¬A⇒A$ would give us nothing, and a witness for $A⅋A$ would gives us two candidate decision procedures for $P$, one of which could be incorrect or even fail to terminate. | |
| Aug 21, 2017 at 11:30 | history | edited | Franka Waaldijk | CC BY-SA 3.0 |
sharpened the mathematical example
|
| Aug 21, 2017 at 11:18 | comment | added | James Smith | No particular reason. It just had a ring to it, you know how it is. I'm glad it came from Errett Bishop. | |
| Aug 21, 2017 at 10:53 | comment | added | Franka Waaldijk | I believe Errett Bishop said this in the foreword to Foundations of Constructive Analysis (1967), why do you ask? | |
| Aug 21, 2017 at 10:39 | comment | added | James Smith | Frank, who said/wrote this...? "Almost every conceivable type of resistance has been offered to a straightforward realistic treatment of mathematics, even by constructivists." | |
| Aug 21, 2017 at 10:14 | history | edited | Franka Waaldijk | CC BY-SA 3.0 |
some better phrasing, clarification
|
| Aug 21, 2017 at 10:07 | history | answered | Franka Waaldijk | CC BY-SA 3.0 |