Embed Notice

Negative axioms can be postulated without loss of canonicity.

In this thread I want to explain a 3-page research note Coquand, Danielsson, Norell, Xu and myself wrote with the above title, back in 2013 with revisions and additions in 2017:

http://www.cs.bham.ac.uk/~mhe/papers/negative-axioms.pdf

There are many reasons people may (or may not) be interested in constructive mathematics.

* One is philosophical. For me, it is hard to agree (or even disagree) with the philosophical justifications, but this thread is not about this.

* Another one is that mathematical objects of interest, such as toposes, are intrinsically intuitionistic in nature, even when they are developed in a classical meta-theory. It is this that I find very persuasive, and this is a purely mathematical view independent of philosophical considerations, but this thread is not about this either.

* Yet another one, related to the first, but founded on a firm mathematical basis instead, is that "constructive proofs compute". I also find this persuasive.

I usually write things here based on the second bullet point, but this thread is about the third one.

1/