3
$\begingroup$

0-1 Laws in first order logic state that the probability of a FOL sentence $\Phi$, defined as follows: $$P(\Phi) = \frac{|\{\omega \in \Omega^{n}:\omega \models \Phi\}|}{|\Omega^{n}|} $$ where $\Omega^{n}$ is the set of all models on a domain of size $n$, either goes to $0$ or $1$ as $n \rightarrow \infty$.

My questions:

  • Is are there fragments of logic where we can compute the asymptotic probability algorithmically ? Any such algorithm is not obvious to me from the linked notes.
  • Does undecidability of FO mean that assymptotic probabilities are also undecidable in general ?
  • Are there fragments where this can be done ?
  • I am specially curious about FO2 (function free FOL with only two variables), C2(function free FOL with only two variables and counting quantifiers) etc.

The reason I am curious about the two variable fragment is that with a single predicates, it seems to be easy for example: $\forall xy. Rxy$ clearly has an assymptotic probability 0, I guess so does $\forall x \exists y Rxy$. But $\exists x \exists y Rxy$ has an asymptotic probability 1.

Improve this question
$\endgroup$

3 Answers 3

Reset to default
5
$\begingroup$

By slightly modifying Grandjean's algorithm (reference in Emil's answer), one can show that for any fixed $k\geq 1$ and for a fixed finite (relational) language $L$, the problem of determining the asymptotic probability of a given sentence of $FO^k$, which contains relation symbols only from $L$, is in PTime.

Here is a rough sketch. Consider the algorithm $TRUTH(\Delta,\varphi)$ presentend in Grandjean's paper. This algorithm describes an alternating procedure and we want to show that it can be implemented in such a way that it uses only logarithmic amount of space (since ALogSpace = PTime). First, since the size of $L$ and the number of variables that can occur in formulas is finite, the size of a complete description $\Delta$ is also finite, so we can store it without any problems. Secondly, we will also need a binary pointer which tells us what is the current subformula of $\varphi$ that we are looking at; this requires space $\log(|\varphi|)$. This latter point is also where the present description starts to deviate from the description that Grandjean gives, since he apparently wants to store the whole subformula (which is clearly not necessary, but in the case that he considers it does not affect the complexity).

Improve this answer
$\endgroup$
5
  • $\begingroup$ Actually, since there are only finitely many possibilities for $\Delta$, hence only finitely many inequivalent formulas, shouldn’t Buss’s formula evaluation algorithm put it in ALOGTIME (i.e., uniform $\mathrm{NC}^1$)? $\endgroup$
    – Emil Jeřábek
    Commented Mar 29, 2022 at 12:19
  • $\begingroup$ There is no upper bound on the quantifier-depth of the sentence $\varphi$, so there are infinitely many inequivalent formulas (for example, for every $n\geq 1$ we have a formula of $FO^2$ over the vocabulary $\{E\}$, where $E$ is binary relation, expressing that there is an $E$-path of length $\geq n$). $\endgroup$
    – Reijo Jaakkola
    Commented Mar 29, 2022 at 12:33
  • $\begingroup$ The number of inequivalent FOk formulas (over the theory of the random structure) is at most exponential in the number of possible $k$-element structures $\Delta$ in the given language. (In other words, the theory has quantifier elimination, hence you only need to count the quantifier-free formulas.) Your example formulas are all equivalent, since there always is an $E$-path of length $\ge n$ between any pair of points. $\endgroup$
    – Emil Jeřábek
    Commented Mar 29, 2022 at 12:46
  • $\begingroup$ Ah, that is indeed true. Could you fill in the missing details for your ALOGTIME-claim (I'm not that familiar with Buss's algorithm). $\endgroup$
    – Reijo Jaakkola
    Commented Mar 29, 2022 at 12:56
  • $\begingroup$ Let me put it this way. Buss’s algorithm allows to evaluate terms over any fixed finite algebra $A$ in a finite signature. Here, we take for $A$ an enumeration of all inequivalent formulas in variables $\{x_1,\dots,x_k\}$, with operations corresponding to the Boolean connectives, and to the $k$ quantifiers $\exists x_1$, ..., $\exists x_k$ (as unary operations). Then, an $FO^k$ formula represents a term over $A$, and evaluation of the formula by the algorithm computes a canonical representant of the formula up to equivalence. In particular, for a sentence, it determines if it’s true or false. $\endgroup$
    – Emil Jeřábek
    Commented Mar 29, 2022 at 13:11
4
$\begingroup$

I assume you are talking about purely relational sentences, as otherwise the 0–1 law does not hold. As should be explained somewhere in those notes, an FO sentence in a finite relational language $L$ has asymptotic probability $1$ if and only if it is provable in the complete theory of the random $L$-structure, axiomatized by the extension axioms $$\forall\vec x\:\bigl(\theta(\vec x)\to\exists y\:\theta^*(\vec x,y)\bigr),$$ where $\theta$ is (the conjunction of) any complete diagram of a tuple $\vec x$, and $\theta^*$ is an extension of $\theta$ to a complete diagram on $\vec x,y$.

This theory is not only decidable—which is an immediate consequence of its being complete and recursively axiomatized—it has the lowest possible computational complexity (for an FO theory consistent with the existence of $\ge2$ objects): it is PSPACE-complete, due to Grandjean [1]. Thus, the asymptotic probability of FO sentences is also PSPACE-complete to decide.

Reference:

[1] Étienne Grandjean: Complexity of the first-order theory of almost all finite structures, Information and Control 57 (1983), no. 2–3, pp. 180–204, doi 10.1016/S0019-9958(83)80043-6.

Improve this answer
$\endgroup$
3
$\begingroup$

As stated, the problem can be reduced to the query evaluation problem over the Rado graph (or the corresponding structure for non-binary vocabularies). Hence, there is a huge chance that the problem is actually in PTime for FO2/C2 (since the usual model-checking problem for FO2/C2 is PTime-complete). See Reijo's reply.

For further reading, I recommend lectures notes by Graedel [1] and the famous FMT book by Libkin [2].

[1] https://logic.rwth-aachen.de/files/AMT-WS19/chapter5.pdf

[2] https://homepages.inf.ed.ac.uk/libkin/fmt/fmt.pdf

Improve this answer
$\endgroup$
2
  • $\begingroup$ What does the chance depend on? $\endgroup$
    – Emil Jeřábek
    Commented Mar 29, 2022 at 9:55
  • $\begingroup$ The usual model checking problem for FO2/C2 is PTime-complete. But here we do model-checking over infinite structure and is implicitly represented, so I can't tell for sure whether it works. My guess is that it should work, but it's just a guess. $\endgroup$
    – Bartosz Bednarczyk
    Commented Mar 29, 2022 at 10:10

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.