Timeline for Two simple cases of quantifier elimination for Heyting algebras
Current License: CC BY-SA 4.0
23 events
when toggle format | what | by | license | comment | |
---|---|---|---|---|---|
Nov 11, 2021 at 5:02 | history | edited | მამუკა ჯიბლაძე | CC BY-SA 4.0 |
Changed title in view of a simpler case added
|
Nov 10, 2021 at 7:36 | history | edited | მამუკა ჯიბლაძე | CC BY-SA 4.0 |
added a simpler case
|
Oct 30, 2020 at 18:31 | history | edited | მამუკა ჯიბლაძე | CC BY-SA 4.0 |
the abbreviation is never used
|
Oct 30, 2020 at 17:50 | history | edited | Emil Jeřábek |
no arithmetic is mentioned anywhere in the question
|
|
Oct 30, 2020 at 17:28 | history | edited | YCor |
edited tags
|
|
Oct 30, 2020 at 17:21 | comment | added | მამუკა ჯიბლაძე | @AndrejBauer That's more adequate, thanks | |
Oct 30, 2020 at 17:17 | comment | added | მამუკა ჯიბლაძე | @MattF. Tried another title, please have a look | |
Oct 30, 2020 at 17:17 | history | edited | მამუკა ჯიბლაძე | CC BY-SA 4.0 |
Tried another title
|
Oct 29, 2020 at 19:18 | comment | added | LSpice | While I agree that the body is improved, I think the original title was clearer. | |
Oct 29, 2020 at 19:15 | history | edited | Andrej Bauer | CC BY-SA 4.0 |
deleted 23 characters in body
|
Oct 29, 2020 at 19:13 | comment | added | Andrej Bauer | In the question, do we have to say "$\neg p$ leads to contradiction" instead of just "$\neg p$ is false"? And as long as I am whining, the "provably" is vacuous, it should go. | |
Oct 29, 2020 at 17:28 | comment | added | მამუკა ჯიბლაძე | @MattF. Just noticed that you also changed the title. While yours is more clear, I think it is sort of misleading. However I must admit I don't see how to improve it further... | |
Oct 29, 2020 at 17:17 | comment | added | მამუკა ჯიბლაძე | @FrankaWaaldijk Accordingly, here is an example when neither $p$ nor $p'$ has form $\neg r\lor\neg\neg r$. Consider the algebra of up-sets of the poset $x<X>0<X'>x'$, and let $p=\{X,X',x'\}$, $p'=\{x,X,X'\}$. They satisfy the requirement with $q=\{X\}$ and $q'=\{X'\}$. However the only two up-sets of the form $\neg r\lor\neg\neg r$ are the whole poset and the whole poset except $0$. | |
Oct 29, 2020 at 16:59 | comment | added | მამუკა ჯიბლაძე | @MattF. Excellent, thank you very much! This is WAY clearer than what I wrote! | |
Oct 29, 2020 at 16:16 | history | edited | user44143 | CC BY-SA 4.0 |
streamlined
|
Oct 29, 2020 at 15:40 | history | edited | მამუკა ჯიბლაძე | CC BY-SA 4.0 |
highlighted the question
|
Oct 29, 2020 at 15:35 | comment | added | მამუკა ჯიბლაძე | @FrankaWaaldijk Great observation! This also relates to another instance of the same question which I decided to omit here: whether one can characterize those $p$ of the form $\neg r\lor\neg\neg r$. This is definitely more restrictive than just $\neg\neg p$: for example, in the duality semantics $\neg\neg p$ means that the corresponding up-set of the dual space contains the whole maximum of the dual space, while if $p$ is $\neg r\lor\neg\neg r$ then in addition this up-set must contain all those points which see unique maximal point. | |
Oct 29, 2020 at 15:24 | comment | added | მამუკა ჯიბლაძე | @MattF. I've highlighted the question, and also tried to make it more precise, is it better now? | |
Oct 29, 2020 at 15:23 | history | edited | მამუკა ჯიბლაძე | CC BY-SA 4.0 |
highlighted the question
|
Oct 29, 2020 at 14:29 | comment | added | Franka Waaldijk | Yes... but I wonder if it's possible. An example I believe to be revealing is this: $p = r\vee \neg r$ and $p'= \neg r\vee \neg\neg r$. We can then take $q=r, q'=\neg r$. Still, neither $p$ or $p'$ is a theorem in IPL, so that particular simplification that I had in mind does not always hold... perhaps some other simplification is possible. | |
Oct 29, 2020 at 14:00 | comment | added | Andrej Bauer | So we're looking for something like "$\neg \neg p$ and $\neg \neg q$ and ..."? | |
Oct 29, 2020 at 13:25 | comment | added | Franka Waaldijk | Sorry! I gave an incorrect answer, and deleted it. Still, this means that I will upvote the question (I thought it was simple...). | |
Oct 29, 2020 at 7:53 | history | asked | მამუკა ჯიბლაძე | CC BY-SA 4.0 |