Can mathematical formalizations in NuPRL be trusted as correct in the greater mathematical practice?

Question

In A Cubical Language for Bishop Sets, the authors write:

As a consequence of its fundamentally untyped nature, formalizing a theorem in Nuprl does not imply the correctness of the corresponding theorem in standard classical math-ematics (the global mathematics of constant or discrete sets), nor even in most forms of constructive mathematics (the local mathematics of variable and cohesive sets). It is worth noting that the problem is not located in the presence of anti-classical principles (which are interpretable in logic over a variety of topoi), and rather arises from the commitment to untyped ontology.

What is meant by this statement? I would wager that the NuPRL team disagrees, as some of their publications are about mathematical theorems, including: Formalizing Category Theory and Presheaf Models of Type Theory in Nuprl and Constructing Analysis and Experimental Mathematics using the NuPRL Proof Assistant.

Is there an example of a theorem that is provable in NuPRL, but that a mathematician would reject as false? Also, it shouldn't be conjured up in ZFC versus MLTT, as theorems like $1 \in 2$ are generally understood and happily ignored.

Answer 1

At least one of the authors of the paper is around so they can speak for themselves what they meant. I can comment on what they wrote, but let me make a disclaimer first, lest someone misunderstand me:

NuPRL was an extremely influential proof assistant that introduced many techniques that are used in today's proof assistants. Its historical importance can be compared to that of AUTOMATH.

Now I can criticize it safely.

NuPRL is a realizability model of sorts. One can certainly “trust” proofs accepted by NuPRL to be valid in the underlying model. But it is hard to say much beyond that. I can make an analogy: suppose someone shows that a statement $\phi$ is valid in the topos of sheaves on the torus. What does that say about $\phi$ being valid in other toposes?

Finding fault with untypedness makes very little sense to me. We know from realizability theory that an untyped realizability model can be equivalent to a typed one, and I do not see the authors arguing that NuPRL is not of that kind. Neither is it clear how things would be better if NuPRL were based on a typed model, say something like PCF. The comment about cohesive variable sets makes me think that the atuhors are complaining that NuPRL does not have a sheaf-theoretic interpretation.

In my opinion, what really matters is the fact that NuPRL relies on validity rather than derivability. To compare NuPRL and Coq (but the same holds if we swap Coq for Agda, and to a lesser degree Lean):

• In Coq a judgement is accepted when it has a derivation. There is a decidable procedure for telling whether a derivation is correct (not to be confused with decidable checking, which is a decidable procedure for telling whether a judgement has a derivation).

• In NuPRL a statement is valid when it is realized. It is undecidable whether a given program actually is a realizer of a given statement.

Consequently, NuPRL suffers from several defects:

1. Statments accepted by NuPRL are valid in one particular (idiosyncratic) model. There seems no systematic way of interpreting statements accepted by NuPRL in other models. In contrast, Coq's formal system has many interpretations (set theory, intuitionistic set theory, realizability, etc.) so statements accepted by it are valid in many situations.

2. When a new proof rule is added to NuPRL, it is justified by there being a realizer for it. However, whether something actually is a realizer depends on further assumptions about meta-theory. With Coq there is no dilemma, because recognizing derivations is a very easy thing that can be carried out in a very weak fragment of arithmetic (so weak that it even does not detect the difference between intuitionistic and classical logic).

3. Because NuPRL is tied to validity in one particular model, it is very opinionated: excluded middle is invalid, Brouwerian continuity is valid (in recent version), choice is invalid, whether Markov's principle is valid depends on your meta-theory, etc. If you don't like these you're out of luck. In contrast, Coq's CIC is very conservative and leaves such statements undecided. The user is free to postulate a variety of different combinations of axioms safely, so long as they know them to be consistent.

Answer 2

As an author of this paper, I think I would write it a little bit differently if I had the chance today. Before I begin, let me echo Andrej's comment that Nuprl is a very significant moment in the history of type theory and even constructive mathematics, and none of what I say (then or now) is meant to detract from that. I obviously have immense respect for Nuprl and the people who built it, who were in many ways pioneers in type theory and in interactive proof assistants. Much of what we have today (like Coq and Agda) owes its present shape to the ideas developed by the PRL Group.

To me the difficulty with relating Nuprl to mathematics is basically one of methodology. As Andrej says, Nuprl's Computational Type Theory is based on "truth in one model"; as a result, there are many things that are true in this specific model that are false in the category of sets, false in many categories of presheaves, and false in many categories of sheaves. This is not the fault of (e.g.) realizability semantics, but rather the fault of confounding syntax and semantics. Both are important, but semantics benefits from multiplicity --- and the multiplicity of semantics is embodied in syntax. We can therefore expect strange results if we say that syntax is just a way to speak about one single example of semantics.

So my aim is not to say "realizability is bad" --- realizability is clearly very good. But I think it is bad on balance to base a proof assistant on one single model (bad in ways that COULD NOT have been anticipated [clarification: by that community] in the early 1980s when this was going on!) because it limits the applicability of your results.

Because Nuprl incorporates axioms that are not true in ordinary math, nor in the relative ordinary math of topoi, we cannot take a Nuprl proof about groups and use it as evidence to a "proper mathematician" for the truth of that statement about groups in a way that applies to that mathematician's work. This limits the ability to communicate and re-use results, but that is to me the entire point of mathematics.

I want to end by saying that my perspective on mathematics is not the only one. Nuprl is much inspired by the ideas of L.E.J. Brouwer who took a very different viewpoint --- a proof in Brouwer's style about groups also does not necessarily lead to evidence that a mathematician would accept for the truth of that statement about groups. But Brouwer's perspective was that all the mathematicians were wrong, and that only he was right. If that was actually so, then one could not blame him for doing his proofs in a way that was not backward compatible.

Therefore, the question that Nuprl raises is nothing less than: is mainstream mathematics wrong? Back when I was building tools based on Nuprl, I believed that normal mathematics was wrong. I no longer believe that though.

Lastly, I want to say that the above applies to Nuprl when viewed as a general-purpose language for mathematics --- for the reasons I describe, it cannot be a general-purpose language in that sense. But this is not the only thing Nuprl has been: Nuprl has also been a "synthetic domain theory" (an implementation of the slogan "domains are just types, don't worry about continuity" --- albeit quite different from the one pursued by the category theorists). Nuprl's synthetic domain theory aimed to let you reason about programs that use partial functions in ways that don't terminate, like LCF. One can argue today whether their approach was the best or not, but I think this is a very interesting aspect of Nuprl that is less well known than it should be. Nuprl qua synthetic domain theory doesn't claim to be general purpose, only useful for a specific purpose. So I think that's a good way to think about Nuprl that respects the great accomplishments of that team.