New answers tagged

2

I don't know the history of the phrase "neutral constructive mathematics", but I would guess that it is meant to be analogous to "neutral geometry". Neutral geometry (or absolute geometry) is the part of plane geometry which makes no assumption about the truth or falsehood of the parallel postulate. A theorem of neutral geometry is valid ...


11

I suppose I ought to contribute an answer to this. Maybe I should start by saying that I did not originate the term "neutral constructive mathematics". I believe I picked it up from Martin Escardo; I'm not sure whether he originated it. On the other hand, of course I can only speak to what I mean by it myself. It's easier to say what I don't ...


7

Surely the way that we should define neutral constructivity is not by legislating particular systems but by considering how those interested in (constructive) foundations should interact with others in the community of mathematicians and vice versa. This is becoming more relevant as interest grows, not just in formalising individual proofs with particular ...


15

You'll probably have better luck with the phrase "intuitionistic higher-order logic" (IHOL). A good place to start is the book by Lambek and Scott, Introduction to Higher Order Categorical Logic. But here is a shorter online article that may be helpful: J. Lambek and P.J. Scott, Reflections on a categorical foundations of mathematics. As Paul ...


3

To 'turn an object $A$ of a category $\mathcal{C}$ into a set' you can consider the set of objects mapping into/out of that object from/to some other object; if you consider maps out of a terminal object ${\bf 1}\to A$ these are called global elements of the object. If $\mathcal{C}$ is a well-pointed topos these global elements are sufficient to delineate ...


8

The general notion you're looking for is a representable functor. For example: $${\mathcal E}(X\times{-},Y) \sim {\mathcal E}({-},Y^X)$$ $${\textsf{Sub}}({-}) \sim {\mathcal{E}}({-},\Omega)$$ The thing on the left is a general contravariant functor from the category to $\mathbf{Set}$. The thing on the right is of the form ${\mathcal E}({-},R)$, where $R$ is ...


Top 50 recent answers are included