From b2e9266b06de41e1dcd329da624806e99bdc61bf Mon Sep 17 00:00:00 2001
From: "David A. Madore" <david+git@madore.org>
Date: Mon, 19 Jan 2026 12:44:01 +0100
Subject: A few clarifications on the syllabus.

---
 programme-inf110.tex | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

(limited to 'programme-inf110.tex')

diff --git a/programme-inf110.tex b/programme-inf110.tex
index 85ea37f..ff5bb1c 100644
--- a/programme-inf110.tex
+++ b/programme-inf110.tex
@@ -98,11 +98,11 @@ Git: \input{vcline.tex}
 \item \textbf{Arithmétique du premier ordre :} les axiomes de Peano ;
   l'idée générale que Curry-Howard sur l'arithmétique de Heyting
   permet d'extraire des algorithmes des preuves ; le fait qu'il est
-  possible formaliser $\varphi_e(i){\downarrow}$ en arithmétique de
-  Heyting/Peano ; le fait que vérifier si une preuve est valable est
-  décidable, mais que savoir si un énoncé est un théorème est
-  seulement semi-décidable ; l'énoncé du théorème de Gödel et l'idée
-  de sa démonstration.
+  possible de formaliser $\varphi_e(i){\downarrow}$ en arithmétique de
+  Heyting/Peano (sans détails) ; le fait que vérifier si une preuve
+  est valable est décidable, mais que savoir si un énoncé est un
+  théorème est seulement semi-décidable ; l'énoncé du théorème de
+  Gödel et l'idée de sa démonstration.
 \item \textbf{Coq :} l'utilisation générale de Coq telle que pratiquée
   en TP, et notamment les principales tactiques de raisonnement (sur
   les connecteurs logiques, types inductifs, égalités, etc.).  Le nom
@@ -138,8 +138,8 @@ Git: \input{vcline.tex}
   $\lambda\mu$-calcul.
 \item Les subtilités de la réalisabilité propositionnelle (p.ex., la
   réalisabilité de la formule de Tseitin).  La sémantique des
-  problèmes finis n'est pas exigible (mais pourra être utilisée si on
-  le souhaite).
+  problèmes finis n'est pas non plus exigible (mais pourra être
+  utilisée si on le souhaite).
 \item Le $\lambda$-cube de Barendregt, les subtilités de la différence
   entre $\exists$ et types sommes, la notion de
   prédicativité/imprédicativité, le système $F$.
-- 
cgit v1.2.3

