Welcome to MathOverflow

Question

8

5

Is there a version of the Löwenheim-Skolem theorem in intuitionistic logic? I'm particularly interested in the "downward" form. The standard proof I know uses the Tarski-Vaught test for elementary substructures, which in turn relies on the fact that "forall" is equivalent to "not exists not", and that fails intuitionistically.

edited Feb 26 2010 at 9:43

Charles Stewart
1,669●8●15

asked Oct 28 2009 at 1:36

Mike Shulman
17.2k●20●70

Kristal Cantwell · Accepted Answer · 2009-10-31 06:05:08Z UTC

I have a reference that says the downward Löwenheim-Skolem theorem does not occur in intuitionistic logic. In the words of the abstract "even a very powerful version of intuitionistic set theory does not yield any of the usual forms of a countable downward Löwenheim-Skolem theorem."

Skolem's paradox and constructivism Journal of Philosophical Logic Springer Netherlands Issue Volume 16, Number 2 / May, 1987

http://www.springerlink.com/content/t28583t748301t04/

Also page 341 of A Companion to Metaphysics By Jaegwon Kim

"...there is no intuitionistically acceptable analogue of the classical downward Löwenheim-Skolem theorem"

Emil Jeřábek · Answer 2 · 2011-02-04 15:12:19Z UTC

Is the question about the Löwenheim–Skolem theorem for classical models in intuitionistic metatheory, or about the Löwenheim–Skolem theorem for intuitionistic (Kripke) models in classical metatheory? The latter certainly holds. One can prove it easily by realizing that a Kripke model can be represented by a suitable two-sorted classical model in such a way that satisfaction of any intuitionistic formula in the original model is first-order definable in the representation, and then applying the classical Löwenheim–Skolem theorem.

Kirill Levin · Answer 3 · 2009-10-30 03:09:22Z UTC

1

It's been a while, but I think Ebbinghaus, Flum & Thomas, in the book Mathematical Logic, get the Löwenheim-Skolem theorems as a byproduct of the completeness theorem, which they prove using the Henkin construction. And I think that is fully constructivist.

answered Oct 30 2009 at 3:09

Kirill Levin
273●2●7

As far as I can tell, the only logic used in that book is classical. On page 34 in my edition, they say explicitly that they will not use ∀ any more because it can be replaced by ¬∃¬, and similarly for ∧ and →; this is okay classically but not intuitionistically. Then the proof of Henkin's Theorem (p79-80 in my edition) proceeds by an induction on the construction of formulas, considering only the cases ¬, ∨, and ∃. Again, this is allowable classically, but not intuitionistically. – Mike Shulman Oct 30 2009 at 19:53

But I think they only do it to shorten the proofs. That is not to say that all the proofs in the book are secretly valid intuitionistic proofs. I suppose it would be a worthy exercise to try and prove the omitted cases of the Henkin proof intuitionistically. – Kirill Levin Oct 31 2009 at 5:22

I'll believe it when I see it. (-: – Mike Shulman Oct 31 2009 at 16:50

2

I wouldn't have thought that the Henkin construction is constructivist. Certainly, to even begin the Henkin construction you need a complete extension of the consistent theory you start with, and the standard Lindenbaum construction of this complete extension involves enumerating the sentences of the language, and then in turn adding each one if it is consistent and its negation if not. That disjunction assumes excluded middle. – Kenny Easwaran Nov 6 2009 at 6:28

Intuitionistic Lowenheim-Skolem?

Remember to vote up questions/answers you find interesting or helpful (requires 15 reputation points)

3 Answers

You can accept an answer to one of your own questions by clicking the check mark next to it. This awards 15 reputation points to the person who answered and 2 reputation points to you.