Axiom checking as type checking?

The key observation of the Curry-Howard correspondence is that the inductive structure of terms in type theory mirrors the inductive structure of proofs in logic.

For example, given two terms $t_1$ and $t_2$ of types $A_1$ and $A_2$, I can construct a term $(t_1,t_2)$ of the product type $A_1\times A_2$. Similarly, given two proofs $p_1$ and $p_2$ of the propositions $Q_1$ and $Q_2$, I can put them together to form a proof $(p_1,p_2)$ of the conjunction $Q_1\land Q_2$.

On the other hand, models of a proposition (at least in ordinary semantics for first-order / predicate logic) just don't have this same kind of inductive structure. Given models $M_1$ and $M_2$ of sentences $\varphi_1$ and $\varphi_2$, there's no canonical way of constructing a model of the conjunction $\varphi_1\land \varphi_2$. So I'm not optimistic that the kind of extension of Curry-Howard that you're looking for is possible.

It's conceivable to me that you could change the notion of "model" to something sufficiently syntactic to make this work - but that would likely involve making a "model" of $\varphi$ essentially an encoding of a proof of $\varphi$, and then relying on the usual Curry-Howard correspondence.

Yes, there are two notions of "fit into" here:

• Terms (what you call instances here) "fit into" types or don't, and that is checked when you do type checking
• Structures (e.g. set theoretical constructions) "fit into" propositions or don't, and that's checked by when you verify whether the structure is a model.

I think there's nothing wrong with drawing an analogy of how things "fit into" another here, as both processes can be considered under the guise of a computational task. Although there are many stratification involved.

• For one, mathematical logicans (and e.g. set theorists) will do everything formalistically with symbols on paper, but nontheless they make a conceptual distrinction between syntax and semantics. As a result, you have philosophical positions like mathematical Platonism which consider mathematical structures as farther away from syntax and closer to something "actual". Something that's realized among possible semantics. Computer science type theorists (which are also logicans of course, just sometimes closer to another school, say the proof theorist ones) will work in large parts purely on the syntactic side (and semantics are sought in more general setups than e.g. in set theorists departments)
• Secondly, as mentioned, both "checkings" here are forms of computations and it's worth pointing out that what's doable here will depend on the underlying logic. The Hindley–Milner type system is the framework that motivated the programming languages ML and then Haskell, and grants a nice type checking routine. The frameworks where good checking is possible made cuts. Modern efforts in ramping up a dependently typed language gear towards a constructive/intuitionistic logic that now include strong forms of quantifiers, while logicans and model theorists do large parts do a deeper and thus less varied (relatively speaking) study of the long established strong first- or higher order logics. The answers in this logic SE questions are one among the most interesting on the platform. As is always the case with such broad questions on logic, one could now go down many rabbit holds. I might give a shoutout to Tarski's restricting theorem for strong logics. Decidability is also a question for type systems, if you just choose any.
• Along with the theme of restrictions, type checking of a term checks all it can, while with propositions, there's always many and different aspects of a structure you can validate. Again, here, if you make cuts and your type system admits subtyping and whatnot, I suppose you can take coarser views on terms here too.
• In the latter notion of "fit in", there's the concept of categoricity and one may try to reflect that in uniqueness types.
• If you have narrowed down a your logics of interest and decide you want to approach your question from a raw computation and "fit into" perspective, then the subject of abstract rewriting and rewriting systems, which may strike one as even more formal than subfields mathematical logic, may be down your alley.

Side note 1: The verification process in the latter case need not even be restricted to axioms but we can do that for any propositions.

Side note 2: I'm not a fan of your initial wording "checking whether a proof of a proposition is correct". I'd instead say "checking whether an expression is a proof of a proposition". I say that because if you use your language here, then we grant every term the status of being a "wrong proof" for almost all propositions. That's just a question of our language here, though.