In any case, there is programming he has written M.H. Escardo. *Infinite sets that admit fast exhaustive search*. In LICS'2007, IEEE, pages 443-452, Poland, Wroclaw, July. pdf <https://www.cs.bham.ac.uk/~mhe/papers/exhaustive.pdf> (paper), hs <https://www.cs.bham.ac.uk/~mhe/papers/exhaustive.hs> (companion Haskell program extracted from the paper from https://www.cs.bham.ac.uk/~mhe/papers/ One could say: *There is nothing outside the code.* (The program stands on its own.) > > > > > > > *constructive mathematics, which I see as a generalization, rather than as > a restriction, of classical mathematics. * > > > Hmm…. That is highly debatable, and usually, when made rigorously, it is > akin to a form of solipsism. > > When a theory has less axioms, it has more models. So generalisation and > particularisation are permuted when we go from theory to model and vice > versa. But in arithmetic and analysis, things are more complicated. In the > Kleene realisability semantic for Intuitionist logic, (or in the effective > topos) we can have theorem which are classically false, for example. > > > > *In constructive mathematics, in the way I conceive it, computation is a > side-effect, rather than its foundation.* > > > Computation is a side effect of both classical arithmetic and intuitionist > arithmetic. > > Classicalism and Intuitionism differ only “really” on the real numbers and > analysis. With just arithmetic, it is mainly a change of vocabulary. I am > aware we can add nuances, but most makes not much sense in any serious > computationalist machine theology, were the main axiom has to be highly > non-constructive. But then physics get constructive defined, and do the > theology of the machine can be tested. > > > > > *What distinguishes classical and constructive mathematics is that the > latter is better equipped to explicitly indicate the amount of information > given by its definitions, theorems and proofs, which is related to topology > and domain theory.* > > > OK. > > > > > * The correct question is not whether a mathematical theorem is > constructive, but instead how much information its formulation (type) and > proof (inhabitant of the type) give. A good foundation has a rich supply of > types and ways to build their inhabitants so that the available amount of > information can be precisely expressed.* > > > Types are for applications. Reality is arguably untyped. With mechanism, > we recover intuitionism as the normal phenomenology of the machine, and > yes, she cannot live without types, locally, but for the fundamental > reality, mechanism requires the abandon of types, or, at the least, a > universal type, like the type of a universal machine when added to a typed > world. > > You allude to the Curry Howard isomorphism, which is very beautiful, but > do not extend so nicely to classical logic (as Krivine claims to have > succeeded, but I am not convinced). Nor Kleene realisability (despite my > very deep appreciation). It is normal, the notion of “other minds” makes no > sense in constructive mathematics, or philosophy. Brouwer mocked his > students who claim to love his course. He asked them, why do you love that > when it shows that you don’t exist … > > Bruno > > > > > - pt > > > > > > -- > > > -- You received this message because you are subscribed to the Google Groups "Everything List" group. To unsubscribe from this group and stop receiving emails from it, send an email to everything-list+unsubscr...@googlegroups.com. To post to this group, send email to email@example.com. Visit this group at https://groups.google.com/group/everything-list. For more options, visit https://groups.google.com/d/optout.