2
$\begingroup$

With some formal systems, it's possible to enumerate all the theorems.

This is the case for instance in propositional calculus or in some first-order theories with a recursively enumerable set of axioms (e.g. group theory, field theory, Peano arithmetic, etc.).

I'm looking for a software that would implement such an enumeration. Or more basically, a software that would produce random theorems (which may or may not be of interest). A software doing that in any of the formal systems listed previously would be acceptable.

$\endgroup$
3
  • 1
    $\begingroup$ You will have to be patient since most of the generated strings will not be a theorem. So, I guess that those "random theorems" are quite boring , but it could be funny. $\endgroup$
    – Peter
    Dec 2, 2023 at 18:47
  • $\begingroup$ Related. $\endgroup$
    – Kurt G.
    Dec 2, 2023 at 19:44
  • $\begingroup$ Not enumerating theorems (or proofs) as you describe. But if you just want some software that produces something you may want to look into "Whole-Proof Generation and Repair with Large Language Models". $\endgroup$
    – AHusain
    Dec 2, 2023 at 20:27

1 Answer 1

4
$\begingroup$

I highly doubt you ever get any interesting theorem, even if you were to run such software for the remainder of your lifetime!

Let's take something like Peano Arithmetic (PA). How do we enumerate its theorems? Well, one obvious way is to systematically crank out strings of symbols, where the symbols are not just the symbols from the language of PA ($0$, $s$, $+$, and $\cdot$), but also those of FOL ... and while there are only finitely many logical operators (and only one open parenthesis and one close parenthesis), we'll need to deal with enumerably many variables. Any reasonable method of that cranks out all possible such strings will be such that the vast majority of strings are not FOL formulas but instead junk strings like $x_1 \to \forall ) + \forall s \to 0 ( 0 =$. Moreover, out of all the strings that actually are formulas, the vast majority will not be theorems, e.g. $s(0)=0$. And, even if you do get something that is a theorem, it is most likely uninteresting, e.g. $0+0=0$.

Even worse, while such an enumeration method will, for any theorem of PA, at some point produce that theorem (even if it is gazillion years from now), it may not be immediately clear to you that any such theorem is a theorem ... certainly if that theorem is an 'interesting' theorem.

So, instead of cranking out (what we hope will be) FOL formulas, what we really need to do is crank out proofs: proofs that have one or more of the Axioms of PA as its premises, and that has the theorem as its conclusion. So, you'll need to have strings that represent proofs ... avoiding proofs that have complicated subproof structures, you could use some Hilbert system ... i.e. you could crank out expressions that (hopefully!) embody sequences of sentences....all you'd need is to add a sentence separator symbol (e.g. $/$) ... a verification algorithm that determines whether every sentence in that sequence of statements is indeed an application of any of the axioms, or is the result of applying Modus Ponens to any two earlier sentences is written easily enough. Still, even with such simplifications, it should be clear that now the VAST majority of what such an enumeration method will out put is junk, and that even in the once in a blue moon case that it produces is an actual sequences of actual FOL formulas, the VAST majority of those does not constitute a proof, and even of those that do constitute a proof, the number of cases where it is a proof of something that is actually non-trivial will be extremely, extremely small.

$\endgroup$
3
  • 2
    $\begingroup$ It seems to me that a systematic generator of propositional calculus proofs would start generating “interesting” theorems in pretty short order, by the admittedly low standards of propositional calculus. The proofs of formulas like $(A\to(B\to C))\to(A\to B)\to(A\to C)$ and $(A\to B\to C)\to (B\to A\to C)$ are pretty short. $\endgroup$
    – MJD
    Dec 2, 2023 at 20:24
  • 2
    $\begingroup$ I don't think you'd want to use a Hilbert system. Probably better is to generate a well-typed expression in some simple expression language, and then compute its type. In a suitable system, the type of any expression is a provable theorem of logic, and the expression itself encodes the proof. Maybe I should stop posting comments and write a real answer. $\endgroup$
    – MJD
    Dec 2, 2023 at 20:27
  • $\begingroup$ @MJD That goes above my head, so yes, I encourage you to write something along those lines as an Answer: I'd be interested in reading that! $\endgroup$
    – Bram28
    Dec 2, 2023 at 21:41

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .