Introduction à la logique

Que connais-tu en maths non logique afin de faire le raccord?

Tout dépend. Par exemple, si tu es familier avec l'algèbre, le th de complétude, c'est une histoire d'idéaux maximaux).

L'indécidabilité provient d'une impossibilité dans le langage de mettre ensemble "programmation" et "convictions métaphysiques".

Par exemple, soit $A$ (donc un pointeur) qui dit "ma négation est évidente". A bien noter que la notion d'évidence est purement syntaxique et par définition simple. On suppose qu'on a mis dans les évidences les effacements et répétitions d’hypothèses.

Tu as alors :

$A = Evident(A\to Tout) = $
$Evident(A\to (A\to Tout)) = $
$Evident([ Evident(A\to Tout) ]\to (A\to Tout)) $

Si donc tu considères que ça doit faire partie des axiomes que tu utiliseras (qu'il est évident que ce qui est évident est vrai), alors $Evident(A\to Tout)$ est une phrase de la forme $Evident(Evident(X)\to X)$. tu as donc une preuve simple de $A\to Tout$ et ce que je viens de raconter se traduit en preuve de 3 lignes de $A$. Conclusion: $Tout$. Et c'est terminé.

Il existe donc une sorte de compromis très artisanal qui a été trouvé, qui esquive pudiquement ces noeuds (ou cycles).

Une autre remarque, dans la littérature tu trouves deux sens différents pour le mot décidable. Dans un cas il désigne le fait qu'une théorie prouver un énoncé ou preuve son contraire.
Dans l'autre le fait qu'un ensemble (d'entiers ou de mots) ne soit pas récursif.

Le fait qu'il existe des ensembles récursivement énumérables pas récursifs est dû, toujours, c'est le grand graal de la logique, au fait que:

$a:=\{x\mid $ il existe un preuve que $x\notin x\}$ est récursivement énumérable
et ne peut coincider avec $\{x\mid x\notin x\}$

Tu ne peux avoir au choix que $a\in a$ et une preuve que $a\notin a$ ou bien $a\notin a$ et pas de preuve que $a\notin a$.

C'est important en informatique car comme tu peux le deviner $\{x\mid x\in x\}$ est lui récursivement énumérable.

Précision, j'ai ici utilisé $\in$ comme voulant dire $(a\in b):= $ l'entier $a$ est une entrée qui fera s'arrêter le programme $b$ sur "oui".

Le tiers exclus est le fait que $X\mapsto non(X)$ est injective: comme

$$non(vrai) = non(A\ ou \ nonA)$$

croire à l'injectivité oblige à croire que $(A$ ou $ nonA)=vrai$

Pour le reste j'attends que tu précises. Attention, la logique se lit très doucement, sinon, la réaction est souvent "j'ai du mal à capter". Prends ton temps.

Si tu veux, en gros pour y entrer avec "passion" douce qui se maintient, il me semble qu'il faille u npeu alterner entre :

1/ Les infinis très "platoniciens" de la théorie des ensembles

2/ Le mécanismes à l'origine de la crise des fondements qui sont tous en rangs serrés derrière le "célèbre procédé diagonal"

3/ L'informatique THEORIQUE (qui donne des résultats amusants et parfois inattendus

4/ Les notions plus classiques de compacité et de complétude.

Quand tu sens la passion partir, tu repenses à l'argument que je t'ai donné "qu'on peut prouver qu'il existe des évidences fausses", et tu cherches la solution (il n'y en pas, donc ça maintient la niac).

Quand t'es apaisé, tu fais un petit tour du côté des "choses bien rédigées" (modèles, preuves classiques, etc)

J'ai oublié de te signaler correspondance de Curry Howard et élimination des coupures, qui sont des gros carrefours aussi.

La CCH étudie le profil des preuves comme garanties matérielles (en l'occurrence informatiques) et a permis d'aller "au coeur du processus de pensée scientifique"

L'élimination des coupures est une étude (je ne te parle pas d'histoire, car historiquement, c'est un peu faussé) de la parenté très forte entre le fait d'avoir prouvé $A\to B$ et $B\to C$, puis d'en déduire $A\to C$ et celle, plus profonde mais moins réflexe de considérer qu'en fait on a prouvé pluss, on a prouvé $[(A\to \to B]\to C$ (qui entraîne, certes, évidemment $A\to C$), mais qui a l'avantage de ne pas "jeter aux oubliettes" qu'on n'a pas seulement envoyé tous les éléments de $A$ dans $C$, mais aussi tout son bidual intégralement.

Itéré, ça permet de voir que la quasi-totalité des preuves de maths peuvent se transformer en : "les seules déductions autorisées sont les conjonctions de ce que vous avez supposé, et avec ça vous avez tout", et donc "in fine" ne servent à rien, et que tout le taf scientifique autour des preuves est dû au fait que les preuves sans coupures sont trop longues (et que donc on a "zippé")

C'est un joli chapitre de la logique. Il y a une forte satisfaction à virer des coupures et tomber sur un truisme alors qu'on avait cru faire oeuvre de subtilité.

Ce phénomène se reflète PAR AILLEURS dans le fait qu'on a tout un panel de preuves "faciles mais magiques" provenant de Zorn (donc de l'axiome du choix) et qu'on peut l'éliminer et tomber sur une sorte d'armada très univoque, mais longue et "effective". L'axiome du choix joue le rôle d'une coupure à bien des égards.