Question 1: I'm interested in fragments of universal second-order logic (USO) that are known to be compact. Are there any that, for example, include negation or first-order existential quantification?
Question 2: More generally (and vaguely), what is the approximate limit (in an intuitive sense) of how expressive a fragment of USO that's constrained to be compact can be?
Background/Assumptions:
I'll refer to statements in prenex normal form with a matrix in negative normal form and higher-order quantifiers before first-order quantifiers as being in game form.
In all cases, I will assume that I have a first-order vocabulary with function symbols, relation symbols, and constant symbols. I will assume a domain with a single sort that cannot be empty.
Fact 1: Existential second-order logic (ESO) is compact.
Fact 2: Universal second-order logic (USO) is not compact.
Here's a proof of the non-compactness of USO. Consider the collection of statements $\{ \text{the domain does not have size exactly $n$} : n \in \mathbb{Z}_{> 0} \}$ and the game form statement corresponding to $\forall f : (\forall x \forall y \mathop. f(x) = f(y) \to x = y) \to (\forall y \exists! x \mathop. f(x) = y)$.
Every finite subset of this can be satisfied by picking a domain that is arbitrarily large. However, the last sentence asserts the Kuratowski-finiteness of the domain, and the other sentences preclude the domain from having any particular finite size. Thus, the set of sentences as a whole is contradictory.
This example works in the empty signature, so I'm curious:
Question 3:
What happens if we start dropping logical symbols from USO?
Attempt:
I think we can get a compact fragment, which I'll call USOC1 as follows.
Let's restrict our attention to USO sentences in game form containing only the logical symbols $\forall$ and $\land$. Note that this means that formulas containing $=$ are excluded. Let's restrict our vocabulary to contain only constants and relation symbols. Let's additionally restrict higher-order instances of $\forall$ to range over relation symbols only. This fragment is very restrictive. I chose it deliberately to make the proof of its compactness as simple as possible.
Given an arbitrary well-formed formulas $\forall \cdots \varphi$, I can hoist the $\land$'s above the quantifier and restrict attention to well-formed formulas of the form $\forall \cdots R(t_1, t_2, \cdots)$.
Every sentence in this fragment is satisfiable in the singleton model where very predicate is always true, so we need to consider arbitrary pairs consisting of a premise and a conclusion.
Let's think about $\Gamma \models_{\text{USOC1}} \varphi$. We want to show that there exists a finite subset $\Gamma_0 \subset \Gamma$ such that $\Gamma_0 \models_{\text{USOC1}} \varphi$.
For case 1, let's consider cases where $\varphi$ is of the form $R(c_1, c_2, \cdots)$. $\varphi$ follows from $\Gamma$ if and only if there exists a single well-formed formula in $\Gamma$ for which $\varphi$ is a substitution instance.
Case 2: Suppose the matrix of $\varphi$ is headed by a vocabulary predicate, but contains first-order universal quantifiers. Replace each free variable $x_i$ with a fresh constant symbol $c_i$ that does not appear in $\Gamma$. The problem is now reduced to an instance of case 1.
Case 3: Suppose $\varphi$ is headed by a second-order quantifier $\forall P \mathop. \alpha(P)$. Let $P'$ be a fresh predicate symbol. Replace the conclusion with $\alpha(P')$. The problem is now reduced to an instance of case 2.
Case 4: Suppose $\varphi$ contains the connective $\land$. $\varphi$ is still finite. We can rewrite it as $L_1 \land L_2 \land \cdots$ where each $L_i$ is $\land$-free. Each $L_i$ is an instance of case 3 and thus follows from a single premise. The set of these premises, which is again finite, implies $\varphi$.
This completes the proof of the compactness of USOC1.