Given a regular logic $\mathcal{L}$, let $\preccurlyeq_\mathcal{L}$ be the usual elementary submodelhood relation for $\mathcal{L}$. There is also a separate submodelhood relation coming from the Tarski-Vaught test: say that $\mathfrak{A}\trianglelefteq_\mathcal{L}\mathfrak{B}$ if $\mathfrak{A}$ is a substructure of $\mathfrak{B}$ and for every $\mathcal{L}$-formula $\varphi$ with parameters from $\mathfrak{A}$ we have $$\varphi^\mathfrak{B}\not=\emptyset\implies \varphi^\mathfrak{B}\cap\mathfrak{A}^{arity(\varphi)}\not=\emptyset.$$

Usually $\trianglelefteq_\mathcal{L}$ is strictly between $\subseteq$ and $\preccurlyeq_\mathcal{L}$. Now every logic $\mathcal{L}$ has a distinguished fragment which "plays nicely" with this substructurehood relation, namely $$\mathcal{L}_{TV}:=\{\varphi\in\mathcal{L}: \mathfrak{A}\trianglelefteq_\mathcal{L}\mathfrak{B}\implies\varphi^\mathfrak{A}=\varphi^\mathfrak{B}\cap\mathfrak{A}^{arity(\varphi)}\}.$$ In general we need not have $\mathcal{L}_{TV}=(\mathcal{L}_{TV})_{TV}$, and so we can non-boringly iterate this process through the ordinals:

  • $\mathcal{L}_{TV(0)}=\mathcal{L}$,

  • $\mathcal{L}_{TV(\alpha+1)}=(\mathcal{L}_{TV(\alpha)})_{TV}$, and

  • $\mathcal{L}_{TV(\lambda)}=\bigcap_{\alpha<\lambda}\mathcal{L}_{TV(\alpha)}$ for $\lambda$ limit.

I've asked at MSE about one aspect of this process applied to second-order logic for a single step; here I'd like to ask an orthogonal question. Let the TV-number of a logic $\mathcal{L}$ be the least $\gamma$ such that $\mathcal{L}_{TV(\gamma)}=\mathcal{L}_{TV(\gamma+1)}$.

What is the TV-number of second-order logic?

Embarrassingly, as far as I know we could have $\gamma=1$ (we can't have $\gamma=0$ since $\mathsf{SOL}_{TV}$ has the full downward Lowenheim-Skolem property). I'd separately be interested in any references about this construction; the abstract model theory literature is messy, and I'd like to avoid reinventing as many wheels as possible.

Motivation: The $TV$-process is basically a quick way of whipping up logics with the downward Lowenheim-Skolem property or analogues thereof (count the formulas and think about Skolem functions), but given that it's not idempotent the "$TV^\infty$-process" $\mathcal{L}\leadsto \bigcap_{\alpha\in \mathit{Ord}}\mathcal{L}_{TV(\alpha)}$ may actually be a more natural way of producing such logics. I'm especially interested in second-order logic and its fragments, and so this question is basically a step towards figuring out which of $TV$ or $TV^\infty$ I should be thinking about at the moment.

  • 2
    $\begingroup$ I was going to ask about iterating the $TV$ operator on your other question, but I never got around to it. $\endgroup$ Mar 15, 2021 at 0:01
  • 3
    $\begingroup$ I hereby propose that the process be called "televise" as in "Noah televised second-order logic". $\endgroup$ Mar 17, 2021 at 8:05


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.