Stack Exchange network consists of 183 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.
Bishop's constructive mathematics has the property that if you prove something, then you can algorithmically extract a constructive witness to it. To slightly oversimplify, the witness to a real number will be a program generating a converging sequence of intervals (pairs of rationals). I'd call that algorithmic.
@Sergei: I'd recommend getting the book, Negri & von Plato, 2001, Structural proof Theory to someone who wants to study this approach, which emphasises the generalised elimination rules of Schröder-Heister, cf. e.g., www-ls.informatik.uni-tuebingen.de/psh/forschung/publikationen/…
@Todd: I did not find the discussion shallow, and I did not find Friedman to be hostile, although I entirely agree that Simpson framed the whole issue in a pointlessly divisive manner: the list-1 vs. list-2 distinction was presented almost as a matter of moral character. I agree that justice was not done to the structuralist viewpoint, but I still think that Friedman is right to say that categorical logicians (among others) have not presented a genuinely independent ontology for mathematics that achieves what modern set theory does.
I think the intent of the question is a good one, but this is a bit of a Celestial Emporium of Benevolent Knowledge approach to categorisation. "Euclid" covers a pretty diverse bunch of things, if it covers any technique found in the Elements.
@Kevin: Would you be happier if, instead of a revised version, an erratum, detailing by page/line the problems in the paper, were sent? This eliminates the risk of confusion over what is being reviewed.
One of my early refereeing mistakes was to do exactly this: after I finished writing my report on the paper with the same title I downloaded from the author's site, I took a look at the paper I had been emailed, to note that this paper was completely different: I had to largely rewrite my report, and changed my recommendation from reject to accept. Never again!
There seems to be a stage beyond 5, which we might call "Stockholm Syndrome", where you identify so completely with the new, frightening, more complex world that the enemy of complexity, the original simplicity, becomes your enemy: the only interesting groups are noncommutative, the only valid intuitions about formalisms are constructively well-grounded ones. We've all met stage-sixers, haven't we?
