oskar/cours
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

eduroam-prg-sg-1-46-206.net.univ-paris-diderot.fr 2025-10-8:15:15:30

Browse Source
This commit is contained in:
oskar
2025-10-08 15:15:30 +02:00
parent eb1b2b1358
commit 408b941a83
2 changed files with 22 additions and 2 deletions
Download Patch File Download Diff File Expand all files Collapse all files

1
règles de démonstration.md
View File

@@ -3,6 +3,7 @@ up:
tags: tags:
- s/maths/logique - s/maths/logique
aliases: aliases:
- règle d'axiome
--- ---
```breadcrumbs ```breadcrumbs

23
théorie logique.md
View File

@@ -13,6 +13,7 @@
> > [!corollaire] Lemme > > [!corollaire] Lemme
> > Une théorie $T$ est cohérente s'il n'existe pas d'énoncé $f$ tel que $T \vdash f$ et $T \vdash \neg f$ > > Une théorie $T$ est cohérente s'il n'existe pas d'énoncé $f$ tel que $T \vdash f$ et $T \vdash \neg f$
> > > >
^coherence
> [!proposition]+ Finitude > [!proposition]+ Finitude
> Si $T \vdash f$ > Si $T \vdash f$
@@ -60,9 +61,27 @@
> > [!démonstration]- Démonstration > > [!démonstration]- Démonstration
> > Soit $(g_1, \dots, g_{n})$ une démonstration formelle de $T \cup \{ f \} \vdash g$ > > Soit $(g_1, \dots, g_{n})$ une démonstration formelle de $T \cup \{ f \} \vdash g$
> > On obtient une démonstration formelle de $T \vdash f \to g$ en partant de la suite $(f \to g_1, \dots, f\to g_{n})$ et en insérant des formules supplémentaires : > > On obtient une démonstration formelle de $T \vdash f \to g$ en partant de la suite $(f \to g_1, \dots, f\to g_{n})$ et en insérant des formules supplémentaires :
> > $T \vdash f \to g_1 \qquad T \cup \{ f \}$ > > $T \vdash f \to g_1 \qquad T \cup \{ f \} \vdash g_{1}$
> > $\vdots$ > > $\vdots$
> > $T \vdash f \to g_{n-1}$ > > $T \vdash f \to g_{n-1} \qquad T \cup \{ f \} \vdash g_{m}$
> > Si $T \cup \{ f \} \vdash g_{m}$ est une [[règles de démonstration|règle d'axiome]]
> > - $1^{\text{er}}$ cas $g_{m} \in T$ :
> > $T \vdash g_{m}$ (axiome)
> > $T \vdash g_{m} \to (f \to g_{m})$ (tautologie : $p \to (q \to p)$)
> > $T \vdash f \to g_{m}$ par [[modus ponens]]
> > - $2^{\text{ème}}$ cas $g_{m} = f$
> > alors $T \vdash (f \to f)$ est une tautologie
> > - Si $T \cup \{ f \} \vdash g_{m}$ est un [[modus ponens]]
> > $T \cup \{ f \} \vdash g_{m}$ ...???
>
> > [!corollaire] (raisonnement par l'absurde)
> > Pour prouver $T \vdash f$ (il faut et ) il suffit de prouver que $T \cup \{ \neg f \}$ n'est pas [[théorie logique#^coherence|cohérente]].
> > > [!démonstration]- Démonstration
> > > - supposons que $T \cup \{ \neg f \}$ n'est pas cohérente
> > > par le théorème de déduction on a que $T \vdash \neg f \to \bot$
> > > alors $T \vdash (\neg f \to \bot) \to f$ ([[tautologie]])
> > > et donc $T \vdash f$ par [[modus ponens]]
> > >