4
$\begingroup$

According to Constructivism in Mathematics: An Introduction by Troelstra A.S. and Van Dalen (https://archive.org/details/constructivismin0002troe/page/718/mode/2up) it is proven in an intuitionisitc meta-theory (as well as a classical meta-theory) that Intuitionistic Predicate Logic is (semantically) complete with respect to Heyting Algebra semantics.

Acoording to Completeness and Incompleteness for Intuitionistic Logic by Charles McCarty (https://www-jstor-org.libsrv.wku.edu/stable/pdf/27590334.pdf?refreqid=excelsior%3A6a685f26e8f7160e6a8acd8600fde1e7) it is shown that IZF (intuitionstic set theory) proves that Intuitionistic Predicate Logic is (semantically) incomplete.

I understand that the two results are NOT contradictory because they are with respect to different semantics. But I'm curious if anyone has analyzed the differences between these semantics too any further depth and can offer any insight on this curious situation.

Additionally, upon further inspection I noticed that in the Semantic Completeness chapter of Troelstra there is a section Incompleteness Results which states: "The results of the previous section (which contained a completness proof) might lead us to believe that completeness for full IQC (this is the abbreviaton for intuitionistic predicate calculus in Troelstra) ... is within reach. We shall show that, nevertheless, we cannot expect to aceive this."

What exactly is full IQC and why does it fail to be complete? Does Heyting Algebra Semantics prove completeness for full IQC while Kripke or beth semantics do not?

Edit: Increasing the clarity of the question in light of the comment section of this post and Henkin-style completeness proofs for intuitionistic logic.

Improve this question
$\endgroup$
10
  • 3
    $\begingroup$ Are these two sources talking about the same semantics? $\endgroup$
    – Alex Kruckman
    Commented Sep 28, 2021 at 23:40
  • 1
    $\begingroup$ In the first link, what does Troelstra mean by the subscript in $\Gamma\ |\!\!\vdash_{cHa}A$ ? $\endgroup$
    – user44143
    Commented Sep 29, 2021 at 5:28
  • 1
    $\begingroup$ 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$. $\endgroup$
    – user44143
    Commented Sep 29, 2021 at 5:40
  • 1
    $\begingroup$ @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. $\endgroup$
    – user44143
    Commented Sep 29, 2021 at 16:32
  • 3
    $\begingroup$ @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. $\endgroup$
    – Alex Kruckman
    Commented Sep 29, 2021 at 16:37

0

Reset to default

You must log in to answer this question.

Browse other questions tagged .