Let us fix some mathematical theory T=T(0), such as ZFC. The aim is to develop algorithm A, which takes any statement S independent of T(0) as an input, and outputs axiom a(S) such that T(1)=T(0)+a(S) is consistent if T(0) is consistent, and either S or negation of S can be proved in T(1). Then algorithm can take another statement S' independent of T(1), and proceed iteratively, forming infinite sequence of theories, such that theory T(n) decides the first n statements given as inputs.

One simple example of A is a randomised algorithm such that a(S) is either S or negation of S with probabilities 0.5.

My question is whether there exists a version of algorithm A witch is (a) deterministic, and (b) the way how it decides every statement S does not depend on the order in which statements are arriving.

An example how the answer may be positive is a restricted setting when T(0)=ZFC, and all statements S are in the form "This particular Diophantine equation has a solution". Then the algorithm always returning a(S)="negation of S" does the job.

A positive answer to this question in general would imply a way to decide all provably independent statements in set theory one way or another in a consistent way.


closed as off-topic by Emil Jeřábek, Pace Nielsen, Jan-Christoph Schlage-Puchta, Joseph Van Name, Ben McKay Apr 7 at 13:06

This question appears to be off-topic. The users who voted to close gave this specific reason:

  • "MathOverflow is for mathematicians to ask each other questions about their research. See Math.StackExchange to ask general questions in mathematics." – Emil Jeřábek, Pace Nielsen, Ben McKay
If this question can be reworded to fit the rules in the help center, please edit the question.

  • 9
    $\begingroup$ The sets of theorems and antitheorems of ZFC are recursively inseparable: there is no deterministic algorithm that always terminates, returns "yes" on theorems (=provable statements of ZFC) and "no" antitheorems (=refutable statements, i.e., negations of theorems), even if you put no constraint whatsoever on what it is allowed to answer for all other statements. This probably dooms your attempts, even though I'm not sure I quite understood what you were trying to do. $\endgroup$ – Gro-Tsen Apr 3 at 10:36
  • 6
    $\begingroup$ You are in effect trying to build a decidable complete extension of ZFC. This can never work, as it contradicts Gödel’s theorem. $\endgroup$ – Emil Jeřábek Apr 3 at 12:17
  • 1
    $\begingroup$ Just to add to Gro-Tsen and Emil's comments, a priori it might be possible to compute a completion of PA or ZFC from a random oracle, but it turns out that for any given algorithm the probability that a random oracle computes a consistent complete extensions of PA or ZFC is 0. This is a strict generalization of the Gödel-Rosser theorem. $\endgroup$ – James Hanson Apr 3 at 15:08
  • 1
    $\begingroup$ Interestingly though there is something slightly non-trivial to be gained from random information in an axiomatic system. For every $\varepsilon > 0$ there is a randomly generated extension of PA (or ZFC) that is arithmetically sound with probability $1-\varepsilon$ (assuming PA or ZFC is arithmetically sound), but whose consequences are not a subset of any sound c.e. extension of PA (or ZFC). Namely we can generate long random binary strings and add sentences of the form "this string has Kolmogorov complexity at least $n$". $\endgroup$ – James Hanson Apr 3 at 15:14
  • $\begingroup$ @JamesHanson This is a fun remark. Do you know of further elaborations or variations along this theme that I could read about? $\endgroup$ – Gro-Tsen Apr 3 at 15:34