Homo Topi face aux fondements des mathématiques et de la logique

Homo Topi

Au départ, je voulais répondre dans le fil de @arnaud_s mais mon commentaire s'est vite transformé en quelque chose de plus global, alors pour ne pas dérailler son fil, j'ouvre le mien. En tout cas, @arnaud_s sache que ton avis est évidemment le bienvenu ici, dis-moi si ce que je raconte touche un peu aux questionnements sous-jacents de ton fil, si j'ai pu t'aider à trouver des réponses à ces questionnements. J'en profite aussi pour adresser ce fil à n'importe quel lecteur étudiant (sachant que c'est surtout en L3 et en Master qu'on se prend la tête avec ces questions des fondements, d'expérience).

Quand j'étais en L3, je me suis intéressé de très près aux fondements des mathématiques. Au point de rater mon année. Je pense que j'étais à la recherche d'une manière de rendre les mathématiques, qui sont abstraites et formelles, "absolues". En gros, "puis-je faire une confiance absolue en les mathématiques ?" Spoiler : non.

En fait, c'est venu d'un défaut d'enseignement. En cours de topologie, on me demandait d'accepter que $\R$ est complet, sans que j'en aie eu de démonstration, la démonstration viendrait plus tard, dans un autre cours, peut-être. Et je me suis rendu compte que beaucoup de choses que j'avais "apprises", en fait, je les avais simplement "acceptées" et utilisées depuis. Le théorème de Pythagore. Je n'en connais aucune démonstration dont j'ai vérifié avec soin qu'elle est valable dans ZFC et non circulaire, je pense qu'il y en a sûrement mais je ne l'ai juste pas vérifié, donc je ne le "sais" pas. Bref, ce que ces réalisations ont provoqué en moi, c'était un profond manque de confiance en les mathématiques. J'ai eu besoin de tout reconstruire depuis le début. J'ai même commencé à me faire mon propre cours de théorie des ensembles et de tout refaire avec ça, j'ai encore ce document dans mes affaires (même s'il ferait bien d'être quasi-entièrement réécrit, mais bref).

Donc j'ai commencé par chercher les fondements des mathématiques. Et plus on cherche, plus on trouve, c'est un puits quasiment sans fond. J'ai fini par trouver les axiomes ZFC, et j'ai commencé à reconstruire les objets les plus fondamentaux des mathématiques que je connaissais avec. $\N$, le principe de récurrence, $\Z$, $\Q$, $\R$, $\C$, j'ai voulu répondre à des questions comme "d'où sort l'indéterminée $X$ des polynômes" et j'ai découvert le truc hyper rassurant que sont les structures algébriques libres et l'algèbre universelle (qui m'ont été expliqués par @Maxtimax qui m'est tout bonnement impossible de remercier suffisamment fort), et ça m'a donné un profond regain de confiance en les mathématiques.

Je me suis rendu compte que ZFC ne me satisfaisait tout de même pas. Pour deux raisons : de 1, le paradoxe de Russell (sous la forme : il n'existe pas d'ensemble de tous les ensembles), et de 2, les schémas d'axiomes. Attention : je ne déclare pas que ce sont des bonnes raisons, ni qu'elles sont profondément justifiées, mais, c'étaient mes raisons.

Pour Russell : je trouvais "impropre" qu'une théorie mathématique permette de concevoir l'existence d'objets dont tout ce qu'on sait, c'est qu'on ne sait pas ce que c'est. Alors j'ai fouillé un peu plus, et j'ai découvert la théorie des classes avec les axiomes NBG. Là, au moins, c'est clair : la classe de tous les ensembles, on sait ce que c'est (une classe propre), ouf. En plus, la théorie des classes me donnait un outil supplémentaire : dans la théorie des catégories, dont on est obligé de se servir quand on fait certaines choses en maths auxquelles j'ai voulu m'intéresser, beaucoup de catégories "importantes" sont des classes propres, donc des objets indéfinissables dans ZFC. Pour les schémas d'axiomes, je pense que ce qui me dérangeait c'était la non-finitude de l'axiomatique, et le fait de dire : pour chaque "formule" du "langage", il existe un axiome. C'est quoi le langage, c'est quoi une formule ? Au secours, on retombe dans l'incertain.

Je me suis rendu compte que les mathématiques que je fais utilisent un tas de symboles. Certains sont définis par ZFC, comme $\subseteq, \geqslant, +, \times, \circ$... et d'autres non. Alors que ZFC les utilise. Je pense à $\in$ et $=$ mais aussi aux symboles logiques présents déjà dans les axiomes de ZFC comme $\Longrightarrow$, $\wedge$ ou $\neg$. Donc j'ai eu besoin de définir ces symboles-là. Il y a plusieurs façons de faire, et justement, c'est ici qu'on commence à rentrer dans les difficultés de @arnaud_s qu'on a vu dans son fil.

Ce qu'il se passe, c'est que toute la théorie mathématique, qu'on la fonde sur ZFC ou sur autre chose, est une sur-couche avec autre chose en dessous. Je suis tombé sur le "calcul des propositions" qui définit les connecteurs logiques, le calcul des prédicats qui définit les quantificateurs, et là on a presque tout. Certains disent que $\in$ et $=$ sont les seuls symboles intrinsèques des mathématiques, personnellement je pense que $=$ se laisse définir à partir de $\in$ (axiome d'extensionnalité, il suffit de transformer le $\Longrightarrow$ en un $\Longleftrightarrow$) et que donc seul $\in$ est "intrinsèque".

