show/hide this revision's text 3 added 9 characters in body

If the proof system is recursively axiomatizable, this situation cannot occur.

If there exists a proof of $\Theta$, there exists an algorithm to find that proof. Namely, search the recursively enumerable set of deductions until you find a proof of $\Theta$. This must terminate, as we have proved that $\Theta$ is provable.

If the proof system is NOT recursive, then this may be possible. Consider the following set of axioms $\Sigma$ in the signature of arithmetic. Let $A$ be an infinite set which does not contain any infinite r.e. set. Define $$ \Sigma = \{ (\bar k = \bar k) \wedge \sigma \mid k \in A, k > \ulcorner \sigma \urcorner, \mathfrak N \models \sigma \} $$

Now, note that any sentence provable in $Th(\cal N)$ is provable is in $\Sigma$. However, there is no algorithm to transform produce such proofs from $\Sigma$. To do so would require enumerating arbitrarily large elements of $A$, which is impossible

show/hide this revision's text 2 added 574 characters in body; added 9 characters in body; added 16 characters in body

If the proof system is recursively axiomatizable, this situation cannot occur.

If there exists a proof of $\Theta$, there exists an algorithm to find that proof. Namely, search the recursively enumerable set of deductions until you find a proof of $\Theta$. This must terminate, as we have proved that $\Theta$ is provable.

If the proof system is NOT recursive, then this may be possible. Consider the following set of axioms $\Sigma$ in the signature of arithmetic. Let $A$ be an infinite set which does not contain any r.e. set. Define $$ \Sigma = \{ (\bar k = \bar k) \wedge \sigma \mid k \in A, k > \ulcorner \sigma \urcorner, \mathfrak N \models \sigma \} $$

Now, note that any sentence provable in $Th(\cal N)$ is provable is in $\Sigma$. However, there is no algorithm to transform produce such proofs from $\Sigma$. To do so would require enumerating arbitrarily large elements of $A$, which is impossible

show/hide this revision's text 1

If the proof system is recursively axiomatizable, this situation cannot occur.

If there exists a proof of $\Theta$, there exists an algorithm to find that proof. Namely, search the recursively enumerable set of deductions until you find a proof of $\Theta$. This must terminate, as we have proved that $\Theta$ is provable.