Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
I have added some sketchy remarks on Lindström’s theorem on first-order logic and a reference to predicate logic. Expert logicians hopefully can live with this or improve on it.
I have revised and expanded the entry on the Löwenheim-Skolem theorem a bit. Hope the slight rewriting is ok!
Following the suggestions in the thread on geometric logic here, I’ve tried to be more explicit in predicate logic that the remarks on Lindström’s theorem there talk only about the standard fragment of first-order logic.
Thomas, I have made some of your references to ‘standard [finitary] first-order logic’ say ‘classical untyped first-order logic’, since this is the standard (going back at least to Hilbert), the one relevant to Lindström’s Theorem, and more precise. But change that if you don't think that it says what needs to be said.
I guess you have much better feel for what terms to use in order to get the message through to the nlab’s intended readership. So if by any chance you happen to pass at Lindström’s theorem you might find other occasions to check or harmonize the terminology.
Concerning ’untyped’, (the reason why I absorbed it into the vague term ’standard’ is probably that) I somewhat fancy the idea that the equivalence of coherent logic to classical first-order logic over the class of Boolean toposes (a point that Lawvere likes to stress) could actually be subsumed under a typed version of the Lindström theorem with a categorical (well-pointed?) Boolean semantics which then of course is going to be interpreted as a characterization of coherent logic namely that there is no logical system that is more expressive than coherent logic and satisfies compactness and the Löwenheim-Skolem theorem.
Well, that would be pretty cool if true!
I am rather optimistic that a Lindstöm type theorem holds over a sufficiently tame class of Boolean toposes (let’s say with enough points and an NNO). E.g. Väänänen suggests that the Craig interpolation theorem entails Lindström type results; and interpolation should already be established for coherent logic by Pitts and Makkai. I am rather afraid that the resulting Lindström theorem is straightforwardly just the classical result and would not offer anything new besides the possibility to spread the rumor that coherent logic is the only logic (well, probably I am naive, seen how much work Makkai has to invest in his monograph to get definability for Boolean pretoposes!). But to look seriously into this would take me too far afield: I was only trying to get my monadic SOL together for the Jonsson-Tarski-topos before Todd talked me into this.
1 to 9 of 9