Timeline for Is intuitionistic predicate logic (semantically) complete or incomplete?
Current License: CC BY-SA 4.0
14 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Sep 30, 2021 at 23:05 | history | edited | ToucanIan | CC BY-SA 4.0 |
added 463 characters in body
|
| Sep 30, 2021 at 15:58 | history | edited | ToucanIan | CC BY-SA 4.0 |
added 40 characters in body
|
| Sep 29, 2021 at 20:07 | comment | added | ToucanIan | @MattF. that's fair. | |
| Sep 29, 2021 at 20:01 | comment | added | ToucanIan | @AlexKruckman that is a good point! I was not thinking about increased generality weakening the set of entailments. I'm still hoping for an answer that clears all this up. | |
| Sep 29, 2021 at 16:37 | comment | added | Alex Kruckman | @ToucanIan "How can $\Gamma$ semantically entail $A$, but a Heyting algebra not capture this semantic entailment"? Maybe $\Gamma$ has a Heyting algebra model, but no set-based model (possibly because producing a set-based model from a Heyting algebra model is non-constructive and we're working in an intuitionistic metatheory). Then $\Gamma$ entails $\bot$ from the point of view of set-based models, but not from the point of view of Heyting algebra models. The point being that a semantics which is more general (in the sense of having models for more theories) will have fewer entailments. | |
| Sep 29, 2021 at 16:32 | comment | added | user44143 | @Toucanlan, unfortunately, figuring that out would require a deeper dive into the preceding 717 pages of Troelstra's book than I am up for at the moment. | |
| Sep 29, 2021 at 16:01 | comment | added | ToucanIan | @MattF. You may be right, but from my other research into the topic I have found the algebraic semantics are the most general semantics. How can $\Gamma$ semantically entail $A$, but a Heyting Algebra not capture this semantic entailment? I fail to see how these would be consistent. | |
| Sep 29, 2021 at 15:55 | comment | added | ToucanIan | @MattF. It has different meanings in different sections. In the sections where IQC is proven it is said (on page 714) to mean the following: "$[[A]] = \top$ in each $\Omega$-model for which $[[B]] = \top$ for all $B \in \Gamma$." The brackets are the notation used for $\Omega$-valuations, and $\Omega$-model is essentially a complete Heyting Algebra that is a model (but not quite). | |
| Sep 29, 2021 at 5:40 | comment | added | user44143 | Perhaps Troelstra is making the claim “if $H\!A$ proves that $\Gamma$ semantically entails $A$, then $\Gamma$ proves $A$“. And meanwhile McCarty is denying the claim “if $\Gamma$ semantically entails $A$, then $\Gamma$ proves $A$“. These would be consistent, and in McCarty’s examples with $A$ an unprovable instance of tertium non datur, $\Gamma$ semantically entails $A$, this semantic entailment is not $H\!A$-provable, and $\Gamma$ does not prove $A$. | |
| Sep 29, 2021 at 5:28 | comment | added | user44143 | In the first link, what does Troelstra mean by the subscript in $\Gamma\ |\!\!\vdash_{cHa}A$ ? | |
| Sep 29, 2021 at 0:54 | history | edited | ToucanIan | CC BY-SA 4.0 |
added 620 characters in body
|
| Sep 29, 2021 at 0:33 | comment | added | ToucanIan | Good point. The first source uses Algebraic Semantics. The second source says, "IZF demonstrate explicitly that propositional and predicate intuitionistic logic and all the nonclassical intermediate logics are incomplete relative to, for example, Tarski semantics." But it seems that the choice of Tarski Semantics is somewhat arbitrary in this statement. | |
| Sep 28, 2021 at 23:40 | comment | added | Alex Kruckman | Are these two sources talking about the same semantics? | |
| Sep 28, 2021 at 22:49 | history | asked | ToucanIan | CC BY-SA 4.0 |