Donc à ce stade, où est-ce que j'en suis : toutes les maths se font avec ZFC (ou équivalent), ZFC a besoin du calcul des propositions et du calcul des prédicats pour pouvoir être écrit, donc, il faut "fonder la logique" avant de "fonder les maths". Ben oui, sauf que, quand on cherche une "formalisation propre" de la logique, ça devient mathématique, d'où l'ouroboros logique que déplore @arnaud_s dans son fil. On trouve des histoires de théorie des langages, théorie des modèles, on ne sait plus qu'est-ce qui fonde quoi, donc tout s'écroule. On re-perd confiance en l'absolu du formel.

En fait, cette quête de l'absolu s'est pratiquement soldée par un échec pour moi. Je ne sais pas si "la logique est vraie" ni si "les mathématiques sont vraies". Mais j'ai quand même une manière d'être en paix avec moi-même sur la question si je peux faire confiance aux mathématiques. Je m'explique.

Il faut faire le constat suivant : la logique, et la science qu'on fait avec cette logique, c'est de la déduction. C'est faire $A \Longrightarrow B$. Peu importe comment on l'écrit, il faut une hypothèse et une règle de déduction pour obtenir une conclusion. Vous me direz ce que vous en pensez, mais pour moi, ce simple constat a été profondément libérateur. Pourquoi ? C'est très simple : il dit qu'il faut, tôt ou tard, accepter des axiomes si l'on veut pouvoir aboutir à des résutats logiques. Et qu'il faut aussi avoir des règles de déduction données.

Au sujet des axiomes : posons-nous un peu la question, les axiomes de ZFC ont-ils la moindre vérité ? Pour moi, la réponse est non. Il suffit de regarder l'axiome de l'infini par exemple, cet axiome est une traduction de l'échec des matheux face aux théorèmes de Gödel. L'existence des entiers naturels n'est pas démontrable proprement ? OK alors on admet leur existence, pouf, axiome de l'infini. Ces axiomes ont été introduits "parce qu'ils marchent", parce qu'ils nous permettent d'établir les résultats qu'on veut établir, résultats qui permettent au cerveau humain de comprendre les lois du monde dans lequel il vit. C'est ça leur seule légitimité : ils permettent au cerveau humain de concevoir des modèles mathématiques de la réalité telle que le cerveau humain la perçoit. Est-ce que ça a quoi que ce soit d'une vérité absolue, ça ? Je ne trouve pas.

Mais le cerveau humain, justement, parlons-en. Je disais qu'il nous faut des règles de déduction pour faire des déductions. Là aussi, il existe différentes formalisations des choses (coupures, système de Hilbert, déduction naturelle...) qui sont tous essentiellement équivalents. Il n'y en a aucun "plus vrai que les autres". La vérité c'est que, peu importe si nous savons construire un langage abstrait pour le modéliser ou non, notre cerveau fait des déductions avec des règles "naturelles" (imposées, littéralement, par la nature, par la chimie des réactions qui ont lieu dans le cerveau) et ce sont ces règes-là qui déterminent notre façon de percevoir le monde. Donc il n'y a pas besoin d'un système de logique absolu, d'un langage indépendant du fonctionnement humain, puisqu'il n'y aura jamais que des humains qui vont s'en servir. Il suffit alors "d'accepter" des axiomes logiques, d'accepter une formalisation écrite de ces axiomes, et de s'en servir. Sont-ils absolus ? Non, probablement pas, tout comme je ne sais pas si j'existe absolument ou si l'univers dans lequel je crois exister ne serait que l'imagination immatérielle d'un être extérieur.

J'ai donc accepté qu'il suffit d'accepter. Choisissons un langage logique qui semble correspondre au fonctionnement de notre cerveau. Choisissons sa syntaxe comme ça nous arrange. Choisissons le langage mathématique qui nous permet d'être sûrs de nous, choisissons les axiomes de notre théorie qui nous permette d'aboutir à des résultats qui ont l'air suffisamment cohérents. Si en faisant ça, on envoie des gens sur la Lune et on les ramène en vie, alors pour Homo Topi, c'est good enough. Même si on ne saura jamais si c'est effectivement vrai. Voilà comment j'ai pu reprendre confiance en les mathématiques après une crise profonde au beau milieu de mes études.

