Is the positive fragment of second-order logic will full semantics compact

logicmodel-theorysecond-order-logicsolution-verification

There are two slightly different versions of compactness:

  1. If $\Delta$ is finitely satisfiable, then $\Delta$ is satisfiable.
  2. 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:

  1. for each $n \in \mathbb{N}$, the domain has at least $n$ entities.
  2. 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:

  • the sentence $\forall x\forall y (x=y\vee x\# y)$ and,
  • for each $n\geq 2,$ the sentence $\exists x_1 \dots \exists x_n \bigwedge_{1\leq i<j\leq n} (x_i\#x_j)$ - call this $G_n$

Take $\varphi=\varphi_1\vee\varphi_2$ where:

  • $\varphi_1=\exists x\exists y (x=y\wedge x\#y)$
  • $\varphi_2=\exists f(f\text{ is injective}\,\wedge\, \exists x\forall y. f(y)\# x).$

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.$

Related Question