1
$\begingroup$

Fitting proves a version of the completeness theorem for intuitionistic FOL in his book on intuitionistic model theory and forcing.

Let $U$ be any set of formulas without parameters (i.e. constant symbols). Then $U \vdash X$ (in the intuitionistic sense) iff in any model $\mathcal{G}$, for any $\Gamma \in \mathcal{G}$, if $\Gamma \vDash U$, $\Gamma \vDash X$.

He later elaborates:

This may be extended to sets $S$ with some parameters. To be precise, to any set $S$ which leaves unused a countable collection of parameters.

First of all, let me clarify that Fitting uses the unfortunately common approach of only defining a first-order language with a countable set of parameters. So it is unclear to me how we could generalize this how languages are usually defined, so with a possibly uncountable set of parameters. If I had a language with $\kappa$ parameters, would this theorem now hold if a countable number were left out or if $\kappa$ many were left out?

I'm also looking for a proof of this fact (it's not as easily googlable as it may seem) and I wonder why we even need this condition. After all, this is not required in the classical case.

Improve this question
$\endgroup$
7
  • $\begingroup$ 237. That’s the limit. $\endgroup$
    – Monroe Eskew
    Commented Sep 24 at 5:36
  • 1
    $\begingroup$ I apologize for Monroe's "humor", dear new contributor. Also, it would help if you gave the title of the book. Is it "Intuitionistic Logic Model Theory and Forcing.", North-Holland Publishing Co., Amsterdam, 1969? $\endgroup$
    – Andrej Bauer
    Commented Sep 24 at 5:55
  • 2
    $\begingroup$ This sounds like some kind of an irrelevant technicality in Fitting’s approach. See, even in the usual Henkin-style proof of completeness of classical FOL, you need to extend the language with $\kappa$ many new constants, where $\kappa$ is the cardinality of the language (or $\aleph_0$ if the latter is finite). If, for some reason, you want to work in a framework where the language is fixed and cannot increase (e.g., if you have problems with book-keeping, which might well be more of an issue for intuitionistic logic), you have to assume that $\kappa$ many of the constant symbols ... $\endgroup$
    – Emil Jeřábek
    Commented Sep 24 at 9:19
  • 2
    $\begingroup$ ... are unused for this construction to go through. So this would suggest that the answer is $\kappa$ rather than $\aleph_0$ for uncountable languages. Anyway, in the usual set-up, the completeness of intuitionistic FO wrt Kripke models holds for arbitrary theories (sets of sentences) in arbitrary languages without any restrictions on unused “parameters”. (Which should follow from Fitting’s approach anyway: formally extend the language with $\kappa$ new constants, apply Fitting’s theorem, and forget about the interpretations of the new constants to get back to the original language.) $\endgroup$
    – Emil Jeřábek
    Commented Sep 24 at 9:21
  • 2
    $\begingroup$ (To clarify, I haven’t looked at the source to check what exactly Fitting does. But as you write yourself that “Fitting uses an unconventional notion of a first-order model”, this should be the explanation.) $\endgroup$
    – Emil Jeřábek
    Commented Sep 24 at 9:27

0

Reset to default

You must log in to answer this question.

Browse other questions tagged .