Skip to main content
3 of 4
added 40 characters in body
ToucanIan
  • 411
  • 2
  • 10

Is intuitionistic predicate logic (semantically) complete or incomplete?

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.

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 proven that IZF (intuitionstic set theory) proves that Intuitionistic Predicate Logic is (semantically) incomplete.

I am unsure how to reconcile these two results.

Edit: FIrst and formost. I am now aware that the semantics involved in the proof of the two claims are in fact different. 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."

If so, my next question is: what exactly is full IQC and why does it fail to be complete?

ToucanIan
  • 411
  • 2
  • 10