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 et si, pour tout énoncé f, ou bien T \vdash f ou bien T \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

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.

[!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 et de règle 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. %%

4.6 KiB Raw Blame History

Propriétés

Cohérence

Exemple

4.6 KiB

Raw Blame History