TL;DR: How / where to formalize results concerning the logical strength of systems? Are proof assistants having a weak base theory but also enough infrastructure to make it feasible?
I'll start by giving some context. In studying Logic and foundations, a clear interest is the consistency of the set of axioms that you use; especially when showing that some statement is “independent” (or simply doesn't follow) from others. The cardinal example (pun slightly intended) of this is the Continuum Hypothesis (CH) that since Cohen we know that it can't be proved nor disproved with current mathematical methods.
The catch, obviously is that “current mathematical methods” above corresponds to “ZFC set theory“ (for which it was proved), and even by adding large cardinal assumptions (which include, by translation, CIC with universes). But if those foundations are self-contradictory, the previous paragraph is wrong. The correct reading is: If ZFC is consistent, then it doesn't prove CH; to the effects of the present question, the interesting version is: If ZFC is consistent, so is ZFC + ¬CH.
There are other equiconsistency results as that. For example, the following theories are equiconsistent:
- ZF + Choice for countable families + “Every subset of $\mathbb{R}$ is Lebesgue measurable”;
- ZFC + “there exists an inaccessible cardinal” (i.e., there exists a set universe).
In order to be able to formalize this theorem in a reasonable context, the underlying logic of the proof assistant should be at least weaker that ZFC plus one universe. Same goes for the independence of CH. On the other hand, proof assistants like Lean (and Coq?) assume a sequence of universes from the start; also, Isabelle/HOL has a session devoted to set theory, but its consistency strength is that of statement 2 above.
The question arises even for Isabelle/ZF if you want to work with theories weaker than ZFC. In this state of affairs, I would like to know if there is any proof assistant that has a very weak foundation, that allows to work smoothly with theories of varying strength.
By searching the site, I found a related question asking for the formalization of model theory, and another relevant one mentioning also other systems of different strength (Peano / Primitive Recursive Arithmetic / Bounded Arithmetic, systems of reverse mathematics). But one point to be considered is that if one starts with plain PA / PRA then you have to code all the reasoning inside it, and usually tactics work only at the surface.