<p>One line of reasoning here is that of Levin Search. <a href="https://people.idsia.ch/%7Ejuergen/optimalsearch.html" rel="nofollow noreferrer">https://people.idsia.ch/~juergen/optimalsearch.html</a> The protocol is to try every program in order, and return the first one which “works.”</p>
<p>If you don’t decide in advance on some maximum program number to try, then what happens? You keep counting forever in the event there is no working program for your problem.</p>
<p>Furthermore, if you don’t set a time limit for each program, then what happens? You inevitably wind up with a program stuck in an infinite loop.</p>
<p>The argument is that you can’t know that a bigger number would permit a solution. You might be digging for gold and give up just a bit too early, and if you need to prove a negative, then you need to count to infinity and check an infinite number of programs, which, barring some (quantum and / or thermodynamic) voodoo unknown to humans, is impossible.</p>
<p>Ok, but nobody’s perfect, including Gödel, so what’s the problem?</p>
<p>One problem is, you can absolutely decide to set a maximum program number and a maximum program timeout like Ray recommended <a href="https://youtu.be/CfjkqpzDkCs?si=0D1kdQR_-DMKKlcx" rel="nofollow noreferrer">https://youtu.be/CfjkqpzDkCs?si=0D1kdQR_-DMKKlcx</a> and prove within these bounds that the formula evaluates true or false. That approach sidesteps the “you can’t prove a negative” issue with a hefty dose of reality and experiment.</p>
<p>Second problem, and this might only apply to treelike formulas, but I reckon it’s graphical too, anyway, all complex formulas are, by definition, formed of simpler subtrees. You could enumerate all subtree tree-words up to inclusion of every primitive and terminal, or perhaps one layer beyond, and if those are all falsy, then you know you’ll never magically flip it around. Can I prove that? Well, I just thought of it, so no. But I reckon the recursive property of first order logic could yield some interesting arguments about decidability.</p>
<p>For a concrete example, the function</p>
<p>e=mc2 in Polish notation could be simply
<em>m</em>cc
And you if you’re counting functions in order then it’s a truism you would reach every smaller function before a longer one, so you would consider *cc first, i.e. these FOL formulas are always constructed from the bottom up and it would seem difficult to ever prove a formula without the necessary “mise-en-place” so you could potentially prove a negative by proving it on a limited (but within that limit, complete) enumeration of the formulas you can access. It is possible that doing this could enable us to make statements about the infinite series of function if the smaller ones fail to provide necessary capabilities then nesting them won’t change their behavior.</p>
<p>After all, you couldn’t build a house of cards multiple levels high without first building one single level of the structure. It’s possible for these and other subtle or obvious arguments to profoundly impact our understanding of supposedly “decided” issues in theoretical CS, such as decidability/undecidability of various systems.</p>

CC BY-SA 4.0
2024-04-11T11:37:05.097Z
Your answer could be improved with additional supporting information. Please [edit] to add further details, such as citations or documentation, so that others can confirm that your answer is correct. You can find more information on how to write good answers [in the help center](/help/how-to-answer).
Community
CC BY-SA 4.0
2024-04-05T23:53:00.980Z
2024-04-17T11:46:16.297Z
2024-04-17T11:46:16.297Z
Bion Alex Howard
<p>&quot;Decidable&quot; means &quot;both semi-decidable and co-semi-decidable&quot;, so &quot;Undecidable&quot; just means &quot;not both semi-decidable and co-semi-decidable&quot;. If a problem is semi-decidable but not co-semi-decidable, it is said to be undecidable. Since it is possible to recursively enumerate all the true theorems of FOL, but there is no procedure to that decides in finite time for any given formula whether it is <em>not</em> true, the theory is not decidable.</p>

