§ Why NuPRL and Realisability makes it hard to communicate math

• Superb answer by jon sterling

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.