Attempts to accommodate theories of different consistency strength in single assistant

Question

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:

1. ZF + Choice for countable families + “Every subset of $\mathbb{R}$ is Lebesgue measurable”;
2. 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.

Answer 1

You could address your goals by using a generic proof assistant, one that supports user-definable theories, such as Isabelle and Metamath, and I am sure there are others. These allow you to define your own weak formal system and work with it. However, once you define your favorite formal system, you will have a bare-bones proof assistant that will only become usable once you implement a substantial library of basic facts and constructions – and that is a rather daunting task. We need to learn how to lower the bar to having domain-specific proof assistants.

Another possibility is to use a popular proof assistant that supports a very strong formalism, but to carefully avoid its power. While not entirely satisfactory, doing so will allow you to actually get things done.

Specifically, suppose you want to show that if $\mathrm{ZFC} + X$ is consistent then so is $\mathrm{ZFC} + Y$, and you'd like to do this by demonstrating that a model of $\mathrm{ZFC} + X$ yields a model of $\mathrm{ZFC} + Y$. In whatever proof assistant you like, formalize the basics of Tarskian semantics: the syntax and logic of the first-order theory $\mathrm{ZFC}$, $\in$-structures, models of $\mathrm{ZFC}$ etc. Then you prove a theorem

ZFCX⇒ZFCY : Π (M : ∈-structure) . (M ⊨ ZFC+X) → Σ (N : ∈-structure) . (N ⊨ ZFC+Y)
ZFCX⇒ZFCY = 〈proof-goes-here〉

Since your proof assistant is too powerful, it allows you to just construct a model N of ZFC+Y from scratch, but you shouldn't do that. Instead you resist the Dark Side and use forcing to construct N from M in the weak fragment that you wish you were working in.

This is not ideal but is still well-worth doing. Think of it as partial formalization. You have formalized the desired construction, but you still have to manually check the proof to verify that it remains within the confines of a weak fragment (this may not be so simple if you use the standard library and lose track of what the library is doing). People actually do such things for lack of a better method. For example, the UniMath library formalizes mathematics in Univalent foundations on top of the assumption Type : Type – which is inconsistent! The authors review the code carefully and avoid dangerous moves. (I have it on good authority that the inconsistent assumption keeps them awake at nights.)