With your approach, the assumption on will_halt that you start out with "Assume we had a program will_halt(source, args) that returns True if eval(source, args) halts and False otherwise." does not hold anymore: there are cases where evaluating source runs forever, but your will_halt returns True. So, whatever you do afterwards does not address the halting problem anymore, because that starts out with your (original) assumptions.
(As an aside, note that it is trivial to write a will_halt function that returns True if the eval(source,args) terminates and without restriction on the return value if eval(source,args) does not terminate. It's useless, though.)
$\mathsf{PA}$ is vastly more than enough to prove that the halting problem is incomputable. $\mathsf{PA}$ is in fact massive overkill for the vast majority of theorems about natural numbers, or "finitary objects" (such as Turing machines, despite the infinite tape present in our intuitive conception of them) more generally.
Meanwhile, in some sense $\mathsf{Q}$ is too weak a system for the question to be meaningful. There is very little which $\mathsf{Q}$ can prove at all - e.g. it cannot prove that every number is either even or odd (= $1$ less than an even number), nor can it prove that addition is commutative. Among other things this means that intuitively-trivial modifications to definitions often wind up resulting in inequivalent versions "over $\mathsf{Q}$." For example, I don't believe that $\mathsf{Q}$ proves that $2$-tape Turing machines are no stronger than $1$-tape machines. At this point it's not clear that the question means what we want it to.
Here's a sketch of why the incomputability of the halting problem goes through in a very weak system of arithmetic. (There are various versions of the halting problem; I'll use $\{e:\Phi_e(0)\downarrow\}$, where $\Phi_e$ is the $e$th Turing machine in the standard enumeration and "$\downarrow$" means "halts," for simplicity.)
The proof boils down to basic logic + a machine construction: given a machine $\Psi$ we need to define an auxiliary machine $\hat{\Psi}$ to "defeat" $\Psi$ as a putative halting problem solver. This $\hat{\Psi}$ behaves as follows: on input $e$ it simulates $\Psi(e)$; once (if ever) this simulated computation halts, $\hat{\Psi}$ goes into an endless loop if the result is $1$ and otherwise halts and outputs $0$ (say).
So all we need is a theory of arithmetic capable of proving that the construction $\Psi\leadsto\hat{\Psi}$ actually "makes sense." Since it's an explicit construction this boils down to a totality claim, and at a glance knowing that polynomial functions are total should already be enough. So we get all the way down to theories of bounded arithmetic, which form incredibly tiny fragments of $\mathsf{PA}$.
Best Answer
The basic idea is to use first-order logic to describe any turing-machine and its input, and to show that those sentences logically imply the 'halting sentence' "This machine with this input will halt" if and only if that machine with that input will indeed halt.
So given that, you can solve the halting problem if you can decide first-order logic consequence, i.e. the Entscheidungsproblem: when presented with any machine and input, you describe it using first-order logic, and decide whether or not the halting sentence is a logical consequence: if the halting sentence is a logical consequence, then the machine will halt, and if the halting sentence i not a logical consequence, then the machine will not halt.
To provide a bit more detail as what that first-order description looks like:
First, let's assume the turing-machine only uses a binary alphabet: $0$'s and $1$'s (or: blanks and marks). So, if we use integers to index the cells of the tape, we can use a predicate Mark(t,x) to say that "At time t, square x has a $1$" (by 'time t' we mean: after t steps of operation).
So, assuming the input tape consists of finitely many $1$'s, we can fully describe that input tape by a first-order logic sentence. For example, assuming that the input tape has $1$s in cells $0$, $1$, and $2$, we can say $$\forall x (Mark(0,x) \leftrightarrow (x = 0 \lor x = 1 \lor x=2))$$.
Indexing the internal states of the machine, we'll also have a predicate $State(t,y)$ that expresses that "After t steps, the machine is in state $y$". Thus, for example, if state $1$ is the starting state, then we use $$State(0,1)$$.
Another predicate we use is $Cell(t,x)$ that says "After t steps of operation, the read-white head of the machine is at cell $x$". So, assuming the machine starts at cell $0$ we can say $$Cell(0,0)$$
The above three statements provide us with the machine-tape configuration at time $0$: it describes what the tape looks like, what state the machine is in, and what cell it is looking at the very start.
Of course, we'll also need to describe how the Turing-machine works. For example, suppose that whenever the machine is in state $1$, and is looking at a $1$, then it will change that $1$ into a $0$, move right, and stay in state $1$. For that, we can use the following expression:
$$\forall t \forall x ((State(t,1) \land Cell(t,x) \land Mark(t,x)) \to (State(t+1,1) \land Cell(t+1,x+1) \land \neg Mark(t+1,x) \land \forall z(z \neq x \to (Mark(t,z) \leftrightarrow Mark(t+1,z)))$$
(see how that works?)
OK, so we add a sentence like that for every transition/instruction that defines the working of the machine.
Now we have all our premises: the machine-tape starting configuration, and how the machine works. OK, so now can show that the machine-tape configuration for any time step after that is a logical consequence of those premises. Following our example, notice that after $2$ steps of operation, the machine will have changed the first two $1$'s into a $0$, is still in state $1$, and is now looking at the third $1$, while the rest of the tape is all blank. This machine-tape configuration can be described as:
$$State(2,1) \land Cell(2,2) \land \forall x (Mark(2,x) \leftrightarrow x = 2)$$
Now, you can easily verify that this statement is a logical consequence of the premises. And, given a complete proof system, it is therefore also provable.
Fun exercise for you to do: use a proof system to derive this statement from the previous ones ... and when you do so, you'll find that you'll need some further axioms like $1+1=2$ or, better yet, use some general axiomatization of the integers ... these are details that I won't provide since that'll detract from the basic proof idea here.
Another thing I won't prove, but simply tell you, is that you can show that any such machine-tape configuration sentence is a logical consequence of the initial premises if and only if that machine and tape are indeed in the very configuration after that many steps as described by the sentence.
Or, in terms of provability: if you have a sound and complete proof system for First-order logic, then a statement like $state(7,4)$ is provable from the premises if and only if the machine as described by the premises, when starting on the input tape as described by the premises, will in fact be in state $4$ after $7$ steps of operation.
OK, so now let's assume that state $0$ is the halting state of the Turing machine. Then we can define a halting sentence as follows:
$$\exists t \ State(t,0)$$
Given the above, this halting sentence is a logical consequence of the premises if and only if the machine-input pair as described by the premises does halt at some point.
So again: if the Entscheidungsproblem is solvable, then we can decide first-order logical consequence. So that means that we can decide whether or not the halting sentence is a logical consequence of the premises, and thereby we can decide, for any machine-input pair, whether or not the machine halts on that input, i.e. we can solve the halting problem.
(note that in the end, we are really not interested in provability: when it comes to the entscheidungsproblem and the halting problem, we are really just interested in decidability of logical consequence and decidability of halting-ness.)
But of course, we can't solve the halting problem. Hence, we can't solve the Entscheidungsproblem either. And this is what Turing showed in his famous 1936 paper: he laid out the notion of (what we now call) Turing-machines to try and give a mathematical definition of 'computation', he used this to show that there are things that are not computable (the halting problem!), and used that to show that the Entscheidingsproblem is not solvable either. As some have said: it's as if he laid down the foundations of all modern computer science almost as a by-product of his proof that the Entscheidungsproblem for logic is unsolvable!