On the Development of Non-Classical Mathematics
It is well known that classical theorems, when viewed from a constructive perspective, come apart at the seams. Typically there are crucial assumptions, implicitly made within the classical framework (a result of the classical validity of omniscience principles), which separate out different versions of the same theorem. Brouwerian examples demonstrate where, and why, these theorems are different and the program of constructive reverse mathematics is often able to pinpoint exactly the strength of nonconstructive principles necessary for the proving of these theorems. A good example is the intermediate value theorem (IVT)|constructively equivalent to the lesser limited omniscience principle (LLPO). The IVT becomes constructively provable if either stronger hypotheses are introduced, or the conclusion is weakened. This talk begins to shed some light on what happens in non-classical mathematics more generally (e.g. relevant mathematics, paraconsistent mathematics). In particular, we investigate results concerning order and locatedness|a constructive concept|within a framework of analysis founded on a variety of paraconsistent logic. Again, we find (perhaps unsurprisingly) that one classical theorem has many paraconsistently distinguishable versions. But we find (perhaps surprisingly) that the constructive techniques which play a central role in highlighting these dfferences can often be adapted to paraconsistency.