Is there a property definable in finite-variable infinitary logic $L^{\omega}_{\omega\infty}$ but not definable in partial fixed point logic FO(PFP) ?
$\begingroup$
$\endgroup$
1
-
2$\begingroup$ Are you interested only in finite models? And do you mean $L_{\infty,\omega}$ rather than $L_{\omega,\infty}$? $\endgroup$– Joel David HamkinsApr 13, 2014 at 15:33
Add a comment
|
1 Answer
$\begingroup$
$\endgroup$
4
Following Noah S's idea (now deleted, I guess because it uses infinitely many variables?), consider the language with infinitely many constants $c_n$ and the finite models in this language. For each set $X\subset\mathbb{N}$, we may consider the collection of finite models $M$ for which $\{n\mid c_n=c_0\}=X$. This property is expressible by a sentence in $L_{\omega_1,\omega}$ logic, using no variables or quantifiers at all. $$\left(\bigwedge_{n\in X} c_n=c_0\right)\wedge\left(\bigwedge_{n\notin X}c_n\neq c_0\right)$$ So this property is definable in $L_{\omega_1\omega}$ logic for any $X\subset\mathbb{N}$. Since there are only countably many finitary formulas, there must be an $X$ for which the property is not definable in PFP logic.
answered Apr 14, 2014 at 12:39
-
$\begingroup$ We could also insist that the models have only two elements, and so what we really have is a partition of the natural numbers into at most two pieces, depending on how the constants are interpreted. $\endgroup$ Apr 14, 2014 at 13:09
-
$\begingroup$ If one objects that the language here is infinite, then we may use instead the language with one constant $0$ and a successor operation $S$, defining the class of finite models $M$ for which the least $n$ for which $S^n(0)=0$ is in $X$. $\endgroup$ Apr 14, 2014 at 13:23
-
$\begingroup$ Yeah, I deleted it because it used infinitely many variables and I didn't see a way to fix it. This is very nice! $\endgroup$ Apr 14, 2014 at 17:38
-
$\begingroup$ @NoahS, the advantage of your method, even though it uses infinitely many variables, is that it works in any language (assuming $=$ is available), whereas I needed something special about the language. $\endgroup$ Apr 14, 2014 at 17:43