CC BY-SA 4.0
2024-04-05T23:22:19.477Z
2024-04-05T23:22:19.477Z
Natalie Clarius
<p>I am very new to this. I am trying to understand some basics about what kinds of enumerations in FOL are possible, and which are not.</p>
<p>If you accept that FOL is defined in terms of a finite number of symbols (alphabet), and that any string of FOL must be finite in length, you can argue that the number of possible strings of FOL is countably infinite. I would say this is because regardless of the size of the alphabet, <em>n</em>, the number of possible strings of length <em>k</em> will have an explicit, computable formula (ie, some combinatorial expression). So, there is a bijection between natural numbers and sets of expressions of FOL; so it is countable.</p>
<p>The set of well-formed expressions is a subset of the set of all expressions, so it would follow that the set of wff is countable.</p>
<p>I have not yet thought enough about how you would attempt to enumerate theorems (= true formula) of FOL, but according to <a href="https://en.m.wikipedia.org/wiki/First-order_logic" rel="nofollow noreferrer">this</a>, FOL is “semi-decidable”:</p>
<blockquote>
<p>Gödel's completeness theorem, proved by Kurt Gödel in 1929,
establishes that there are sound, complete, effective deductive
systems for first-order logic, and thus the first-order logical
consequence relation is captured by finite provability. Naively, the
statement that a formula φ logically implies a formula ψ depends on
every model of φ; these models will in general be of arbitrarily large
cardinality, and so logical consequence cannot be effectively verified
by checking every model. However, it is possible to enumerate all
finite derivations and search for a derivation of ψ from φ. If ψ is
logically implied by φ, such a derivation will eventually be found.
Thus first-order logical consequence is semidecidable: it is possible
to make an effective enumeration of all pairs of sentences (φ,ψ) such
that ψ is a logical consequence of φ.</p>
</blockquote>
<p>I am looking for some supportive clarification and explanation, while I try to study this. Why does FOL become undecidable, when you try to constrain an enumeration from “well formed formula” to “true, well-formed formula”?</p>

CC BY-SA 4.0
2024-04-06T13:54:21.183Z
not all subsets of a computable set are computable. all formulas are, provable formulas are not. FOL means its provable formulas.
Kaveh
CC BY-SA 4.0
2024-04-06T19:40:13.677Z
This question is not research-level and therefore not suitable for this forum. Please ask such questions at https://math.stackexchange.com or https://cs.stackexchange.com.
Andrej Bauer
<decidability><first-order-logic><enumeration>
Help understand why FOL wff are enumerable, but FOL is undecidable
Julius Hamilton
# Help understand why FOL wff are enumerable, but FOL is undecidable

(Asked by: username_0 on 2024-04-05)

I am very new to this. I am trying to understand some basics about what kinds of enumerations in FOL are possible, and which are not.

If you accept that FOL is defined in terms of a finite number of symbols (alphabet), and that any string of FOL must be finite in length, you can argue that the number of possible strings of FOL is countably infinite. I would say this is because regardless of the size of the alphabet, *n*, the number of possible strings of length *k* will have an explicit, computable formula (ie, some combinatorial expression). So, there is a bijection between natural numbers and sets of expressions of FOL; so it is countable.

The set of well-formed expressions is a subset of the set of all expressions, so it would follow that the set of wff is countable.

