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.



> 
> 1. Can one characterize exactly what it means that Q1 may be *consistently lying*?
> 2. 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.)



Model existence and consistency conditions for $\Pi_1^0$ oracles
There's a natural way to define "consistently lying" (let's say *plausible*, to include the true $\Pi^0\_1$ theory):



> 
> A set $A$ of (indices for) $\Pi^0\_1$ sentences is *plausible* if $PA\cup A\cup\{\neg \varphi: \varphi\in\Pi^0\_1\setminus A\}$ is consistent.
> 
> 
> 


Note that this definition requires us to believe that $PA$ is consistent (in order to avoid triviality - although of course we could replace $PA$ with something weaker if we prefer), and to take for granted the notion of "consistency" (this is a bigger foundational issue). For now I'm not going to treat these issues, but for what it's worth the latter seems inescapable to me: I see no reason that there should be a notion of plausible set of sentences which is resistant to changes in the ambient metatheory of arithmetic.


The sentence "$T$ is consistent is (for appropriate $T$) a $\Pi^0\_1$ sentence; so - as you observe - if $T$ is inconsistent, and $A$ is plausible, then "$\neg Con(T)$"$\in A$. Put another way, any theory a plausible set thinks is consistent, *is* consistent. Of course the converse may fail badly: a plausible $A$ may think that practically anything is inconsistent!


Similarly, your comment about models generating plausible sets is entirely correct. Suppose $T$ is appropriate (e.g. $T=PA$); then for any model $M\models T$, let $A\_M=\{\varphi: \varphi\in \Pi^0\_1, M\models\varphi\}$. (Note that $A\_M$ is a set of *standard* $\Pi^0\_1$ sentences.) Now $A\_M$ is a plausible set (note that this is true even if $M\models\neg Con(T)$!). (Note that such an $M$ may think "my $\Pi^0\_1$ theory is inconsistent;" this does not mean that $A\_M$ will be implausible!)


Finally, you ask whether the converse holds: given a plausible $A$, does $A$ provide a proof of $Con(T)$ (assuming "$Con(T)$" is in $A$)? The answer is yes, roughly because - as you expect - we can use $A$ to effectively perform the Henkin construction relative to $T$. Perhaps surprisingly, the answer remains yes - in a certain sense - even if "$Con(T)$" is **not** in $A$!


This is via - as the beginning of your question suggests - Turing reductions more complicated than the explicit Henkin process. I claim that every plausible set $A$ is of **PA degree**; it is well-known that any PA degree computes a model of any computable consistent theory $T$.


Recall that a set is of PA degree if it computes a path through any computable infinite binary tree $\mathcal{T}\subseteq 2^{<\omega}$. (I'll use the mathcal font for trees here to avoid confusion with theories. Well, for every such $\mathcal{T}$ and $\sigma\in\mathcal{T}$, let $p\_\mathcal{T}(\sigma)$ be the sentence $$\mbox{"The subtree $\mathcal{T}\_\sigma=\{\tau\in\mathcal{T}: \tau\preccurlyeq\sigma\mbox{ or }\sigma\preccurlyeq\tau\}$ has height at least that of $\mathcal{T}$."}$$ Let $A$ be plausible; we now inductively a path $f$ through $\mathcal{T}$ as


* $f(i)=1$ iff $p\_{\mathcal{T}}(f\upharpoonright i-1^\smallfrown\langle 0\rangle)\not\in A.$


(Adopting the convention that $f\upharpoonright -1)$ is the empty string.)


By plausibility of A, $f$ cannot die out before $\mathcal{T}$ does.




---


OK, so any plausible $A$ is PA, and hence computes a model of any consistent computable theory $T$; but *how* does it compute such a model, given that the obvious Henkinization construction breaks down right at the outset if $A$ thinks $T$ is inconsistent?


Well, the tree above should remind you of Rosser's trick - replacing the Godel sentence "I am not provable" with the sentence "For any proof of me, there is a shorter disproof of me" to reduce the consistency assumption. That's exactly what's going on here. Basically, we perform the Henkinization argument not *preserving consistency*, but *avoiding rapid inconsistencies*: that is, we look at some sentence $\varphi$ (in a witness-expanded language), and ask $A$ "Which of [what we have so far]+$\varphi$ and [what we have so far]+$\neg \varphi$ has a *shortest* proof of inconsistency?" We then pick the other one.