Mon concept des fondements :

1) Calcul des propositions : on introduit les symboles $\Longrightarrow$, $\wedge$, $\vee$, $\neg$, on introduit les constantes "vrai" et "faux", on axiomatise leur fonctionnement en se basant sur le fonctionnement naturel de la logique du cerveau humain, et après on déclare que faire de la logique, c'est utiliser ce qu'on a défini de la manière dont on l'a défini. C'est un outil, c'est l'utilisateur qui en définit l'utilité.

2) Calcul des prédicats et mathématiques : on introduit les symboles $\forall$, $\exists$, $\in$, on se donne des axiomes pour démarrer une théorie, et après on s'en sert en leur appliquant les règles de notre logique, cf le point 1).

3) A propos de la théorie des langages : je refuse d'y voir l'ouroboros logique de "il faut la théorie des ensembles pour faire de la logique". Pour moi, c'est plutôt, étant donné un langage logique, peut-on modéliser mathématiquement son fonctionnement ? Le but étant par exemple de "coder" ce langage physiquement pour qu'une machine puisse faire de la logique humaine par simple application des lois de la physique. La logique que j'utilise en maths, je lui donne une syntaxe formelle parce que c'est pratique, pas parce qu'un mathématicien me dit qu'il n'y a que comme ça qu'un système logique puisse avoir de la valeur. Et la syntaxe, c'est moi qui la choisis, selon ce qui m'arrange. Exactement comme les axiomes de cette logique (les règles de déduction). Il ne faut pas confondre formaliser, et fonder. Il faut fonder un jour, sans quoi on n'a rien. Mais si tout le monde est d'accord sur ces fondements, alors tout va bien, peu importe si l'un ou l'autre les formalise autrement que moi.

Bref. J'ai été très long, et je ne sais pas si j'ai été très clair, ou utile. Merci d'avoir lu.

Foys

Il n'y a pas besoin d'axiome de l'infini pour définir les nombres entiers dans ZF (sans infini). Les nombres entiers sont définis comme les ordinaux successeurs dont tous les éléments sont successeurs. Cependant l'axiome de l'infini sert à affirmer (c'est équivalent) qu'il existe un ensemble qui les contient tous. La négation de cet axiome (consistante avec ZF) entraîne que tous les ordinaux sont des entiers.

Médiat_Suprème

1, le paradoxe de Russell (sous la forme : il n'existe pas d'ensemble de tous les ensembles),
Il n'y a pas de paradoxe de Russell dans ZFC

2, les schémas d'axiomes. 
Quel problème peut bien poser un schéma d'axiomes ?

J'avais fait remarquer à arnaud_s qu'il cherchait un dictionnaire non pas alphabétique, mais dont chaque mot serait défini exclusivement à partir des précédents, je lui avais aussi parlé du trilemme de Münchhausen, je crois que ces remarques vous concernent aussi

Foys

Formaliser consiste à expliciter des fondements (sans quoi on ne sait pas de quoi on parle). fonder le jeu d'échec = donner ses règles (et non pas expliquer comment gagner ce qui est autre chose).

Homo Topi

@Foys : pour $\N$, je sais. Vu le public auquel je me suis adressé, je pense que je peux attendre qu'on comprenne ce que je voulais dire même si je me suis exprimé de manière imprécise. Quant à "formaliser consiste à expliciter des fondements", justement, tu entres dans l'ouroboros logique : comment écrire les règles de la logique si la logique sert à fonder la TDE mais qu'on veut s'imposer d'utiliser la TDE pour justifier la syntaxe du langage ? C'est pour ça que je parle du fonctionnement naturel du cerveau. Il y a une différence entre le concept et l'écriture du concept. Rien que quand on dit que la logique mathématique est bivalente (un énoncé a une valeur de vérité parmi vrai/faux et une seule) on sous-entend déjà le tiers exclu et la non-contradiction, pourtant on les réintroduit parmi les règles logiques formelles quand même.

@Médiat_Suprème tu chipotes aussi pour passer exprès à côté du truc. La formulation correcte est "il n'existe pas d'ensemble de tous les ensembles", cet énoncé est lié au paradoxe de Russell. Si le but de la TDE est de formaliser la notion de "collection d'objets", alors la collection de tous les ensembles est un truc indescriptible par les axiomes ZFC. Pourtant, c'est un objet qu'on peut concevoir, qu'on est même naturellement amené à observer quand on fait de la TDE. Quand au problème de la notion de schéma d'axiomes, j'ai dit ce qu'il y avait à en penser. "Attention : je ne déclare pas que ce sont des bonnes raisons, ni qu'elles sont profondément justifiées, mais, c'étaient mes raisons."

