Reference request: the space of formalisms for proving function totality

Question

I'd like to develop an intuition about the space of axiomatic systems (formalisms) that can be used to prove totality of Turing machines.

To this end, I'm interested in the set of "totality proof checker" algorithms. Each such algorithm verifies proofs of function totality under some consistent set of axioms. That is (assuming a Turing-equivalent computational model with indexed partial functions $\varphi_e$, $e \in \mathbb{N}$),

\begin{align*} C = &\{ c \in \mathbb{N} \mid {} && \text{A function $\varphi_c$ is a totality proof checker iff}\\ &\quad \forall e ( && \text{given any function $\varphi_e$,}\\ &\quad \quad \exists p(\varphi_c(\langle e,p\rangle) = 1) &&\text{if $\varphi_c$ accepts some $p$ as proof of totality for $\varphi_e$}\\ &\quad \quad \Longrightarrow \forall x(\varphi_e(x)\downarrow) && \text{then $\varphi_e$ does in fact terminate on all inputs.}\\ &\quad )\\ &\} \end{align*}

(We might also require that totality proof checkers return $0$ when a proof isn't accepted.)

I'm looking for literature that can help me understand the space of such totality checkers, and in particular subset of computable ones: That is, once we're given some totality proof $p$, we can compute whether to accept the proof ($\varphi_c(\langle e,p\rangle)$). Some open-ended questions I have in particular (and I'm not sure if I'm asking the right questions):

• Can we enumerate some interesting subset of the computable totality checkers?
• Do the computable totality checkers form some sort of hierarchy with respect to the set of functions they can prove total?
• Is there some "maximally powerful" computable totality checker $\varphi_c$ such that whenever a function is provably total under any computable totality checker, then it is provably total under $\varphi_c$? I'm expecting there isn't -- but perhaps some weaker variant of this exists?

So my question is:

1. Is there literature that answers these types of questions? (I tried undergraduate textbooks like [1] but they didn't help much.)

2. Alternatively, it seems like the space of totality checkers might be the computational equivalent (via the Curry-Howard correspondence) of some space of axiom systems. Can we establish such a correspondence so that existing literature on formal logic can be brought to bear on this question?

[1] Rebecca Weber, Computability Theory