§ 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.