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.
Best Answer
Compactness does not hold for positive second-order logic with full semantics. Take the language with a single binary relation $\#$ as well as equality $=.$ Take $\Gamma$ to consist of:
Take $\varphi=\varphi_1\vee\varphi_2$ where:
Any model $M$ of $\Gamma\cup\{\neg \varphi_1\}$ satisfies ${\#}^M=(\neq)^M$ by which I mean that $\#$ is interpreted as the inequality relation $\{(x,y):x\neq y\}.$ So $M$ is infinite, and it satisfies $\varphi_2$ by taking $f$ to be any injective non-surjective function. Therefore $\Gamma\models\varphi.$
Consider a finite subset $\Gamma_0$ of $\Gamma,$ and set $n=\max\{k:G_k\in\Gamma_0\}.$ Define $M_n$ to be the structure with domain of order $n,$ with ${\#}^{M_n}=({\neq})^{M_n}.$ Then $M_n$ is a model of $\Gamma_0\cup\{\neg\varphi\}$ so $\Gamma_0\not\models \varphi.$