102 lines
4.6 KiB
Markdown
102 lines
4.6 KiB
Markdown
#s/maths/logique
|
|
|
|
> [!definition] Définition
|
|
> Une théorie est un ensemble d'énoncés
|
|
^definition
|
|
|
|
# Propriétés
|
|
|
|
## Cohérence
|
|
> [!proposition]+ Cohérence
|
|
> une théorie est cohérente si $\top \not \vdash \bot$
|
|
>
|
|
> > [!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$
|
|
> >
|
|
^coherence
|
|
|
|
> [!proposition]+ Complétude syntaxique
|
|
> Une théorie $T$ est syntaxiquement complète si elle est [[théorie logique#^coherence|cohérente]] et si, pour tout énoncé $f$, ou bien $\top \vdash f$ ou bien $\top \vdash \neg f$
|
|
^completude-syntaxique
|
|
|
|
> [!proposition]+ Finitude
|
|
> Si $T \vdash f$
|
|
> il existe une partie finie $T_{0}$ de $T$ telle que $T_{0} \vdash f$
|
|
> > [!démonstration]- Démonstration
|
|
> > regarder une démonstration de $T \vdash f$
|
|
> > $T_0 = \{ \text{axiomes de } T \text{ qui apparaissent} \}$
|
|
> > C'est une preuve de $T_0 \vdash f$
|
|
>
|
|
> > [!corollaire]
|
|
> > Une théorie $T$ est cohérente si et seulement si toute partie finie de $T$ est cohérente
|
|
>
|
|
> > [!corollaire]
|
|
> > Si $(T_{n})_{n \in \mathbb{N}}$ est une suite croissante ($T_0 \subseteq T_1 \subseteq T_2 \subseteq \cdots$) de théories **cohérentes**
|
|
> > Alors $\displaystyle T = \bigcup _{n \in \mathbb{N}} T_{n}$ est cohérente
|
|
> >
|
|
> > > [!démonstration]- Démonstration
|
|
> > > Soit $F \subseteq T$ une partie finie de $T$
|
|
> > > On se demande si $F$ est cohérente
|
|
> > > $f \in F \leadsto n_{f} \in \mathbb{N} \text{ tq } f \in T_{n_{f}}$
|
|
> > > $\displaystyle n = \min_{f \in F}(n_{f})$
|
|
> > > $F \subseteq T_{n}$ cohérente par hypothèses
|
|
> > > Donc $F$ est cohérente
|
|
>
|
|
> > [!corollaire]
|
|
> > Soit $(T_{i})_{i \in I}$ une **[[famille filtrante]]** de théories **cohérentes**
|
|
> > Alors $\displaystyle \bigcup _{i \in I} T_{i}$ est cohérente
|
|
>
|
|
> > [!corollaire]
|
|
> > Si $T$ est une théorie cohérente
|
|
> > Il existe une théorie cohérente $T'$ telle que $T \subseteq T'$ et qui est maximale (parmi les théories cohérentes contenant $T$) :
|
|
> > $\begin{cases} T \subseteq T' \\ T' \text{ est cohérente} \\ \text{si } f \not\subset T',\quad T' \cup \{ f \} \text{ n'est pas cohérente} \end{cases}$
|
|
> >
|
|
> > > [!démonstration]- Démonstration
|
|
> > > Application du [[lemme de Zorn]] :
|
|
> > > $\mathscr{C} = \{ \text{théories cohérentes} \}$ est inductif
|
|
> > > toute famille filtrante d'éléments de $\mathscr{C}$ est donc majorée
|
|
|
|
> [!proposition]+ Théorème de déduction
|
|
> Soit $f$ un énoncé, soit $T$ une théorie
|
|
> On a équivalence entre :
|
|
> - $T \cup \{ f \} \vdash g$
|
|
> - $T \vdash f \to g$
|
|
>
|
|
> > [!démonstration]- Démonstration
|
|
> > 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 :
|
|
> > $T \vdash f \to g_1 \qquad T \cup \{ f \} \vdash g_{1}$
|
|
> > $\vdots$
|
|
> > $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]]
|
|
> > >
|
|
|
|
|
|
|
|
%%
|
|
Tout cadre de raisonnement spécifique construit sur un langage donné.
|
|
|
|
Dans une approche syntaxique, une théorique logique, aussi appelée alors _théorie axiomatique_, est définie par un ensemble d'[[axiome|axiomes]] et de [[règle d'inférence|règles d'inférence]].
|
|
Dans une approche sémantique, elle est donnée par une interprétation particulière des éléments du langage.
|
|
|
|
# Exemple
|
|
Sur un même langage formel, il est possible de construire des théories logiques différentes. Par exemple, le symbole formel d'addition `+` n'aura pas la même interprétation en arithétique classique où l'on a `1+1 = 2`, et dans le [[calcul booléen]], où l'on a `1+1 = 0`.
|
|
%%
|
|
|