Algorithm to force decidability of statements using an intuitionistic series of new axioms Say that a set $\Phi$ is a finite set of statements in
Peano arithmetic is meekly consistent if it contains no
"inner,immediate" contradiction, i.e. for any statements $\alpha,\beta$, it does not contain 
any of $\lbrace \alpha,\neg{\alpha} \rbrace$, $\lbrace\alpha\wedge\beta,\neg{\alpha}\rbrace$,
$\lbrace\alpha\wedge\beta,\neg{\beta}\rbrace$, $\lbrace\alpha\vee\beta,\neg{\alpha},\neg{\beta}\rbrace$, $\lbrace\alpha,\alpha\Rightarrow\beta,
\neg{\beta}\rbrace$, $\lbrace \alpha,\beta,\neg{\alpha\wedge\beta} \rbrace$, $\lbrace \alpha,\neg{\alpha\vee\beta} \rbrace$,
 $\lbrace \beta,\neg{\alpha\vee\beta} \rbrace$ or $\lbrace \forall x \alpha(x),\neg{\alpha(c)}\rbrace$
where $c$ is a constant. Thus for example
$\lbrace\alpha,\alpha\Rightarrow\beta,\beta\Rightarrow\gamma,\neg{\gamma}\rbrace$ is meekly consistent
but not consistent in the usual sense.
Consider pairs $(\Phi,n)$ where $\Phi$ is a meekly consistent finite set of statements in
Peano arithmetic and $n$ is an integer. Say that $p'=(\Phi',n')$ is an 
elementary intuitionistic extension of $p=(\Phi,n)$ iff either $n'=n+1$ and
$\Phi'=\Phi$, or $n'=n$ and $\Phi'=\Phi\cup \lbrace \phi \rbrace$ where
-$\Phi\cup\lbrace\phi\rbrace$ stays meekly consistent.
-$\phi$ satsifies the intuitionistic constraint : if $\phi$ is of the form
$\exists x \alpha(x)$, then $\alpha(k)\in\Phi$ for some $k\leq n$.
Next, say that $p'$ is an intuitionistic extension of $p$ if there is 
a chain of elementary intuitionistic extensions starting with $p$ and ending with
$p'$. We call $p$ accessible from $A$ (or $A$-accessible for short) when it is an intuitionistic extension of
$(A,0)$, where $A$ is a finite set of axioms (or provably true statements) of 
Peano arithmetic.
For a finite set $\cal F$ of statements in Peano arithmetic, we say that
$\cal F$ is decided by $p=(\Phi,n)$ iff $\Phi$ contains $\phi$ or $\neg\phi$
for any $\phi\in{\cal F}$.
If we do not worry about effectiveness, it is obvious that for any $A$, any $\cal F$
is decided by some $A$-accessible $p$ : use "Skolemization" and for any true 
existential statement $\exists \alpha(x)$ in $\cal F$, simply walk up the integers 
until you encounter a witness $i$ satisfying $\alpha(i)$. Once you have done
that for each one of them, the intuitionistic constraint becomes vacuous for all
true statements, so you can finish by inserting all the true statements in $\cal F$, along with the negations of the false statements in $\cal F$.
It is quite another matter to ask if there is a computable algorithm that produces
an $A$-accessible $p$ deciding $\cal F$, from any given $\cal F$ and $A$.
Intuitively all the obstacles to such an algorithm comes from logical connections 
between statements in the finite set $\cal F$, and we should be able to
enumerate those obstructions in finite time, so such an algorithm should exist. I don't 
know how to turn that intuition into a proof however.
 A: What I find strange in your definition is that you don't ask that for formulae $\phi$ meekly consistent to be "satisfied" by $\Phi$. What I mean is for $\phi=\alpha\vee\beta$ you ask only that $\neg \alpha\notin\Phi$ or $\neg\beta\notin \Phi$ but you don't ask that $\alpha\in\Phi$ or $\beta \in \Phi$.
So I think that you can trivially build an accessible $p$ for any set $F$ of statements in Peano arithmetic. I show this by recurrence on the number of statement in $F$:
$F=\{\phi\}$: two cases either $\phi\in A$ and then $p=(A,0)$ decide $F$, or $\phi\notin A$ then $p=(A\cup\{ \neg \phi\},0)$ is an elementary intuitionistic extension of $(A,0)$ and $p$ decide $F$.
Assume now that one can build an accessible $p=(\Phi,n)$ for any set $F$ of $k$ statements in Peano arithmetic.
Let $F=F'\cup\{\phi\}$ be a set such that $F'$ contains $k+1$ statements in Peano arithmetic. Let $p=(\Phi,n)$ be such that $p$ is accessible and $p$ decide $F'$ (it is computable by hypothesis).
Either $\phi\in\Phi$ and then $p$ decide $F$. Or $\phi\notin\Phi$ and thus $p'=(\Phi\cup\{ \neg \phi\},n)$ is an elementary intuitionistic extension of $p=(\Phi,n)$ and thus is accessible and $p'$ decide $F$.
Hence for any (finite) $F$ you can build an accessible $p$ such that $p$ decide $F$.
