Almost All Classical Theorems Are Intuitionistic
RAIRO. Theoretical Informatics and Applications, Tome 56 (2022), article no. 9

Canonical expressions represent the implicative propositions (i.e., the propositions with only implications) up-to renaming of variables. Using a Monte-Carlo approach, we explore the model of canonical expressions in order to confirm the paradox that says that asymptotically almost all classical theorems are intuitionistic. Actually we found that more than 96.6% of classical theorems are intuitionistic among propositions of size 100.

Reçu le :
Accepté le :
Première publication :
Publié le :
DOI : 10.1051/ita/2022009
Classification : 11B73, 03F55, 06E30, 05-04, 05-08
Keywords: Intuitionistic logic, classical logic, combinatorics, asymptotic, random generation, Bell number, Catalan number, Monte-Carlo method 
@article{ITA_2022__56_1_A9_0,
     author = {Lescanne, Pierre},
     title = {Almost {All} {Classical} {Theorems} {Are} {Intuitionistic}},
     journal = {RAIRO. Theoretical Informatics and Applications},
     year = {2022},
     publisher = {EDP-Sciences},
     volume = {56},
     doi = {10.1051/ita/2022009},
     mrnumber = {4523320},
     zbl = {07644261},
     language = {en},
     url = {https://www.numdam.org/articles/10.1051/ita/2022009/}
}
TY  - JOUR
AU  - Lescanne, Pierre
TI  - Almost All Classical Theorems Are Intuitionistic
JO  - RAIRO. Theoretical Informatics and Applications
PY  - 2022
VL  - 56
PB  - EDP-Sciences
UR  - https://www.numdam.org/articles/10.1051/ita/2022009/
DO  - 10.1051/ita/2022009
LA  - en
ID  - ITA_2022__56_1_A9_0
ER  - 
%0 Journal Article
%A Lescanne, Pierre
%T Almost All Classical Theorems Are Intuitionistic
%J RAIRO. Theoretical Informatics and Applications
%D 2022
%V 56
%I EDP-Sciences
%U https://www.numdam.org/articles/10.1051/ita/2022009/
%R 10.1051/ita/2022009
%G en
%F ITA_2022__56_1_A9_0
Lescanne, Pierre. Almost All Classical Theorems Are Intuitionistic. RAIRO. Theoretical Informatics and Applications, Tome 56 (2022), article no. 9. doi: 10.1051/ita/2022009

[1] H. P. Barendregt, W. Dekkers and R. Statman, Lambda Calculus with Types. Perspectives in Logic. Cambridge University Press (2013). | MR | Zbl

[2] A. Biere, M. J. H. Heule, H. Van Maaren and T. Walsh (Eds.), Handbook of satisfiability. Vol. 185 of Frontiers in Artificial Intelligence and Applications. IOS Press (2009). | Zbl

[3] C. Bright, J. Gerhard, I. S. Kotsireas and V. Ganesh, Effective problem solving using SAT solvers, in edited by J. Gerhard and I. S. Kotsireas Maple in Mathematics Education and Research - Third Maple Conference, MC 2019, Waterloo, Ontario, Canada, October 15-17, 2019, Proceedings, Vol. 1125 of Communications in Computer and Information Science (Springer 2019) 205–219.

[4] S. A. Cook, The complexity of theorem-proving procedures. in Proceedings of the 3rd Annual ACM Symposium on Theory of Computing, May 3-5, 1971, Shaker Heights, Ohio, USA, edited by M. A. Harrison, R. B. Banerji and J. D. Ullman. ACM (1971) 151–158. | Zbl | DOI

[5] P. Flajolet and R. Sedgewick, Analytic Combinatorics. Cambridge University Press (2008). | MR | Zbl

[6] H. Fournier, et al., Classical and intuitionistic logic are asymptotically identical. edited by Jacques Duparc and Thomas A. Henzinger, CSL, Vol. 4646 of Lecture Notes in Computer Science. Springer, (2007) 177–193. | MR | Zbl | DOI

[7] A. Genitrini. Erratum for the paper Intuitionistic vs Classical Tautologies, Quantitative Comparisons. Personal communication, April 2021.

[8] A. Genitrini, J. Kozik and M. Zaionc. Intuitionistic vs. classical tautologies, quantitative comparison, in Types for Proofs and Programs, International Conference, TYPES 2007, Cividale del Friuli, Italy, May 2-5, 2007, Revised Selected Papers, edited by M. Miculan, I. Scagnetto and F. Honsell. Vol. 4941 of Lecture Notes in Computer Science. Springer (2007) 100–109. | MR | Zbl

[9] G. Gentzen. Untersuchungen uber das logische schließen. J. Math. Zeitsch. 39 (1934) 176–210. | MR | JFM | Zbl | DOI

[10] D. E. Knuth. The art of computer programming, Vol. 4 of Fascicle 3: Generating All Combinations and Partitions. Addison-Wesley Publishing Company (2005). | MR

[11] D. E. Knuth, The art of computer programming, Vol. 4 of Fascicle 4: Generating All Trees, History of Combinatorial Generation. Addison-Wesley Publishing Company (2006). | MR

[12] S. Mimram. PROGRAM = PROOF. Independently published (2020). URL: https://www.amazon.fr/dp/B08C97TD9G/.

[13] J.-L. Rémy. Un procédé itératif de dénombrement d’arbres binaires et son application à leur génération aléatoire. RAIRO Theor. Informatics Appl. 19 (1985) 179–195. | MR | Zbl | Numdam

[14] N. J. A. Sloane, The on-line encyclopedia of integer sequences. Published electronically at https://oeis.org/ (2021). | MR

[15] A. J. Stam, Generation of a random partition of a finite set by an urn model. J. Comb. Theory, Ser. A 35 (1983) 231–240. | MR | Zbl | DOI

[16] P. Tarau, A hiking trip through the orders of magnitude: deriving efficient generators for closed simply-typed lambda terms and normal forms, in Logic-Based Program Synthesis and Transformation - 26th International Symposium, LOPSTR 2016, Edinburgh, UK, September 6-8, edited by 2016, Revised Selected Papers, M. V. Hermenegildo and P. López-García, Vol. 10184 of Lecture Notes in Computer Science. Springer (2016) 240–255. | MR | Zbl

[17] P. Tarau and V. De Paiva, Deriving theorems in implicational linear logic, declaratively. Proceedings 36th International Conference on Logic Programming (Technical Communications), ICLP Technical Communications 2020, (Technical Communications) UNICAL, Rende (CS), Italy, 18-24th September 2020, edited by in F. Ricca, et al. Vol. 325 of EPTCS (2020) 110–123. | MR | Zbl

[18] The Sage Developers, SageMath, the Sage Mathematics Software System (Version 7.4), 206. https://www.sagemath.org.

Cité par Sources :