7
$\begingroup$

According to Cantor's attic, Vopenka's principle is equivalent to the existence of a strong compactness cardinal for any "logic". But I can't find a definition of what a "logic" is either there or in any of the cited references.

Question: What is a "logic" in the sense of this statement?

Some examples are given: apparently infinitary logic $L_{\kappa\kappa}$ is a "logic", and infinitary higher(but finite)-order logic $L_{\kappa\kappa}^n$ is a "logic". Thus Vopenka's principle should imply the existence of a proper class of strongly compact cardinals, and even a proper class of extendible cardinals.

But I don't think it's supposed to be as simple as "Vopenka's principle is equivalent to a proper class of extendibles", so there must be more "logics" than these. The next thing I can think of is some sort of infinitary-order infinitary logic $L^\alpha_{\kappa\kappa}$. It would also make sense to consider structures with infinitary operations. I don't know if there's a large cardinal principle associated to strong compactness for either of these sorts of logic.

And then of course there are "logics" such as various flavors of type theory (which higher order logic starts to resemble anyway!) but just for cultural reasons, I doubt that "logic" is meant to encompass anything along these lines.

Improve this question
$\endgroup$
12
  • 1
    $\begingroup$ @AlecRhea I'm not sure precisely which formulation of Vopenka's principle you're referring to, but I suspect it's one which says "there is no full embedding $Ord \to Gph$" (or various other categories or classes of categories may be substituted for the categorh $Gph$ of graphs). In this context, $Ord$ is viewed as a large poset. Equivalently, it is the category of well-ordered sets $\alpha$ and maps which preserve the operation $min: P(\alpha) \setminus \{\emptyset\} \to \alpha$ (since any such map $\alpha \to \beta$ just embeds $\alpha$ as an initial segment of $\beta$). $\endgroup$
    – Tim Campion ♦
    Sep 6, 2018 at 23:44
  • 1
    $\begingroup$ I would guess that the statement is referring to the notion of "logic" as defined in "abstract model theory". You can find the definition in the section on Lindstrom's theorem in Chang & Keisler's Model Theory or in the book Model Theoretic Logics edited by Barwise and Feferman. $\endgroup$
    – Alex Kruckman
    Sep 7, 2018 at 1:26
  • 1
    $\begingroup$ @AlexKruckman Too late! Ninja'd. You had the right textbook, though, "Model Theoretic Logics" $\endgroup$
    – Keith Millar
    Sep 7, 2018 at 3:56
  • 1
    $\begingroup$ Ok, I found my copy of Chang & Keisler and looked at their definition of abstract logic (Definition 2.5.1 on p. 128). I don't see any issue with making second-order or higher-order logics into abstract logics, as long as their given their intended semantics where e.g. the semantics of quantifying over a predicate is quantifying over the full power set of a structure. What part of the definition seems like a problem to you? $\endgroup$
    – Alex Kruckman
    Sep 7, 2018 at 14:07
  • 1
    $\begingroup$ That's right, you can't do that in the classical second-order/higher-order logic. Of course, you could formulate a logic where the vocabulary has higher order symbols in it. But classical higher-order logics don't have such symbols built into the vocabulary - they only allows you to quantify over higher-order variables. Note, though, that you can axiomatize topological spaces via a third-order formula $\varphi(X)$ in the empty vocabulary with a single third-order free variable $X$, so that $M\models \varphi(\tau)$ if and only if $\tau$ is a topology on $M$. $\endgroup$
    – Alex Kruckman
    Sep 7, 2018 at 15:27

1 Answer 1

Reset to default
4
$\begingroup$

https://www.jstor.org/stable/2273786?seq=1#page_scan_tab_contents Is the article where it is from. It seems to have never been added to the library, which would be my fault.

https://projecteuclid.org/download/pdf_1/euclid.pl/1235417266 is the first chapter of the textbook where I personally found it, although I would use the JSTOR article in the library of Cantor's Attic after this post.

The massive textbook I used is called "Model-Theoretic Logics" by the "Ω-Group" (the coolest pen-name for a group of mathematicians). In Part F, this equivalence is proven.

Chapter XVII is "Set-theoretic definability of logics" (written by Väänänen, one of my heroes) which is where this comes from. The definition is quite nuanced, but it is a great read. I recommend this textbook.

What Is a Logic? (loose definition)

We start with a "vocabulary." $\tau$ is often used for this type of object; it is defined as a (nonempty) class of constant symbols, finitary predicate symbols, and finitary function symbols (simple enough). However, you also have to have "sort symbols" for every function symbol and every constant symbol, and furthermore you have to have sort symbols for every argument of every relation symbol and every input of every function symbol.

The sort symbols are just for well-defining "terms" and their syntactics. The "$\tau$-terms" are built up of just function symbols applied to constant symbols, each of which are then given a "sort" to help define things later.

Using the sort, you can well-define the number of inputs in a given "formula" made out of $\tau$.

An "abstract logic" $\mathcal{L}$ gives every vocabulary $\tau$ a class $\mathcal{L}(\tau)$ of formulae and "atomic $\tau$-formulae of $\mathcal{L}$." More important is that it gives every $\tau$ a relation $\models^\tau$ which defines semantics: how a structure interprets a formula of $\mathcal{L}$.

The kind of logic we are talking about has been formalized by Väänänen, but it suggests that the definitions of $\models^\tau$ and deciding what things are atomic formulae are recursive somewhat (synctatic) and furthermore there is a set $A$ such that every formula of $\mathcal{L}$ is in $A$ and that $\mathcal{L}$ can easily describe this set $A$ (the syntax of $\mathcal{L}$ is representable).

There is a lot more to this definition that I haven't talked about, so this is a very rough summary. I urge you to take a look at the book instead of just taking my word (I am in no ways an expert).

Improve this answer
$\endgroup$
12
  • 1
    $\begingroup$ 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. $\endgroup$
    – Alex Kruckman
    Sep 7, 2018 at 14:17
  • $\begingroup$ @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? $\endgroup$
    – Tim Campion ♦
    Sep 7, 2018 at 15:17
  • $\begingroup$ 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. $\endgroup$
    – Tim Campion ♦
    Sep 7, 2018 at 15:22
  • $\begingroup$ 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. $\endgroup$
    – Tim Campion ♦
    Sep 7, 2018 at 15:45
  • $\begingroup$ @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. $\endgroup$
    – Keith Millar
    Sep 7, 2018 at 16:30

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.