Timeline for Intuitionistic Lowenheim-Skolem?
Current License: CC BY-SA 2.5
5 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Nov 6, 2009 at 6:28 | comment | added | Kenny Easwaran | 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. | |
| Oct 31, 2009 at 16:50 | comment | added | Mike Shulman | I'll believe it when I see it. (-: | |
| Oct 31, 2009 at 5:22 | comment | added | Kirill Levin | 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. | |
| Oct 30, 2009 at 19:53 | comment | added | Mike Shulman | 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. | |
| Oct 30, 2009 at 3:09 | history | answered | Kirill Levin | CC BY-SA 2.5 |