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.

  • 3
    $\begingroup$ Are these two sources talking about the same semantics? $\endgroup$ Sep 28 '21 at 23:40
  • 1
    $\begingroup$ In the first link, what does Troelstra mean by the subscript in $\Gamma\ |\!\!\vdash_{cHa}A$ ? $\endgroup$
    – Matt F.
    Sep 29 '21 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$
    – Matt F.
    Sep 29 '21 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$
    – Matt F.
    Sep 29 '21 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$ Sep 29 '21 at 16:37

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.