Timeline for Is there a semantics for intuitionistic logic that is meta-theoretically "self-hosting"?
Current License: CC BY-SA 4.0
16 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jan 29, 2022 at 16:01 | comment | added | AnduinWilde | It seems Andrew Bacon's Non-classical Metatheory for Non-classical Logics related here. | |
| Feb 25, 2021 at 3:31 | comment | added | Dan Doel | Those two sets are isomorphic, yes. The problem is that neither of those is isomorphic to the powerset of a singleton. The more obvious is the latter, where: $x \in \{\varnothing,\{1\}\} → x = \varnothing ∨ x = \{1\}$. If $\mathcal P\{1\}$ were that set, then we would have $\{1|φ\} = \varnothing ∨ \{1|φ\} = \{1\}$, which is equivalent to $¬φ ∨ φ$. Your semantics are actually classical as given, because $M(p) = 0 ∨ M(p) = 1$. By using a powerset, you could give a value for $p$ that is a subsingleton whose equality with $1$ is equivalent to an undecidable proposition. | |
| Feb 25, 2021 at 1:22 | comment | added | ttbo | @DanDoel I don't think I understand what you are saying there. Do you agree that even in an intuitionistic meta-theory, the set $\{0,1\}$ and the set $\{\varnothing,\{1\}\}$ are isomorphic? In that case the important point is that we don't get to assume we have proofs about statements like $M(p) = y$. Re-interpreting the co-domain of $M$ in some other form seems like a matter of style. | |
| Feb 24, 2021 at 18:21 | comment | added | Dan Doel | The power set of $\{1\}$ contains all subsingleton sets $\{1|φ\}$. Asserting that every subsingleton is either $0$ or $1$ is asserting excluded middle for every such $φ$. | |
| Feb 24, 2021 at 1:36 | comment | added | ttbo | The powerset of $\{1\}$ is just two values, so it seems the same as using $\{0,1\}$. Why is it important to use the powerset? | |
| Feb 24, 2021 at 1:30 | vote | accept | ttbo | ||
| Feb 23, 2021 at 12:40 | comment | added | Andrej Bauer | You should not be using $\{0, 1\}$ for truth values. Use the powerset of $\{1\}$ instead. | |
| Feb 23, 2021 at 7:48 | history | edited | ttbo | CC BY-SA 4.0 |
summarize my understanding of one of the answers
|
| Feb 19, 2021 at 19:05 | answer | added | aws | timeline score: 9 | |
| Feb 19, 2021 at 18:14 | history | became hot network question | |||
| Feb 19, 2021 at 17:36 | answer | added | Mike Shulman | timeline score: 13 | |
| Feb 19, 2021 at 14:51 | comment | added | cody | Quite related: mathoverflow.net/q/320186/36103 | |
| Feb 19, 2021 at 13:42 | answer | added | Sam Sanders | timeline score: 8 | |
| Feb 19, 2021 at 9:22 | comment | added | David Roberts♦ | Maybe not an answer, but the meaning explanation of type theory comes to mind. This is due to Per Martin-Löf. I think it is almost surely the case that people have considered your question before, but I don't know where or who (see also: Jonathan Sterling, Type Theory and its Meaning Explanations, arXiv:1512.01837) | |
| Feb 19, 2021 at 8:04 | review | First posts | |||
| Feb 19, 2021 at 12:55 | |||||
| Feb 19, 2021 at 7:58 | history | asked | ttbo | CC BY-SA 4.0 |