Skip to main content
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