0
$\begingroup$

My understanding is that Stephen Wolfram's concept of a multiway system begins with certain rules and then generates all possible combinations of those rules. There are many distinct mathematical structures that can be generated depending on the choice of initial rules: https://www.wolframphysics.org/universes/

For a long time I have been interested in the idea of computationally enumerating every possible expression of a formal theory. For example, if ZFC has 10 axioms, I assume you would, for example, start with the empty set, and consider which of the 10 axioms then implies the existence of another set. Then, you would consider which of the axioms can be applied, to the set you just generated. And so on.

I believe there are deep mathematical theories regarding limitations in enumerating all sets, which I intend to study.

For now, I would like to know if there is a multiway system which is structurally identical to taking the axioms of ZFC, written in formal logic, and applying every possible valid sequence of rules, to generate every possible expression (up to a specific number of iterations of the program that does this, since it would go on forever).

I do not know as much mathematics as I would like to, so if you think my question is not clear or does not make sense, please fill me in on what concepts I should study so I can ask a more specific question. This is my attempt to describing what I would like to know more about. Thanks.

Improve this question
$\endgroup$

2 Answers 2

Reset to default
4
$\begingroup$

Wolfram's multi-way systems are expressive enough to accommodate generation of any computably enumerable set. Thus they are powerful enough to generate all theorems of a computably enumerable formal systems, which all formal systems used in practice (ZFC, Peano arithmetic, type theory etc.) are.

While the idea of enumerating all theorems of a theory is alluring, enumerating all theorems is useless for the purposes of discovering new knowledge, due to combinatorial explosion: there are too many theorems of ZFC! What good is it to be able to generate millions of theorems per second, if we don't have some way of sorting out the relevant ones from the trash? And what does "relevant" mean, if not "popular" or "gives the author social status"?

Supplemental It may not be clear whether the question asks for an enumeration of derivable or valid judgements. A useful answer can be given about derivability, which I attempted to do above. Regarding enumeration of all valid judgements, that is well-known to be impossible in interesting cases due to Gödel's incompleteness phenomena, and that's that.

Improve this answer
$\endgroup$
3
  • $\begingroup$ I have struggled to express what I want to know because I have so many questions at the same time, but I now believe that reverse mathematics is what I have been looking for. I have wanted to know what are the least expressive systems we know of and proving what their capabilities and limitations are, and comparing them to each other in some encompassing general framework, if possible. I am going to study this now. $\endgroup$
    – Julius H.
    Nov 26 at 11:20
  • $\begingroup$ @hmltn You might enjoy this book. I found it to be written in a very readable style (it's aimed at non-specialist with a math undergrad level of knowledge), but it also still covers plenty of technical details. $\endgroup$
    – David Young
    Nov 26 at 18:31
  • $\begingroup$ @hmltn: It sounds like math.stackexchange.com is a better forum for your question. $\endgroup$
    – Andrej Bauer
    Nov 26 at 20:19
2
$\begingroup$

For a long time I have been interested in the idea of computationally enumerating every possible expression of a formal theory.

Who hasn't! :) As one with a background in linguistics, I am sure you will appreciate the distinction syntax/semantics, which is very relevant to mathematical and formal logic, too: formal statements and even, with some caution, their provability, is a syntactic/formal notion, while the truth of statements, i.e. theoremhood, is a semantic one, and not subordinate to provability.

Another distinction that is crucial is first-order vs higher-order theories: standard ZF(C) is a first-order theory, though already a very strong one relatively speaking, indeed first-order is the much weaker arithmetic system in Goedel's incompleteness theorem. And we are usually (mostly?) interested in first-order theories because these are the ones that can be effectively implemented say in a real computer: with higher-order we can only implement higher-order symbolic computation.

In particular, you may want to look at two fundamental results to begin with:

  • Goedel's incompleteness theorem: where Goedel constructs a statement of plain natural number arithmetic (PM is the underlying theory there), that is not provable from the axioms and rules of inference, despite at a meta-level we conclude the the statement must be true, whence it is indeed unprovable: notice in particular the distinction between a mathematical notion being expressible in the language/system (we can say it in that system) and the corresponding statement being provable in that system (we can derive it). https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_theorems#First_incompleteness_theorem

  • Tarski's undefinability theorem, about the undefinability of arithmetic truth in arithmetic itself, still about first-order theories in particular. https://en.wikipedia.org/wiki/Tarski%27s_undefinability_theorem

And I won't say much at all about semantics, that's an even tougher topic, except for mentioning two keywords here: proof theory, and model theory: https://en.wikipedia.org/wiki/Proof_theory https://en.wikipedia.org/wiki/Model_theory

That much for a very quick intro, now back to "enumerating every possible expression", at least two cautions there: 1) despite there is some sense to doing such an operation up to the notion of "cumulative hierarchy", incompleteness means you are never going to enumerate them all (more precisely: no effective procedure exists that can systematically enumerate all and only the valid formulas of any such system: which is incompleteness and, under another form, the halting problem); and, 2) you'd still be enumerating syntactic constructs only, namely, formulae: whether those correspond to "sets" or anything else is not per se a syntactic thing...

I am sure much more could be said and I am also sure I have botched some details, I am more of a symbolic/abstract/natural language logician (a la P.F. Strawson, see Introduction to Logical Theory, a wonderful book and intro to the subject IMO) than any expert in mathematical or even formal logic: so I am myself more of a student here, sharing notes and hoping some teacher might jump on this and correct us both. :)

Improve this answer
$\endgroup$
11
  • 1
    $\begingroup$ In what sense did you address the question asked, namely if there is a Wolfram multiway ssytem that enumerates the theorems of ZFC? $\endgroup$
    – Andrej Bauer
    Nov 20 at 12:24
  • $\begingroup$ I am too new to comment on your answer, but "enumerating all theorems" is impossible, not just "useless", so your answer is rather wrong (sure, model theory: not enough space here...). That said, I have not even mentioned Wolfram because indeed I find that effort essentially misguided, but the questioner here is a beginner, so I didn't think appropriate reading and answering his question to the letter, or saying "forget about Wolfram", I have rather tried to give basic coordinates: but I think you do have a point, I should have been more explicit. $\endgroup$
    – Julio Di Egidio
    Nov 20 at 12:43
  • $\begingroup$ I agree the question is a bit misguided, and in that sense your answer is useful. But of course, your interpretation of "enumerating all theorems" has to be dishonest for you to claim that it is actually false. (Nowhere did I suggest that anybody can actually enumerate infinitely many things in finite time.) It is relatively easy to write a program which enumerates the theorems of a given c.e. formal system. $\endgroup$
    – Andrej Bauer
    Nov 20 at 14:21
  • 1
    $\begingroup$ The distinction between first-order and higher-order is not crucial. The derivable judgements of any computably enumerable formal system are computably enumerable. All formal systems seen in practice, whether they be first-order or higher-order, satisfy this condition. $\endgroup$
    – Andrej Bauer
    Nov 20 at 14:23
  • 1
    $\begingroup$ Ah, I see, you think we're trying to enumerate the semantically valid statements. I would argue that the OP's second paragraph indicatates they are looking for the the enumeration of provable statements (start with axioms and apply all rules in all possible ways, which is also in accordance with how Wolfram multiway systems work.) $\endgroup$
    – Andrej Bauer
    Nov 20 at 14:26

Your Answer

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

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