7
$\begingroup$

According to godelian in Henkin-style completeness proofs for intuitionistic logic there are multiple intuitionstically valid proofs of the completeness of inuitionistic predicate calculus (IPC) via modified Kripke models, Category Theory, etc.

I'm inquiring whether there is a proof in terms of Heyting algebra semantics. I've found two completeness proofs using Heyting algebra semantics: the first one for the propositional calculus in Palmgren - Semantics of intuitionistic propositional logic (which I think could be extended to the predicate calculus) and the second one for the predicate calculus in Valentini - A simple proof of the completeness theorem of the intuitionistic predicate calculus with respect to the topological semantics. Both seem to be intuitionistically valid to ME, but I am suspicious of this for multiple reasons. The primary one being that Gödel and Kreisel showed that such a proof (with out modifications) entails non-constructive principles.

Improve this question
$\endgroup$
8
  • 1
    $\begingroup$ First, the linked question does NOT ask for intuitionistic METATHEORY. Whatever I wrote there is only supposed to work in a classical metatheory, I made no claims about its constructive validity. I’m not sure if I had in mind any particular issues with algebraic semantics. The case of predicate logic is more complicated as quantifiers do not correspond to algebraic operations as nicely as connectives, but basically, with a bit of care it works if you take the Lindenbaum–Tarski algebra of the theory in a language expanded with infinitely many new constants. The only substantial issue is ... $\endgroup$
    – Emil Jeřábek
    Commented Jul 30, 2021 at 10:09
  • 1
    $\begingroup$ ... that the Lindenbaum–Tarski algebra is not complete. You have basically two options: (1) You define the semantics so that the Heyting algebras are not required to be complete, only that all suprema and infima actually used when computating valuations in the given model exist. Then the Lindenbaum–Tarski algebra works as is, but the semantics as a whole is quite awkward to use, as it is next to impossible to see whether a given model is actually sound (i.e., that the relevant suprema and infima exist). (2) You define the semantics so that the algebras are required to be complete. ... $\endgroup$
    – Emil Jeřábek
    Commented Jul 30, 2021 at 10:14
  • 1
    $\begingroup$ ... Then you need to embed the Lindenbaum–Tarski algebra in a complete Heyting algebra, and you need to do it in such a way that existing suprema and infima used to compute valuations in the model do not change. The way to do this is to take the Dedekind–MacNeille completion, which is not particularly difficult, but it means you need to do a lot of extra work. $\endgroup$
    – Emil Jeřábek
    Commented Jul 30, 2021 at 10:17
  • $\begingroup$ I was conflating the two comments of the link. The first comment explicitly states that OP is looking for a completeness proof in a "constuctive meta-theory" while you are simply telling OP how one can do henkin-style completeness proofs. Apologies. $\endgroup$
    – ToucanIan
    Commented Jul 30, 2021 at 17:33
  • 1
    $\begingroup$ I see no reason for that either. It is straightforward to present the argument so that given $T$ and $\phi$, you construct a Heyting algebra model such that all axioms of $T$ get value $1$, and such that “if $\phi$ gets value $1$, then $T\vdash\phi$”. I would be rather more concrned whether the constructions of the Lindenbaum–Tarski algebra (which uses a quotient) and, especially, of the Dedekind–MacNeille completion (which uses a power set) can be done in whatever setup for constructive mathematics you are using. But I am no expert in constructive mathematics. $\endgroup$
    – Emil Jeřábek
    Commented Jul 30, 2021 at 18:19

3 Answers 3

Reset to default
7
$\begingroup$

Harry de Swart's PhD from the University of Nijmegen (the Netherlands) was (explicitly) about this kind of topic. He establishes the completeness of IPC using search trees, in an intuitionistic meta theory. I do not know how search trees relate to your question.

H.C.M. de Swart: Intuitionistic logic in intuitionistic metamathematics, Dissertation, 1976, University of Nijmegen. https://core.ac.uk/reader/43594080

de Swart has since left this field, so I do not know if he will answers questions via email.

Improve this answer
$\endgroup$
1
  • $\begingroup$ Thanks for the reply! I've reviewed this PhD thesis and am interested to say the least. At the same time I am inclined to say it is unrelated to Heyting Algebra Semantics. According to escholarship.org/content/qt2vp2x4rx/… Algebraic Semantics are the most general in terms of the hierarchy $\endgroup$
    – ToucanIan
    Commented Jul 9, 2021 at 17:02
3
$\begingroup$

It's going to depend on exactly what you mean by Heyting algebra semantics, but there is a proof in Troelstra and Van Dalen, Constructivism in Mathematics, Vol 2, for what they call $\Theta$-models, where $\Theta$ is a Heyting algebra. The completeness theorem appears as Theorem 6.12.

Improve this answer
$\endgroup$
2
  • $\begingroup$ The version I gained temporary access to did not have numbered theorems. Which chapter contains said theorem? $\endgroup$
    – ToucanIan
    Commented Jul 30, 2021 at 18:16
  • 1
    $\begingroup$ It's in chapter 13 (Semantical completeness), section 6. $\endgroup$
    – aws
    Commented Jul 30, 2021 at 19:11
0
$\begingroup$

I have a completeness proof based on Abstraction Logic, but it is a classical proof: https://doi.org/10.47757/abstraction.logic.1

Also, it is for intuitionistic abstraction logic and all logics extending it.

Improve this answer
$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .