[FOM] Is current computability theory intuitionistic?

[Sam Sanders]

There is another (in my opinion fundamental) difference between the classical and constructive case:  

Computability theory and reverse mathematics are closely related: For instance, one has the nice "Big Five systems"
picture where each of these systems can be viewed in terms of a major computability-theoretic notion.  

This Big Five picture crucially depends on the distinction between on one hand "theorem of ordinary mathematics" (expressed in second-order arithmetic)
and "logical formula without mathematical meaning" on the other hand.  The first kind tends to 'cluster around the Big Five' as it were, whereas
the second kind are 'all over the place', i.e. the Big Five picture.   There are of course exceptions and border-line cases, depending on one's point of view.  
Nonetheless, there is a notion of "natural mathematical theorem" (see also unprovability theory), and we have a certain body of 
mathematics which came to be independent/not influenced by mathematical logic.   

However, intuitionistic mathematics has been developed much more in tandem with intuitionistic logic, and with an eye towards logic in general;
The rejection of excluded middle being the most obvious example.  For this reason, the line between "mathematical theorem" and "logical formula without mathematical meaning"
is much more blurred in intuitionistic (or constructive) math than in its classical counterpart.  (One could even make a case for the claim that intuitionistic
math and logic have to be developed in tandem).   Similar claims are valid for constructive math in general.  

Hence, by the very nature of constructive math and its connection to logic, one expects not the Big Five picture for constructive reverse mathematics (i.e. RM in a constructive base theory), 
but something more complicated.  The differences set forth by Carl also contribute to this complexity, but my main point is that the notion of "mathematical theorem" is much wider 
constructively:  A much higher threshold must be crossed before something does not count as "mathematical theorem" anymore.  

Best,

Sam

PS: The above constitutes no value judgement whatsoever.  

On 19 Jun 2013, at 16:48, Carl Mummert <mummertc at marshall.edu> wrote:

> On Tue, Jun 18, 2013 at 11:59 AM, Steve Stevenson <steve at clemson.edu> wrote:
> I didn't know to ask this question when I was learning and now I'm too
> old to read all the standard books. My recollection though is that
> computability texts use classical logic. Is that true? Does it matter?
> 
> It is certainly true. As with any other mathematical subject that is not intentionally studied constructively, classical logic is used throughout recursion theory. For example, 
> 
> * It would be routine in computability theory to assert that a given Turing machine, on a given input, which is proven to not run forever, must halt after some fixed number of steps. This form of Markov's principle is not universally accepted among constructivists. 
> 
> * The classical equivalence between sets and their characteristic functions is taken for granted. This equivalence is not valid constructively, because a set of natural numbers with a characteristic function must be decidable in the constructive sense (each number either is, or is not, a member of a given set), while several popular constructive systems do not prove that every set of natural numbers is decidable in the constructive sense.  
> 
> There are many more examples, but these highlight how early in the subject the constructive and classical theories will begin to diverge. Perhaps more importantly, the way in which the subjects diverge depends on the particular constructive theory being used (for example, HA^\omega and CZF differ in key respects).
> 
> I would suspect that someone must have studied constructive recursion theory, to see how much of the classical theory goes through, but I don't know of a good reference. There is certainly much more research on constructive type theory. 
> 
> I do not believe that the question whether the use of classical logic matters in recursion theory can be separated from the same question about mathematics in general. The usual arguments about classical and constructive mathematics will apply. 
> 
> - Carl 

-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20130621/28eb5d49/attachment.html>