Timeline for Vopenka's principle is equivalent to the existence of a strong compactness cardinal for any "logic"?
Current License: CC BY-SA 4.0
20 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Aug 20, 2023 at 17:48 | history | edited | Keith Millar | CC BY-SA 4.0 |
minor syntax issues
|
| Aug 19, 2023 at 23:52 | history | edited | Keith Millar | CC BY-SA 4.0 |
added 5404 characters in body
|
| Jun 15, 2020 at 7:27 | history | edited | CommunityBot |
Commonmark migration
|
|
| Sep 10, 2018 at 15:50 | vote | accept | Tim Campion | ||
| Sep 9, 2018 at 9:37 | comment | added | Jiří Rosický | Look at www1.maths.leeds.ac.uk/~pmtadb/AccessibleCategories2018/… | |
| Sep 7, 2018 at 19:28 | comment | added | Keith Millar | @TimCampion No problem, it's good to formally define things in a compact and straightforwards way. | |
| Sep 7, 2018 at 17:49 | comment | added | Tim Campion | @KeithMillar I see, thanks. Sorry to harp on about this, but what I'm driving at is that the sorts in Ebbinghaus' notion of "logic" have nothing whatsoever to do with higher order entities -- in fact, the isomorphism-invariance rule for satisfaction entails that the sorts of the vocabulary may only be first-order sorts, and therefore the functions / relations in the vocabulary are also necessarily first-order, just as in Chang and Keisler's definition, or in classical higher-order logic according to Alex Kruckman in the comments above. | |
| Sep 7, 2018 at 17:30 | comment | added | Keith Millar | @TimpCampion by complex I mean that it isn't quite intuitive or layman. However, you are correct that it is much more compact and quicker/more straightforwards. You are also correct that it can't represent all higher-order entities. | |
| Sep 7, 2018 at 17:14 | comment | added | Tim Campion | But we can't actually do this, again because of isomorphism-invariance. | |
| Sep 7, 2018 at 17:14 | comment | added | Tim Campion | Then for each $x \in X$ and $R \in P$ we need some sort of formula $\epsilon(x,R)$ whose interpretation is that $x \in R$. The first option would be to add $\epsilon$ to the signature. But then by isomorphism-invariance, we are essentially required to use Henkin semantics, which means we're not really doing second-order logic at all. The second option would be to have a rule in our logic which adds a formula $\epsilon(x,R)$ automatically, and stipulates that in the semantics, this formula can only be satisfied if the interpretation $[P]$ of $P$ is the powerset of $[X]$. | |
| Sep 7, 2018 at 17:13 | comment | added | Tim Campion | @KeithMillar I don't understand your second sentence -- I just gave Ebbinghaus' complete definition in one comment and it didn't seem particularly complex to me. Regarding your first sentence, the fact that a logic may have many sorts does not imply that its sorts may adequately represent higher-order entities. In fact, I see two ways to try to fit higher-order symbols in Ebbinghaus' framework, both of which seem problematic. Let's say we want to formalize a theory with one first-order sort $X$ and one second-order sort $P$ where $P$ represents the powerset of $X$. | |
| Sep 7, 2018 at 16:34 | history | edited | Keith Millar | CC BY-SA 4.0 |
clarifying that i'm not a reliable source
|
| Sep 7, 2018 at 16:30 | comment | added | Keith Millar | @TimCampion This logic already includes higher-order function and relation symbols, as it is many-sorted. But that definition is much more formal and accurate, even though it is a lot more complex. | |
| Sep 7, 2018 at 15:45 | comment | added | Tim Campion | The definition of "logic" in Model-Theoretic Logics is in Ebbinghaus' Ch II. It can be summarized as follows. Many-sorted first-order vocabularies form a category $Voc$ under injective well-typed maps. First-order structures form a functor $Str: Voc^{op} \to Cl$ where $Cl$ is the category of classes. A "logic" is a functor $Lang: Voc\to Cl$ equipped with a dinatural transformation $\models:Lang \times Str \to 2$ where $2$ is the constant functor at $\{0,1\}$. Of course, there's still the ambiguity of what a class or class function is. | |
| Sep 7, 2018 at 15:22 | comment | added | Tim Campion | I suspect this notion of "logic" is not the "utlimate" notion of "logic" for which a similar theorem holds. For example, Theorem 6.9 here suggests to me that one could get a similar theorem for higher-order logics which allow the vocabulary to include higher-order function / relation symbols. | |
| Sep 7, 2018 at 15:17 | comment | added | Tim Campion | @KeithMillar There are a bunch of classes which appear both in Vopenka's principle and in the definition of a logic. In this theorem, are these to be interpreted as definable classes in ZFC, or are we working in NBG or something? | |
| Sep 7, 2018 at 14:17 | comment | added | Alex Kruckman | More precisely, the result in question is Part F, Chapter XVIII, Theorem 1.5.17 on p. 661 of Model Theoretic Logics and is attributed to Makowsky. | |
| Sep 7, 2018 at 3:36 | history | edited | Keith Millar | CC BY-SA 4.0 |
defining things
|
| Sep 7, 2018 at 3:12 | history | edited | Keith Millar | CC BY-SA 4.0 |
oof
|
| Sep 7, 2018 at 2:49 | history | answered | Keith Millar | CC BY-SA 4.0 |