Let a $\Pi_1^0$ sentence be a sentence asserting that some given Turing machine never halts at the empty input tape. Let Q1 be a (potentially consistently lying) oracle for deciding $\Pi_1^0$ sentences, and let a Q1-TM be a Turing machine with access to Q1. Let TT be a given first order theory whose axioms are enumerable by a Turing machine (without access to Q1), and assume that Q1 predicts that TT is consistent.
- Can one characterize exactly what it means that Q1 may be consistently lying?
- Is the existence of Q1-TMs sufficient for constructively proving that a model of TT exists?
The general idea is that Q1 is potentially consistently lying, iff it is impossible to prove that Q1 is lying. A proof that Q1 is lying would ideally be a Q1-TM, which halts at the empty input tape exactly if Q1 is lying. We assume that Q1 always predicts the same outcome for the same query.
If a given Turing machine halts at the empty input tape, then Q1 must correctly predict this. (Otherwise, consider the Q1-TM which enumerates all TMs, asks Q1 whether they will halt, and concurrently runs all TMs for which Q1 predicted they would not halt. If any of those TMs halts, then the Q1-TM halts and thereby proves that Q1 lied.)
If Q1 predicts that a given first order theory TT' is consistent and $\phi$ is an arbitrary first order sentence in the language of TT', then Q1 must predict that TT'+$\phi$ is consistent or predict that TT'+$\lnot\phi$ is consistent. If $\varphi$ is an arbitrary first order formula in the language of TT' and $c$ is a constant not occurring in $\varphi$ or TT', then Q1 must predict that TT'+$\exists x \varphi\to \varphi\frac{c}{x}$ is consistent.
Those last two statements about Q1 already show the sort of statements which would be required for constructively proving that a model of TT exists. (But the reasoning here already seems to come from a meta level.) If TT=PA (or TT=PRA) then any model of TT+Con(TT) should yield a potentially consistently lying oracle Q2. But will the last two statements about Q1 really be true for Q2? (Here, the assumption/hope is that we may also be allowed to use TT for trying to prove that Q2 is lying.)