15
$\begingroup$

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.

$\endgroup$
4
  • 1
    $\begingroup$ Nobody but the authors would really know what they meant. That said, I think this is mostly confusion due to poor wording that the authors could correct by rephrasing. As worded, I would interpret that there is no valid interpretation of Nuprl proofs in any recognized context. That doesn't make sense as-is. As admitted by the authors: the untyped ontology is an ontology! (Perhaps they claim it is not?) I certainly believe that some could-be interpretations of Nuprl proofs are impossible due to the untyped nature of Nuprl. $\endgroup$ Mar 11, 2022 at 5:38
  • $\begingroup$ That is a fair point that only really the authors would know, but evidence to the point that NuPRL constructions can indeed be trusted (or not!) by the working mathematician would resolve the issue in my eyes. The cited text is more evidence for why it is up for question. $\endgroup$ Mar 11, 2022 at 7:04
  • $\begingroup$ What the statement means, even with its current wording, is that there is no known interpretation of Nuprl proofs in a non-realizability context. I don't think there is a need to correct this... But I have expanded on the point in my full answer below. $\endgroup$ Mar 13, 2022 at 19:41
  • $\begingroup$ Here's an example of the flavor of statement that should be true in some form in Nuprl, which a mathematician would reject as false: "There exists a type B such that every type A is a subquotient of B." (It may take some care to state this properly though.) $\endgroup$ Mar 13, 2022 at 20:28

2 Answers 2

13
$\begingroup$

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.

$\endgroup$
9
  • 2
    $\begingroup$ This may deserve a standalone question, but what exactly is the metatheory used by NuPRL? This is a fairly critical question, but it is never explicitly laid out. The only place where I got an indirect answer was ironically the Rahli et al. implementation of NuPRL in Coq... $\endgroup$ Mar 11, 2022 at 9:33
  • $\begingroup$ @Pierre-MariePédrot: I don't know the answer. Bob Harper probably does. $\endgroup$ Mar 11, 2022 at 20:47
  • $\begingroup$ As an author of that paper, i agree with Andrej's characterization of our intent. For me a good language does not say things that are false in most topoi, but nuprl's CTT by definition (for better or for worse!) proves many things that are not true of sets, not true of presheaves, not true of sheaves, etc. Whether the nuprl formalism shares this problem depends on what version you consider, but it is very hard to pin down the meaning of a statement in the PRL formalism because the meaning of the sequent is totally nonstandard. (But closed statements are not difficult to see the meaning of.) $\endgroup$ Mar 13, 2022 at 19:15
  • $\begingroup$ to answer PMP's question, in the old days nuprl's semantics were done in "ordinary math". Now we know that they work in Coq without assuming axioms, but either impredicativity (like in coq) or induction recursion is needed for the PER model unless you plan to model only a fragment of the universe hierarchy. $\endgroup$ Mar 13, 2022 at 19:17
  • $\begingroup$ Is the impredicativity needed to show that PERs form a complete lattice? I bet they use that, for instance to get least fixed points of monotone operators on PERs. $\endgroup$ Mar 13, 2022 at 20:03
16
$\begingroup$

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.

$\endgroup$
3
  • 1
    $\begingroup$ I'm curious why you say that the badness of basing a proof assistant on one model could not have been anticipated in the early 1980s. I would have thought that even then, one could make an argument that a proof assistant should produce a proof that the average mathematician would accept. $\endgroup$ Mar 15, 2022 at 18:18
  • $\begingroup$ I think the problem is not so much the time but the community; so maybe my comment is misleading... You have to understand (1) the tradition that the people building proof assistants were working, and (2) the social and cultural disconnection between those people and the community of people who might have known better. $\endgroup$ Mar 15, 2022 at 19:59
  • $\begingroup$ Lastly I think there was a vision about computer programming being a new way to think about mathematics, and the early "versions" of this vision involved basing mathematics on a concrete model of computer programming. Such ideas have always been present in the philosophy of constructive mathematics, but the level of sophistication changed dramatically in the 20th century. From that point of view, it is natural to want to have a proof assistant to let you explore this new kind of mathematics. I think that viewpoint cannot actually pan out in the way that was hoped, but some are still trying. $\endgroup$ Mar 15, 2022 at 20:05

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.