I have not yet thought enough about how you would attempt to enumerate theorems (= true formula) of FOL, but according to [this](https://en.m.wikipedia.org/wiki/First-order_logic), FOL is “semi-decidable”:

> Gödel's completeness theorem, proved by Kurt Gödel in 1929,
> establishes that there are sound, complete, effective deductive
> systems for first-order logic, and thus the first-order logical
> consequence relation is captured by finite provability. Naively, the
> statement that a formula φ logically implies a formula ψ depends on
> every model of φ; these models will in general be of arbitrarily large
> cardinality, and so logical consequence cannot be effectively verified
> by checking every model. However, it is possible to enumerate all
> finite derivations and search for a derivation of ψ from φ. If ψ is
> logically implied by φ, such a derivation will eventually be found.
> Thus first-order logical consequence is semidecidable: it is possible
> to make an effective enumeration of all pairs of sentences (φ,ψ) such
> that ψ is a logical consequence of φ.

I am looking for some supportive clarification and explanation, while I try to study this. Why does FOL become undecidable, when you try to constrain an enumeration from “well formed formula” to “true, well-formed formula”?

**Tags:** decidability, first-order-logic, enumeration
> **Comments:**
> **username_1**: not all subsets of a computable set are computable. all formulas are, provable formulas are not. FOL means its provable formulas.  
> **username_2**: This question is not research-level and therefore not suitable for this forum. Please ask such questions at https://math.stackexchange.com or https://cs.stackexchange.com.  

---

## 2 answers

### Answer by username_3 on 2024-04-05. Score: 1

One line of reasoning here is that of Levin Search. [https://people.idsia.ch/~juergen/optimalsearch.html](https://people.idsia.ch/%7Ejuergen/optimalsearch.html) The protocol is to try every program in order, and return the first one which “works.”

If you don’t decide in advance on some maximum program number to try, then what happens? You keep counting forever in the event there is no working program for your problem.

Furthermore, if you don’t set a time limit for each program, then what happens? You inevitably wind up with a program stuck in an infinite loop.

The argument is that you can’t know that a bigger number would permit a solution. You might be digging for gold and give up just a bit too early, and if you need to prove a negative, then you need to count to infinity and check an infinite number of programs, which, barring some (quantum and / or thermodynamic) voodoo unknown to humans, is impossible.

Ok, but nobody’s perfect, including Gödel, so what’s the problem?

One problem is, you can absolutely decide to set a maximum program number and a maximum program timeout like Ray recommended <https://youtu.be/CfjkqpzDkCs?si=0D1kdQR_-DMKKlcx> and prove within these bounds that the formula evaluates true or false. That approach sidesteps the “you can’t prove a negative” issue with a hefty dose of reality and experiment.

Second problem, and this might only apply to treelike formulas, but I reckon it’s graphical too, anyway, all complex formulas are, by definition, formed of simpler subtrees. You could enumerate all subtree tree-words up to inclusion of every primitive and terminal, or perhaps one layer beyond, and if those are all falsy, then you know you’ll never magically flip it around. Can I prove that? Well, I just thought of it, so no. But I reckon the recursive property of first order logic could yield some interesting arguments about decidability.

For a concrete example, the function

e=mc2 in Polish notation could be simply
*m*cc
And you if you’re counting functions in order then it’s a truism you would reach every smaller function before a longer one, so you would consider \*cc first, i.e. these FOL formulas are always constructed from the bottom up and it would seem difficult to ever prove a formula without the necessary “mise-en-place” so you could potentially prove a negative by proving it on a limited (but within that limit, complete) enumeration of the formulas you can access. It is possible that doing this could enable us to make statements about the infinite series of function if the smaller ones fail to provide necessary capabilities then nesting them won’t change their behavior.

After all, you couldn’t build a house of cards multiple levels high without first building one single level of the structure. It’s possible for these and other subtle or obvious arguments to profoundly impact our understanding of supposedly “decided” issues in theoretical CS, such as decidability/undecidability of various systems.

> **Comments:**
> **username_4**: Your answer could be improved with additional supporting information. Please [edit] to add further details, such as citations or documentation, so that others can confirm that your answer is correct. You can find more information on how to write good answers [in the help center](/help/how-to-answer).  

---

### Answer by username_5 on 2024-04-05. Score: 0

"Decidable" means "both semi-decidable and co-semi-decidable", so "Undecidable" just means "not both semi-decidable and co-semi-decidable". If a problem is semi-decidable but not co-semi-decidable, it is said to be undecidable. Since it is possible to recursively enumerate all the true theorems of FOL, but there is no procedure to that decides in finite time for any given formula whether it is *not* true, the theory is not decidable.


---

