There are two slightly different versions of compactness:
- If $\Delta$ is finitely satisfiable, then $\Delta$ is satisfiable.
- If $\Gamma \models \varphi$ then there exists a finite subset $\Gamma_0 \subset \Gamma$ such that $\Gamma_0 \models \varphi$.
I'm interested in the second one here because positive second-order logic does not have actual contradictions. For second-order logic though, these two notions line up.
Consider second-order logic with a single non-empty domain. We have function and relation symbols as vocabulary items. A constant is a nullary function.
Additionally, quantifiers can introduce functions and relations of arbitrary arity (e.g. $\exists f / 2$ or $\forall R / 3$). Suppose our connectives are $\land$, $\lor$ and $\lnot$.
Consider the fragment without $\lnot$. Let's call this positive second-order logic.
Positive second-order logic with Henkin semantics is definitely compact.
I'm wondering whether positive second-order logic with full semantics is compact.
Attempt:
One argument for showing that second-order logic with full semantics is not compact is to consider the following statements:
- for each $n \in \mathbb{N}$, the domain has at least $n$ entities.
- the domain is Kuratowski finite (every injection is a bijection).
These are finitely satisfiable but not satisfiable.
However, positive second-order logic is quite weak. It can express maximum bounds on the size of the domain, e.g.
$$ \forall x_1 \cdots x_n \mathop. \bigvee_{1 \le i < j \le n+1} x_i = x_j \;\; \text{is equivalent to} \;\; \exists_{\le n} \top $$
It cannot express minimum bounds however.
Additionally, neither Kuratowski finiteness nor Kuratowski-infiniteness can be expressed in positive second-order logic.
We can express that a function is bijective.
$$ \exists g \mathop. \forall x \mathop. x = g(f(x)) \; \text{where $f$ is a free variable} \\ \;\;\; \text{expresses that $f$ is a bijection} $$
I think we can express injectivity as well.
$$ \exists g \mathop. \forall x \mathop. f(x) = f(g(f(x))) \; \text{where $f$ is a free variable} \\ \;\;\; \text{expresses that $f$ is an injection} $$
But we can't form an implication as a single sentence because $\lnot$ and $\to$ are both prohibited.