Timeline for Adding nonconstructive disjunction to intuitionistic logic
Current License: CC BY-SA 3.0
20 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Aug 23, 2017 at 2:47 | comment | added | Dmytro Taranovsky | The reason the introduction rule is (in your words) 'weird' is that it combines introduction and cut, while (if possible) we would like cut-elimination to hold. I revised my posting with my now clearer understanding of the properties of '⅋'. | |
| Aug 22, 2017 at 11:19 | comment | added | Andrej Bauer | @მამუკაჯიბლაძე: yes, that looks right (about $\lnot A \to B$). | |
| Aug 22, 2017 at 10:59 | comment | added | Andrej Bauer | Ok, I changed my comment, and just gave the intro rule, which can be read off directly. | |
| Aug 22, 2017 at 10:59 | history | edited | Andrej Bauer | CC BY-SA 3.0 |
deleted 455 characters in body
|
| Aug 22, 2017 at 10:54 | comment | added | Andrej Bauer | Oops, you're totally right, I got my encoding wrong. Sorry about that. | |
| Aug 22, 2017 at 10:52 | comment | added | მამუკა ჯიბლაძე | As for your $\lor_\Omega$, I think I have a proof that this is exactly $\neg A\to B$. Indeed if $\neg A\to B$ holds then we might take $X=A$ in $\exists X\ (X\to A)\land(\neg X\to B)$, while if $\exists X\ (X\to A)\land(\neg X\to B)$ holds and $\neg A$ also holds then $\exists X\ (\neg X)\land(\neg X\to B)$ holds too, which implies $B$. | |
| Aug 22, 2017 at 10:38 | comment | added | მამუკა ჯიბლაძე | Hmm then $\varphi=\exists\ X\ \psi$, which would give$$[\exists\ X\ \psi]\iff[\forall Y\ (\forall\ X\ (\psi\to Y))\to Y]$$ | |
| Aug 22, 2017 at 10:36 | comment | added | Andrej Bauer | Yea I am using the ••Church encoding** of existential quantifier in terms of universal quantifier in higher order logic it's not specific to realizability. | |
| Aug 22, 2017 at 10:34 | comment | added | მამუკა ჯიბლაძე | Again, maybe this is realizability specifics? In the general case, I just mean applying$$\varphi\iff\forall\ Y\ (\varphi\Rightarrow Y)\Rightarrow Y$$to $\varphi=\exists\ X\ (\neg X\to A)\land(\neg\neg X\to B)$. Are you using something stronger? | |
| Aug 22, 2017 at 10:26 | comment | added | Andrej Bauer | Really? That's not how we usually encode the existential. (Think of the elimination rule) | |
| Aug 22, 2017 at 10:14 | comment | added | მამუკა ჯიბლაძე | Is it obvious that you might use the same $X$ inside and outside? Theoretically it should be$$\forall\ Y[\forall\ X(((\neg X\to A)\land(\neg\neg X\to B))\to Y)]\to Y$$ | |
| Aug 22, 2017 at 9:38 | comment | added | Andrej Bauer | I added a remark on what the elimination rule for $\par$ ought to look like. It's not pretty. | |
| Aug 22, 2017 at 9:38 | history | edited | Andrej Bauer | CC BY-SA 3.0 |
added 710 characters in body
|
| Aug 21, 2017 at 22:50 | comment | added | Andrej Bauer | Yes, I think the binary objects are (up to isomorphism) the $\lnot\lnot$-dense subobjects of $\Omega_{\lnot\lnot}$. I mentioned that in the answer. I think we could have gone for something a bit more general, actually, and take them to be $\lnot\lnot$-dense subjobjects of $\Omega$. Hmm, what is $A \lor_\Omega B$? It's $\exists X \in \Omega . (X \Rightarrow A) \land (\lnot X \Rightarrow B)$, what is that? | |
| Aug 21, 2017 at 22:38 | comment | added | მამუკა ჯიბლაძე | Does "binary" have an abstract characterization, independent of the realizability specifics? | |
| Aug 21, 2017 at 22:32 | history | edited | Andrej Bauer | CC BY-SA 3.0 |
added 7 characters in body
|
| Aug 21, 2017 at 20:03 | history | edited | Andrej Bauer | CC BY-SA 3.0 |
added 174 characters in body
|
| Aug 21, 2017 at 16:41 | history | edited | Andrej Bauer | CC BY-SA 3.0 |
deleted 18 characters in body
|
| Aug 21, 2017 at 16:35 | history | edited | Andrej Bauer | CC BY-SA 3.0 |
added 1123 characters in body
|
| Aug 21, 2017 at 16:13 | history | answered | Andrej Bauer | CC BY-SA 3.0 |