<p>By slightly modifying Grandjean's algorithm (reference in Emil's answer), one can show that for any fixed <span class="math-container">$k\geq 1$</span> and for a fixed finite (relational) language <span class="math-container">$L$</span>, the problem of determining the asymptotic probability of a given sentence of <span class="math-container">$FO^k$</span>, which contains relation symbols only from <span class="math-container">$L$</span>, is in PTime.</p>
<p>Here is a rough sketch. Consider the algorithm <span class="math-container">$TRUTH(\Delta,\varphi)$</span> 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 <span class="math-container">$L$</span> and the number of variables that can occur in formulas is finite, the size of a complete description <span class="math-container">$\Delta$</span> 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 <span class="math-container">$\varphi$</span> that we are looking at; this requires space <span class="math-container">$\log(|\varphi|)$</span>. 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).</p>

CC BY-SA 4.0
2022-03-29T12:19:36.857Z
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$)?
Emil Jeřábek
CC BY-SA 4.0
2022-03-29T12:33:44.157Z
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$).
Reijo Jaakkola
CC BY-SA 4.0
2022-03-29T12:46:45.297Z
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.
Emil Jeřábek
CC BY-SA 4.0
2022-03-29T12:56:50.467Z
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).
Reijo Jaakkola
CC BY-SA 4.0
2022-03-29T13:11:59.993Z
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.
Emil Jeřábek
CC BY-SA 4.0
2022-03-29T10:17:09.313Z
2022-03-29T10:40:50.947Z
2022-03-29T10:40:50.947Z
Reijo Jaakkola
<p>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 <span class="math-container">$L$</span> has asymptotic probability <span class="math-container">$1$</span> if and only if it is provable in the complete theory of the random <span class="math-container">$L$</span>-structure, axiomatized by the extension axioms
<span class="math-container">$$\forall\vec x\:\bigl(\theta(\vec x)\to\exists y\:\theta^*(\vec x,y)\bigr),$$</span>
where <span class="math-container">$\theta$</span> is (the conjunction of) any complete diagram of a tuple <span class="math-container">$\vec x$</span>, and <span class="math-container">$\theta^*$</span> is an extension of <span class="math-container">$\theta$</span> to a complete diagram on <span class="math-container">$\vec x,y$</span>.</p>
<p>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 <span class="math-container">$\ge2$</span> objects): it is PSPACE-complete, due to Grandjean [1]. Thus, the asymptotic probability of FO sentences is also PSPACE-complete to decide.</p>
<p><strong>Reference:</strong></p>
<p>[1] Étienne Grandjean: <em>Complexity of the first-order theory of almost all finite structures</em>, Information and Control 57 (1983), no. 2–3, pp. 180–204, doi <a href="https://doi.org/10.1016/S0019-9958(83)80043-6" rel="nofollow noreferrer">10.1016/S0019-9958(83)80043-6</a>.</p>

CC BY-SA 4.0
2022-03-29T09:18:52.790Z
2022-03-29T12:26:27.800Z
2022-03-29T12:26:27.800Z
Emil Jeřábek
<p>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.</p>
<p>For further reading, I recommend lectures notes by Graedel [1] and the famous FMT book by Libkin [2].</p>
<p>[1] <a href="https://logic.rwth-aachen.de/files/AMT-WS19/chapter5.pdf" rel="nofollow noreferrer">https://logic.rwth-aachen.de/files/AMT-WS19/chapter5.pdf</a></p>
<p>[2] <a href="https://homepages.inf.ed.ac.uk/libkin/fmt/fmt.pdf" rel="nofollow noreferrer">https://homepages.inf.ed.ac.uk/libkin/fmt/fmt.pdf</a></p>

CC BY-SA 4.0
2022-03-29T09:55:54.943Z
What does the chance depend on?
Emil Jeřábek
CC BY-SA 4.0
2022-03-29T10:10:39.697Z
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.
Bartosz Bednarczyk
CC BY-SA 4.0
2022-03-29T09:45:32.733Z
2022-03-29T15:48:39.770Z
2022-03-29T15:48:39.770Z
Bartosz Bednarczyk
<p><a href="http://math.uchicago.edu/%7Emay/REU2018/REUPapers/Abraham.pdf" rel="nofollow noreferrer">0-1 Laws in first order logic</a> state that the probability of a FOL sentence <span class="math-container">$\Phi$</span>, defined as follows:
<span class="math-container">$$P(\Phi) = \frac{|\{\omega \in \Omega^{n}:\omega \models \Phi\}|}{|\Omega^{n}|} $$</span>
where <span class="math-container">$\Omega^{n}$</span> is the set of all models on a domain of size <span class="math-container">$n$</span>, either goes to <span class="math-container">$0$</span> or <span class="math-container">$1$</span> as <span class="math-container">$n \rightarrow \infty$</span>.</p>
<p>My questions:</p>
<ul>
<li>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.</li>
<li>Does undecidability of FO mean that assymptotic probabilities are also undecidable in general ?</li>
<li>Are there fragments where this can be done ?</li>
<li>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.</li>
</ul>
<p>The reason I am curious about the two variable fragment is that with a single predicates, it seems to be easy for example: <span class="math-container">$\forall xy. Rxy$</span>  clearly has an assymptotic probability 0, I guess so does <span class="math-container">$\forall x \exists y Rxy$</span>. But <span class="math-container">$\exists x \exists y Rxy$</span> has an asymptotic probability 1.</p>

<graph-theory><pr.probability><first-order-logic>
Evaluating asymptotic probabilities of First Order Logic Formulas?
SagarM
# Evaluating asymptotic probabilities of First Order Logic Formulas?

(Asked by: username_0 on 2022-03-29)

[0-1 Laws in first order logic](http://math.uchicago.edu/%7Emay/REU2018/REUPapers/Abraham.pdf) 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.

**Tags:** graph-theory, pr.probability, first-order-logic


---

## 3 answers

### Answer by username_1 on 2022-03-29. Score: 5

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

> **Comments:**
> **username_2**: 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$)?  
> **username_1**: 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$).  
> **username_2**: 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.  
> **username_1**: 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).  
> **username_2**: 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.  

---

### Answer by username_2 on 2022-03-29. Score: 4

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](https://doi.org/10.1016/S0019-9958(83)80043-6).


---

### Answer by username_3 on 2022-03-29. Score: 3

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>

> **Comments:**
> **username_2**: What does the chance depend on?  
> **username_3**: 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.  

---

