C'est bien ce qui me semblait. Sauf qu'en fait, non, pas du tout. Au contraire.
On a plutôt (en restant dans la caricature, je ne veux pas d'ennuis avec les matheux) :
Logique classique > mathématiques classiques du XIXe, théorie des ensembles, preuves sur papier et tableau noir. Les maths des physiciens.
Logique intuitionniste / théorie des types de Martin-Löf > programmation, preuves formelles assistées par ordinateur. Les maths des informaticiens.
Et d'après le texte que tu as donné, la logique "tiers inclus" ressemble beaucoup à une ébauche de la théorie des types. Y compris la hiérarchie d'univers pour éviter l'indécidabilité de Gödel.
La théorie des types, c'est la base de toute une branche de l'informatique théorique, et notamment de l'école française des preuves formelles (OCaml, Coq).
L'objectif de cette branche de recherche, c'est de formaliser toutes les mathématiques en rendant les définitions, théorèmes et démonstrations intelligibles par les ordinateurs. Ceci à fin d'automatiser la vérification des démonstrations (les mathématiciens sont des humains faillibles, l'expérience montre qu'ils n'ont pas une rigueur suffisante pour vérifier des démonstrations compliquées), voire de faciliter ou carrément d'automatiser l'écriture de démonstrations.
S'il y avait une conspiration pour remplacer les mathématiciens par des ordinateurs, alors la théorie des types en serait le fer de lance.
Le postulat de base en logique intuitionniste et en théorie des types, c'est qu'il n'y a pas l'axiome du tiers exclu (ni l'axiome du choix). Ça nous prive de certains modes de raisonnements comme la démonstration par l'absurde. En contrepartie, ça permet une logique constructive : si je sais prouver la propriété A=>B (propriété A implique propriété B), alors je sais écrire un programme qui prend un élément de A en entrée et renvoie un élément de B. Du coup, écrire une démonstration de A=>B, c'est équivalent à programmer une fonction de type A->B.
Donc ta théorie était que les machines ne peuvent pas penser comme les humains parce que les machines pensent avec le tiers exclus et pas les humains ?
Dommage, c'est
exactement le contraire. C'est une vision des raisonnements mathématiques (ou de la pensée en général si on n'a pas peur des généralisations hasardeuses) comme une activité purement calculatoire faisable par une machine qui a mené à développer des logiques sans axiome du tiers exclu. Une approche d'ailleurs controversé par les formalistes à l'époque, qui défendaient les principes du raisonnement "humain" d'Aristote, dont le tiers exclu :
https://en.wikipedia.org/wiki/Brouwe...rt_controversy
Mais ça c'est de la philo.