Je ne connaissais pas le trilemme de Münchhausen mais c'est extrêmement intéressant. Et ça justifie un peu mon procédé : tôt ou tard, on gagne à simplement admettre qu'il faut accepter de poser UNE base. Et que tout ce qu'on construit dépend de cette base. Et qu'il n'y aura jamais de base absolue.

Foys

@Homo Topi s'il y avait un cercle vicieux inévitable dans la définition des maths il n'existerait aucun logiciel d'assistanat de preuves en math (Lean, Coq, Mizar etc). Ces logiciels n'auraient aucune existence physique (s'ils avaient eu besoin au prélable de maths déjà fondées pour commencer à être écrits ce qui n'est pas le cas). Pourtant ils existent quand même. On pourrait dire de même de la récursivité en général. Pourquoi un programme informatique comme la définition courante de la factorielle (0! := 1 et pour tout n, (n+1)! := (n+1) * (n!)) peut exister et rendre des résultats à chaque appel?

Foys

Les mathématiciens et informaticiens ont vaincu au 20ième siècle ce prétendu "ouroboros" pour faire exister physiquement les ordinateurs.

Homo Topi

Je ne comprends pas de quoi tu parles, je pense que nous ne parlons pas de la même chose.

Définis-moi le langage logique nécessaire à écrire un axiome tel que l'axiome d'extensionnalité. Quelles bases logiques, syntaxiques, etc, sont nécessaires pour écrire cet axiome ?

Médiat_Suprème

Je reviens sur ce que vous dites du paradoxe de Russell dans ZFC : vous avez envie que l'ensemble de tous les ensembles existe

1. C'est une façon de ramener la théorie naïve dans ZFC, ce qui est contre nature
2. C'est peut-être une envie liée au platonisme, et là, je n'ai pas d'argument, à part vous faire remarquer que c'est de la philosophie et pas des mathématiques
3. Sinon, appelons cela des chibrückes, et honnêtement, je ne vois pas pourquoi le chibrückes de tous les chibrückes devrait exister
4. Pourquoi ne pas parler du paradoxe des entiers, puisque l'entier plus grand que tous les entiers n'existe pas

Homo Topi

@Médiat_Suprème hors-sujet total.

Je dis que dans la théorie des classes, la collection de tous les ensemble est une classe, donc un objet de la théorie. Alors que dans ZFC, ce n'est pas le cas : les objets de la théorie sont les ensembles, et il n'existe pas d'ensemble de tous les ensembles. C'est tout ce que je disais (je n'argumente pas à propos de l'utilité de la classe de tous les ensembles).

Médiat_Suprème

Et alors ?

Je ne vois même pas de bonne raison d'en être chagriné

Homo Topi

Et justement, j'ai dit et répété qu'il n'y en avait pas de bonne raison. J'ai dit qu'à l'époque c'était un truc qui me dérangeait et m'a incité à creuser davantage.

Foys

1°) Un objet (texte) est une variable si:

(i)c'est $o$

(ii)ou bien c'est $\cdot$ suivi à sa droite d'une variable.

2°) Un objet est une formule si:

(i)C'est $\in$ immédiatement suivi de deux variables à sa droite

(ii)C'est $\Box$ suivi de deux formules immédiatement à sa droite, $\Box$ désignant l'un des symboles suivants: $\Rightarrow, \Leftrightarrow, \vee, \wedge$.

(iii) C'est $\neg$ suivi immédiatement d'une formule à sa droite

(iv) C'est $\mathbf Q$ suivi immédiatement d'une variable à sa droite puis d'une formule, $\mathbf Q$ désignant l'un des deux symboles suivants: $\forall, \exists$

On appelle "axiome d'extensionnalité" la chose suivante:

$\forall o \forall \cdot o \Rightarrow \forall \cdot \cdot o \Leftrightarrow \in \cdot \cdot oo \in \cdot \cdot o \cdot o \forall \cdot \cdot o \Leftrightarrow \in o \cdot \cdot o \in \cdot o \cdot \cdot o$

3°) L'axiome d'extensionnalité est-il une formule? Oui, en effet:

(i). $o$ est une variable d'après 1°) (i).

(ii) $\cdot o$ est une variable d'après 3°) (i) et 1°) (ii)

(iii) $\cdot \cdot o$ est une variable d'après 3°) (ii) et 1°) (ii)

(iv) $\in \cdot \cdot o o$, $\in \cdot \cdot o \cdot o$, $\in o \cdot \cdot o$ et $\in \cdot o \cdot \cdot o$ sont des formules d'après 3°) (i), 3°) (ii), 3°) (iii) et 2°) (i)

(v) $\Leftrightarrow \in \cdot \cdot o o \in \cdot \cdot o \cdot o$ et $\Leftrightarrow \in o \cdot \cdot o\in \cdot o \cdot \cdot o$ sont des formules d'après 3°)(iv) et  2°) (ii)

(vi) $\forall \cdot \cdot o \Leftrightarrow \in \cdot \cdot o o \in \cdot \cdot o \cdot o$ et $\forall \cdot \cdot o \Leftrightarrow \in o \cdot \cdot o\in \cdot o \cdot \cdot o$ sont des formules d'après 3°) (v) et 2°) (iv)

(vii) $ \Rightarrow \forall \cdot \cdot o \Leftrightarrow \in \cdot \cdot oo \in \cdot \cdot o \cdot o \forall \cdot \cdot o \Leftrightarrow \in o \cdot \cdot o \in \cdot o \cdot \cdot o$ est une formule d'après 3°) (vi) et 2°) (ii)

(viii) $\forall \cdot o \Rightarrow \forall \cdot \cdot o \Leftrightarrow \in \cdot \cdot oo \in \cdot \cdot o \cdot o \forall \cdot \cdot o \Leftrightarrow \in o \cdot \cdot o \in \cdot o \cdot \cdot o$ est une formule d'après 3°) (vii) et 2°) (iv)

(ix) $\forall o \forall \cdot o \Rightarrow \forall \cdot \cdot o \Leftrightarrow \in \cdot \cdot oo \in \cdot \cdot o \cdot o \forall \cdot \cdot o \Leftrightarrow \in o \cdot \cdot o \in \cdot o \cdot \cdot o$ est une formule d'après 3°) (viii) et 2°) (iv) ce qui est l'affirmation visée.

Homo Topi

Tu ne définis pas qui est $o$ donc dès la première ligne je ne peux pas comprendre. Tu ne définis pas non plus $\cdot$ ni aucun des symboles que tu utilises. Définis tous les symboles que tu utilises. Je suis curieux de voir comment tu fais. Et je n'essaie pas de te piéger, j'essaie d'apprendre/de comprendre.

Thierry Poma

@Homo Topi : bonsoir. En ce moment, quand j'ai le temps, j'étudie le livre de Charles Ehresmann (livre intitulé Catégories et structures), dont son épouse Andrée Ehresmann, née Bastiani, a rédigé un livre de théorie des ensembles où les concepts de pré-univers et d'univers y sont détaillés.

Charles Ehresmann utilise la théorie de vN-B-G, mais il souligne dans son introduction, que l'on pourrait élaborer sa théorie des catégories avec des univers. Le cadre dans lequel l'on devrait se placer est donc ZFC+U (adjonction de l'axiome des univers ou de l'axiome équivalent des cardinaux fortement inaccessibles), et pas seulement ZFC. Potentiellement, je peux trouver un univers dans lequel je peux fourguer les ensembles que je veux ; j'ai toujours la possibilité d'aller plus loin en utilisant un autre univers, et ainsi de suite.

Foys

Ce sont juste des symboles choisis arbitrairement. C'est comme si tu disais que tu ne comprends pas les textes en français parce que les symboles 'a,b,c,d,...,x,y,z' ne veulent rien dire en soi. Les règles du jeu et ses symboles distinctifs sont arbitraires, les conséquences de ces règles, non (penser au jeu d'échecs).

Homo Topi

@Thierry Poma techniquement, c'est déjà ce que je fais avec NBG quand je mentionne le "il n'existe pas d'ensemble de tous les ensembles". Va savoir pourquoi, mon cerveau a besoin d'un type de grosse boîte qui peut contenir toutes les boîtes de type "ensemble", mais l'idée que les grosses boîtes ne puissent pas être mises dans une maxi-boîte encore plus grosse dans la même théorie, ça il s'en fout. Mais oui, il serait plus cohérent d'autoriser une infinisation de la hiérarchie des boîtes, tout en gardant à l'esprit que la quasi-totalité des maths se font dans les 2-3 types de boîte les plus petits.

@Foys on est d'accord que les symboles sont arbitraires, c'est leur comportement qui ne l'est pas. Tu dois poser les axiomes auxquels tes symboles $o$ etc. obéissent pour que ton exposé ci-dessus puisse avoir la moindre signification, c'est ça que j'attends de voir.

Foys

Le reste se trouve dans n'importe quel bouquin de théorie de la démonstration, l'axiome d'extensionnalité n'étant que le premier d'entre eux...

Une formule $X$ est un théorème si $X$ est un axiome ou bien s'il existe une formule $Y$ tels que $Y$ et $\Rightarrow YX$ sont des théorèmes. Cette définition n'est pas plus circulaire que celle de formule et de variable livrées plus haut.

Les axiomes sont des axiomes logiques dans le style de ceux du lien ci-après: https://les-mathematiques.net/vanilla/index.php?p=/discussion/2296806/quest-ce-quune-demonstration#latest

(il faudrait rajouter des axiomes fixant le comportement des connecteurs autres que $\Rightarrow$; ou les défnir comme des abréviations mais ça ne pose pas de problèmes) ainsi que des axiomes spécifiques de théorie des ensembles.

Homo Topi

Tout ça, je suis d'accord. Il faut fixer des axiomes, je n'ai jamais dit autre chose. On va se noyer à force de ne pas avoir de problème précis.

Je veux savoir quels sont les axiomes de la logique mathématique, quelles sont les règles de déduction de la logique mathématique. Et je pose la question : comment écrit-on formellement ces axiomes et ces règles ? Comment rédige-t-on une démonstration formelle obtenue en appliquant ces axiomes et ces règles ?

Foys

Tu devrais prendre un livre de théorie de la démonstration où tout est détaillé (c'est un peu long à faire).

[Utilisateur supprimé]

Les schémas d'axiomes sont des théories du premier ordre qui peuvent s'exprimer par des formules du second ordre. Les maths précédant la logique formelle (j'essaie de ne pas prononcer "naïf set theory") sont très semblable à une théorie du second ordre, donc la notion de schéma d'axiomes n'y est pas présente : regardez bien, le schéma d'axiomes de compréhension n'est qu'un axiome en théorie naïve (j'ai essayé de ne pas prononcer ce mot, mais bon..).

Homo Topi

A l'époque, j'ai essayé de tout m'apprendre avec ça. Je vais poser quelques questions au lieu de refaire ensemble ici tout un cours de logique.

Si je prends par exemple le connecteur logique "et" : on peut décider de le modéliser par $\wedge$. Le $\wedge$ sert à former des nouvelles propositions : si $A$ et $B$ sont deux propositions, alors $A \wedge B$ est une nouvelle proposition. La phrase que je viens d'écrire en gras, c'est quoi ? Un axiome ? 

Thierry Poma

@Homo Topi : voici une autre alternative.

Homo Topi

@cohomologies bienvenue dans mon fil ! Je me souviens vaguement de premier/second ordre, je pense redevenir fou avec ce fil, à voir si j'entraîne quelqu'un avec moi.

Foys

À une époque j'avais implémenté la logique du premier ordre classique avec nand et forall ici : https://pastebin.com/KfCCrVhd

Ce n'est qu'un exemple parmi les centaines de choses que l'on pourrait faire (nand est essentiellement une mauvaise idée à cause de la taille des formules que l'on obtient).

Homo Topi

@Thierry Poma tu connais la "option paralysis" ? Comme au restaurant ? Je subis un peu ça avec ZFC, ZFC étendu, NBG, catégories, autre axiomatisation des catégories, etc. Je pense me concentrer sur la logique pure vu la tournure que prend ce fil, sinon je vais péter un câble

raoul.S

Homo Topi a dit :

Je veux savoir quels sont les axiomes de la logique mathématique, quelles sont les règles de déduction de la logique mathématique....

Il y a ce bouquin par exemple qui répond à tout ça.

Voici un extrait pour toi :  

[Utilisateur supprimé]

@raoul.S entend que @Homo Topi croule sous les différentes alternatives et il rajoute le coup fatal 😆
La théorie de la démonstration et le livre de David-Nour 😆
Là @Homo Topi va être KO.

Homo Topi

En fait je pense ne pas avoir clairement expliqué ce qui me "pose problème" (en vrai, je n'ai pas de problème, je chipote). Tout le monde me balance des extraits de cours, ce sont des choses que je sais en principe déjà, vu sous un formalisme ou un autre.

J'ai du mal à formuler des questions précises sur les choses que je ne trouve éventuellement pas claires dans les fondations de la logique. Je vais y réfléchir.

[Utilisateur supprimé]

Je te conseille de prendre le Cori-Lascar, lit bien la préface en entier ainsi que le contenu des deux tomes.

Thierry Poma

@Homo Topi : si tu veux acquérir le livre cité par @raoul.S , autant pointer le bon lien, voire attendre ceci.

Homo Topi

Je ne pense pas que de me conseiller un 35ème livre sur le sujet présente un réel intérêt, je n'ai ni le budget, ni le temps, ni l'énergie de lire chaque bouquin qu'on m'ait conseillé.

Laissez-moi juste filtrer un peu ce que j'ai dans la tête. Je poserai une question précise.

Homo Topi

Voilà déjà une première problématique.

En calcul des propositions, on utilise entre autres le symbole $\wedge$ (pour "et"). $\wedge$ tout seul ne veut rien dire, il a besoin d'une variable (propositionnelle) à gauche de lui et une autre à droite. Si $A$ et $B$ sont des propositions (des énoncés avec une unique valeur de vérité), alors $A \wedge B$ est une proposition : la théorie du calcul des propositions doit contenir des axiomes permettant de déterminer la valeur de vérité de $A \wedge B$ en fonction de celles de $A$ et de $B$. 

Première question : comment rédige-t-on formellement ces axiomes ? Dans quel langage écrit-on le calcul des propositions ?

Foys

Homo Topi a dit :

Si 𝐴 et 𝐵 sont des propositions (des énoncés avec une unique valeur de vérité),

Ce sont des propos de ce type qui me font penser que tu devrais tout reprendre depuis le début et consulter les sources proposées en allant à ton rythme. Les phrases/propositions/etc n'ont pas intrinsèquement de "valeur de vérité". Ce genre de considération est ajouté indépendamment. Les objets manipulés sont syntaxiques avant toute chose.

Homo Topi

Je ne comprends pas l'intérêt de traiter des propositions sans valeur de vérité. J'ai vraiment besoin qu'on m'explique ça avant de me lancer dans la lecture de 150 bouquins. Faire de l'assemblage syntaxique vide de sens ne m'a l'air d'aucune utilité.

[Utilisateur supprimé]

$\wedge$ ne signifie absolument rien, c'est juste un symbole noté de cette façon, on aurait pû le noter d'une autre façon. L'ensemble des formules du calcul des propositions (les variables propositionelles étant fixées) est une structure libre sur le langages des connecteurs (affectés de leurs arités), une distribution de valeur de vérité est une morphisme de l'ensemble des formules propositionelles muni de sa structure vers $\{0;1\}$ muni de la structure qui convient.
Il n'y a pas "d'axiomes de logique" tel que tu l'entends, la logique c'est juste des maths.

JLapin

Homo Topi a dit :

Première question : comment rédige-t-on formellement ces axiomes ? Dans quel langage écrit-on le calcul des propositions ?

Tu as quelques réponses à tes questions dans les sceenshots de Raoul.S

Homo Topi

cohomologies a dit : https://les-mathematiques.net/vanilla/index.php?p=/discussion/comment/2392216/#Comment_2392216

[Inutile de recopier l’avant dernier message. Un lien suffit. AD]

C'est justement des réponses de ce type qui ne peuvent avoir aucun sens pour moi (ce que j'appelle ouroboros logique). Définis-moi "structure libre sur le langage des connecteurs" ou "morphisme" ou "arité" sans utiliser ZFC qui utilise $\wedge$ dans la définition de ses axiomes. À mon sens tu utilises des objets qui ont besoin du calcul des propositions pour être définissables pour définir le calcul des propositions.

Foys

@Homo Topi la phrase "dans le groupe $G$, on a $aba^{-1}b^{-1} \neq 1_G$" n'est ni vraie ni fausse. Pourquoi? Parce que $G$ pourrait désigner $\mathfrak S_3$, $a=(1,2)$ et $b:=(1,2,3)$ auquel cas elle serait vraie. Ou bien $G:=\Z$, $a:=b:=0$ auquel cas elle serait fausse.

Les énoncés mathématiques ne sont susceptibles d'être vrais et faux qu'après fixation des valeurs des lettres et symboles apparaissant dedans et introduction de  règles de manipulation supplémentaires; on ne peut parler de sens des énoncés avant ça. Par contre une démonstration ne fait JAMAIS référence à ce sens des formules: il s'agit d'un objet syntaxique. C'est vital de comprendre ça déjà. Sinon tes questions resteront sans réponse, faute de vouloir écouter les réponses.

[Utilisateur supprimé]

@Homo Topi tu te lances dans le formel beaucoup trop tôt !
Le formel se développe avec les maths et non l'inverse. Si tu regardes le Cori-Lascar, tu vois qu'on développe la théorie formelle des ensembles en utilisant les maths, on ne fait pas l'inverse.

Médiat_Suprème

Münchhausen quand tu nous tiens !

Foys

Il n'y a pas vraiment de Munchaüsen ici sauf pour ceux qui veulent à tout prix voir le baron se sortir de l'eau. Il est totalement assumé que les symboles logiques employés sont non définis.

Médiat_Suprème

Ben non, justement, Homo Topi ne semble pas l'assumer.

Homo Topi

Je trouve assez insultant qu'on insinue que je refuse d'écouter ou quoi que ce soit de ce genre.

Je trouve étrange que vous trouvez tous entièrement normal que le langage logique avec les symboles serait de la syntaxe pure sans aucun sens et que ce sont les mathématiques qui donnent du sens aux choses. Je n'ai jamais rien lu de ce genre, et croyez-moi, j'ai passé du temps à chercher ces choses-là à l'époque. J'ai beaucoup de mal à comprendre comment tout ça est censé fonctionner...

[Utilisateur supprimé]

J'abandonne, je bosse sur un truc en algèbre en ce moment et j'ai pris du retard. @Foys et @Thierry Poma et @Médiat_Suprème sont compétents et de bon conseil. Bon courage à tous.

Médiat_Suprème

Je trouve assez insultant que vous parliez de hors sujet quand on répond précisément à vos questions !

Homo Topi

Je ne suis pas d'accord, je n'ai pas beaucoup plus de réponses qu'avant, seulement plus de questions. Si je prends le propos de @Foys par exemple :

Foys a dit :

@Homo Topi la phrase "dans le groupe $G$, on a $aba^{-1}b^{-1} \neq 1_G$" n'est ni vraie ni fausse. Pourquoi? Parce que $G$ pourrait désigner $\mathfrak S_3$, $a=(1,2)$ et $b:=(1,2,3)$ auquel cas elle serait vraie. Ou bien $G:=\Z$, $a:=b:=0$ auquel cas elle serait fausse.

Les énoncés mathématiques ne sont susceptibles d'être vrais et faux qu'après fixation des valeurs des lettres et symboles apparaissant dedans et introduction de  règles de manipulation supplémentaires; on ne peut parler de sens des énoncés avant ça. Par contre une démonstration ne fait JAMAIS référence à ce sens des formules: il s'agit d'un objet syntaxique. C'est vital de comprendre ça déjà. Sinon tes questions resteront sans réponse, faute de vouloir écouter les réponses.

Pour moi, ça a très peu de sens. La "phrase" "dans le groupe $G$, on a $aba^{-1}b^{-1}\neq 1_G$" n'est pas un énoncé mathématique correctement formulé. Du moins, sans plus de contexte. Il faudrait soit quantifier les lettres $G$, $a$,$b$, soit les avoir définies au préalable pour en faire des "constantes locales". Je ne comprends pas du tout cette idée de manipuler des énoncés qui n'ont pas de valeur de vérité précisée, je ne vois pas du tout comment on est censé concevoir ça.

Pour moi, une démonstration dans son sens le plus épuré, c'est un assemblage de déductions de "je sais $A$ et $A \Longrightarrow B$, donc je sais $B$", mais ça ça ne peut avoir aucun sens si $A$ et $B$ n'ont pas des valeurs de vérité, donc je ne comprends pas comment on est censé faire une démonstration. Et pourtant, j'en ai fait quelques-unes dans ma vie, donc, il va falloir qu'on m'explique ce qu'il se passe ici.

JLapin

C'est ça que tu cherches je crois.

https://fr.wikipedia.org/wiki/Déduction_naturelle

Homo Topi

Non, ça je connais déjà. J'ai mentionné le modus ponens, c'est bien une preuve que j'ai déjà vu ça.

Mais justement, peu importe où je regarde, je trouve qu'une "proposition" EST un énoncé qui a une unique valeur de vérité. Le calcul des propositions, comme moi je le connais, c'est :

1) les connecteurs logiques et comment les utiliser (syntaxe) pour fabriquer des nouvelles propositions, par exemple fabriquer $A \wedge B$ à partir de deux variables propositionnelles $A$ et $B$

2) les axiomes régissant ces connecteurs logiques pour déterminer, en fonction des valeurs de vérité des variables propositionnelles qui la constituent, la valeur de vérité d'une proposition plus complexe. Par exemple : si $A$ est une proposition vraie et $B$ est une proposition fausse, alors $A \wedge B$ est une proposition fausse. Pour moi ça c'est un axiome, on peut résumer ces axiomes dans des tables de vérité si l'on veut.

Mais à aucun moment on oublie la valeur de vérité ici.

Une démonstration, après, oui c'est peut-être autre chose. J'ai du mal à dissocier le modus ponens (de $A$ et $A \Rightarrow B$, je déduis $B$) et $[A \wedge (A \Rightarrow B )] \Rightarrow B$. Je pense que c'est surtout ça que j'ai besoin de comprendre.

JLapin

C'est ça alors qui t'intéresse ?

https://fr.wikipedia.org/wiki/Calcul_des_prédicats

[Utilisateur supprimé]

Sans vouloir être méchant, j'ai bien peur que tout le monde ne perde son temps en répondant à @Homo Topi, c'est un exercice en futilité, comme parler à un aveugle avec le langage des signes. La meilleure volonté du monde n'y changera rien.