Skip to content

fix(notebook,#17357): Lean-03b -- attente d axiomes alignee sur la sortie committee (F1) #20116

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
myia-ai-01 merged 1 commit into from
Oct 11, 2026
+10 −5
Merged

fix(notebook,#17357): Lean-03b -- attente d axiomes alignee sur la sortie committee (F1) #20116

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
15 changes: 10 additions & 5 deletions MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-03b-Formalized-Formal-Logic-Lean-Python.ipynb
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -534,9 +534,14 @@
"### Le noyau répond : audit des axiomes\n",
"\n",
"Un théorème Lean ne dit pas seulement *quoi* est prouvé — `#print axioms`\n",
"liste **sur quoi** il repose. Pour des théorèmes d'évaluation sur un fragment\n",
"fini, l'attendu est l'axiome minimal : aucun `sorry`, aucune déclaration\n",
"non constructive importée en contrebande."
"liste **sur quoi** il repose. Sur ce fragment, l'attendu est : **aucun `sorry`**, et **aucun axiome\n",
"au-delà de ceux que la sémantique du pont exige**. La sémantique FFL est\n",
"`Prop`-valuée (`Valuation α := α → Prop`), donc décider `v 0` ou `v 1` passe\n",
"par `Classical.propDecidable` : `valuations_exhaustive` — et `peirce_valid`,\n",
"qui l'appelle — portent `Classical.choice`, en plus de `propext` et\n",
"`Quot.sound`, les axiomes du noyau. Le seul théorème purement syntaxique du\n",
"lot, `peirce_provable`, n'en utilise aucun. La lecture ci-dessous sépare les\n",
"deux régimes."
]
},
{
Expand Down Expand Up @@ -627,7 +632,7 @@
" `or_satisfiable`.\n",
"- **Au-delà de l'exécution** : `peirce_provable` donne la *dérivation* (versant\n",
" preuve), et `completeness!` (Tait) garantit que table et dérivation ne\n",
" peuvent pas diverger sur ce fragment.\n",
" peuvent pas diverger sur ce fragment.\n- **Le prix en axiomes** : la lecture ci-dessus se fait en deux régimes —\n `peirce_provable` ne dépend d'**aucun** axiome (dérivation purement\n syntaxique), tandis que `or_not_valid` et `or_satisfiable` ne portent que\n `propext` et `Quot.sound`, les axiomes du noyau, et que `peirce_valid`\n comme `valuations_exhaustive` y ajoutent `Classical.choice`. C'est le\n `by_cases` sur `v 0 : Prop` de `valuations_exhaustive` qui le requiert, et\n `peirce_valid` l'hérite par `rcases`. La validité sémantique se paie d'un\n axiome non constructif ; elle ne se paie pas d'un `sorry`.\n",
"\n",
"**Dette assumée** (même position que\n",
"[Tweety-5d](../Tweety/Tweety-05d-Stable-Synthesis-Lean-Python.ipynb)) : Tweety n'est pas\n",
Expand Down Expand Up @@ -893,4 +898,4 @@
},
"nbformat": 4,
"nbformat_minor": 5
}
}
Loading