On Jun 16, 11:07 am, Aatu Koskensilta <aatu.koskensi...@uta.fi> wrote: > Herman Jurjus <hjm...@hetnet.nl> writes: > > Also many classical mathematicians appreciate this as an example > > showing that the extensional notion 'Turing computable' is a slight > > distortion of the intuitive notion 'computable'. > > Possibly, but I don't think this is quite the right diagnosis. The issue > is more subtle. > > It's a well known phenomenon that many classically minded mathematicians > who have had little practice in constructive thinking are unwittingly > inconsistent in their reading of intuitionistic quantifiers. It's an > equally striking phenomenon that classically minded mathematicians in > certain contexts naturally adopt an intuitionistic reading of classical > quantifiers. In addition to the example provided by Virgil [...]
So is there a FORMAL constructivistic (or, more specifically, intuitionistic) theory in which we can formalize 'computable' so that it is faithful to the kind of "intensional" notion as held by Virgil?
(Classically, if f is recursive then it is computable, and, if we accept Turing's thesis we get the other direction so that we may formalize the notion of "computable" as recursive.)
