[FOM] an abyss?

[Antonino Drago]

I read Per Martin-Loef's paper: 
"The Hilbert-Brouwer controversy resolved?",
 in M. van Atten er al. (eds): One Hundred Years of Intuitionism (1907-2007), Birkhauser, 2007, 243-256. 
I think that the paper is a very informative review on best research results obtained in past decades on the FOM . 
It mainly deals with the crucial problem of an definitive appraisal, with respect to the foundations of both mathematics and logic, on Hilbert's program, i.e. the program which dominated this kind of research in the last century. 

In my opinion, its final notes leave a great perplexity in the reader. 
According the author, Hilbert's program failed two times; one time owing to Goedel's results; its revised or modified Hilbert's program, allowing more than finitist means, failed the second time in the 90's. On the other side, the original Brouwer's program was unsuccessfull. May this conclusion be called a reconciliation, after so unexperienced, collective effort of research? 

Worse, Martin-Loef sees as representing the present situation an "abyss" between the kind of mathematics relying on grosso modo constructive means and the kind of mathematics including the law of the excluded middle.

I woud like to see comments on this deceiving appraisal on the present situation, resulting from a century of hard and extraordinary research. Do FOMers agree, or not?  

Moreover, I ask: After that Susan Haak made use of the notion of radical variation in meaning of logical notions (Deviant Logic, pp. 11-14) and after J. Ferreiròs ("The road to modern Logic- An Interpretation", J. Symb. Logic, 7, 2001, 441-484) in order to intepret the history of the logic of 20th Century successfully applied a notion similar to Kuhn's paradigm, i.e. schemata (see p. 442), maybe 
the time has come to introduce the further notion suggested by the new historiography of science, i.e. the notion of "incommensurability" through what Martin-Loef calls "abyss"?  

In more technical terms: is the abyss  constituted by the law of the double negation, i.e. the wwell-known law separating, according to Dummett and Prawitz, classical logic and most kinds of non-classical logic?

In even more refined technical terms: is double negation (as failure) representable in Aritificial intelligence?
Thanks in advance
Best   regards
Antonino Drago
Univ. of Pisa
drago at unina.it
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20120619/d4d610cf/attachment.html>