$\textbf{Q}$ fails to prove some correct $\forall$-rudimentary sentence 
Show that the existence of a semirecursive set that is not recursive
  implies that any consistent, axiomatizable extension of Q fails to
  prove some correct $\forall$-rudimentary sentence.

I have the following facts:


*

*Every recursive function is representable in Q (and by an $\exists$-rudimentary formula).

*Every recursive relation is definable in Q (and by an $\exists$-rudimentary formula).


If $T$ is a consistent, axiomatizable theory containing Q:


*

*Every set semi-definable in $T$ is semirecursive.

*Every set definable in $T$ is recursive.

*Every total function representable in $T$ is recursive.


Are there any examples of semirecursive sets where this structure holds? Or must their existence be proven mathematically?
 A: There are certainly many examples of sets of natural numbers that are semirecursive but not recursive. 
One famous example begins with an enumeration $f_i$ of all the partial recursive functions. Let $A = \{ j : \text{for some $n$, } f_j(n) = 0\}$. That set is easily shown to be semirecursive, but a diagonalization argument shows that it is not recursive. 
Another example is related to the halting problem: $B = \{ j : f_j(0) \text{ is defined} \}$. A similar diagonalization argument shows that this set is not recursive, but it is easily shown to be semirecursive. 
The phenomenon of sets that are semirecursive but not recursive spreads throughout all of mathematical logic. 
For example, the set of (codes of) formulas of the language of Peano Arithmetic that are provable in Peano Arithmetic. This set is semirecursive (search all proofs for a proof of a particular theorem) but, by the incompleteness theorems, it cannot be recursive. 
Similarly, we can take the set of (codes of) first order sentences, in a language with one binary function symbol, that are logically valid. This set is semirecursive but not recursive. This is a famous theorem of Trahktenbot about undecidable theories. Many other undecidable theories are known. 
For one more example, the set of (codes of) multivariate polynomials over the integers that have at least one root is semidecidable but not decidable - this is the resolution of Hilbert's 10th problem due to Matiyasevich, Davis, Putnam, and Robinson. 

Here is the rest of the idea behind the problem. Let $A$ be a semirecursive set that is not recursive.


*

*$A$ is definable by a $\Sigma^0_1$ formula $h$, i.e. a $\Sigma$-rudimentary formula. So we have that, for all $k$, $h(k) \leftrightarrow k \in A$. The complement of $h$ is a $\Pi^0_1$ formula, i.e., a $\forall$-rudimentary formula.

*A particular property of $Q$  and stronger theories is that $Q$ is proves every true (i.e. correct) $\Sigma^0_1$ sentence. In particular, for each $k$ such that $k \in A$, we have that $Q$ proves $h(k)$.

*Also, because the axioms of $Q$ are all true (i.e. correct), we have that for each $k$, if $Q$ proves $h(k)$ then $k \in A$, and if $Q$ proves $\lnot h(k)$ then $k \not \in A$

*If it were also the case that, for all $k \not \in A$, $Q$ proves $\lnot h(k)$, then $A$ would be recursive. The decision procedure would be: given $k$, search for a proof in $Q$ of $h(k)$ or $\lnot h(k)$. Then $k \in A$ or $k \not \in A$, accordingly, from (3).

*Thus there is some true $\forall$-rudimentary sentence, which is of the form $\lnot h(k)$ for some $k$, which $Q$ does not prove.
