Timeline for How many constant symbols can a set of intuitionistic formulas have for completeness to hold?
Current License: CC BY-SA 4.0
9 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Sep 24 at 15:47 | comment | added | zaq | @EmilJeřábek This makes a lot of sense! Although I think this should be caused by the fact that Fitting uses one "global" language in his book and doesn't even really define the notion of a language. I think the semantics themselves are equivalent (at least I hope so). Thank you! | |
| Sep 24 at 9:27 | comment | added | Emil Jeřábek | (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.) | |
| Sep 24 at 9:21 | comment | added | Emil Jeřábek | ... 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.) | |
| Sep 24 at 9:19 | comment | added | Emil Jeřábek | 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 ... | |
| Sep 24 at 6:11 | comment | added | zaq | @AndrejBauer Yes, sorry! The relevant chapter is "Additional first order results", the subsection "Compactness". You will be able to find many alternative formulations with the same weird condition there. Also, in my research I've discovered that Fitting uses an unconventional notion of a first-order model, so the chapter on semantics might also be important. | |
| Sep 24 at 5:55 | comment | added | Andrej Bauer | 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? | |
| Sep 24 at 5:36 | comment | added | Monroe Eskew | 237. That’s the limit. | |
| S Sep 24 at 5:23 | review | First questions | |||
| Sep 24 at 5:28 | |||||
| S Sep 24 at 5:23 | history | asked | zaq | CC BY-SA 4.0 |