The Experimental Effectiveness of Mathematical Proof

The aim of this paper is twofold. First, it is an attempt to give an answer to the famous essay of Eugene Wigner about the unreasonable effectiveness of mathematics in the natural sciences [25]. We will argue that mathematics are not only reasonably effective, but that they are also objectively effective in a sense that can be given a precise meaning. For thatâ€”and this is the second aim of this paperâ€”we shall reconsider some aspects of Popperâ€™s epistemology [23] in the light of recent advances of proof theory [8, 20], in order to clarify the interaction between pure mathematical reasoning (in the sense of a formal system) and the use of empirical hypotheses (in the sense of the natural sciences).

The technical contribution of this paper is the proof-theoretic analysis of the problem (already evoked in [23]) of the experimental modus tollens, that deals with the combination of a formal proof of the implication U â‡’ V with an experimental falsification of V to get an experimental falsification of U in the case where the formulÃ¦ U and V express empirical theories in a sense close to Popperâ€™s. We propose a practical solution to this problem based on Krivineâ€™s theory of classical realizability [20], and describe a simple procedure to extract from a formal proof of U â‡’ V (formalized in classical second-order arithmetic) and a falsifying instance of V a computer program that performs a finite sequence of tests on the empirical theory U until it finds (in finite time) a falsifying instance of U.

I thought I had already posted this, but apparently not.

Consider this paper the main gauntlet thrown down to those who insist that mathematical logic, the Curry-Howard Isomorphism, etc. might be fine for "algorithmic code" (as if there were any other kind) but is somehow inapplicable the moment a system interacts with the "real" or "outside" world (as if software weren't real).

**Update:** the author is Alexandre Miquel, and the citation is "Chapitre du livre Anachronismes logiques, Ã paraÃ®tre dans la collection Logique, Langage, Sciences, Philosophie, aux Publications de la Sorbonne. Ã‰d.: Myriam Quatrini et Samuel TronÃ§on, 2010."

## Recent comments

1 hour 44 min ago

1 hour 49 min ago

2 hours 5 min ago

14 hours 26 min ago

18 hours 53 min ago

20 hours 55 min ago

23 hours 43 min ago

1 day 5 min ago

1 day 49 min ago

1 day 1 hour ago