Cours 1 : Introduction

Introduction

Tiers-exclus :

Prop : \(∃𝛼, 𝛽∈ℝ\backslash ℚ, \\ 𝛼^𝛽∈ℚ\)

Dém :

  • Si $\sqrt{2}^\sqrt{2}∈ℚ$ : $𝛼=𝛽=\sqrt{2}$

  • Sinon : $𝛼=\sqrt{2}^\sqrt{2}, 𝛽 = \sqrt{2}$

NB : démonstration non constructive, non admise si on n’admet pas le tiers-exclus.

Hilbert : conjectures ⟶ “ je peux accepter l’existence de nouveaux objets si je prouve qu’il n’y a pas de contradiction avec les axiomes de l’arithmétique élémentaire.”

Dans l’arithmétique élémentaire : on peut coder toutes les fonctions récursives.

MAIS : Gödel : on ne pourra jamais démontrer la cohérence de l’arithmétique élémentaire avec ses axiomes.

Aujourd’hui : logique mathématique = branche des maths la plus abstraite.

Correspondance de Curry-Howard : un énoncé = un type, une preuve constructive = un programme.

Calculer = simplifier des preuves ⟶ théorie de la programmation : très proche de la théorie de la démonstration.

Ex :

  • Normalisation forte en programmation théorique ⟶ application aux compilateurs, etc …

    • ex: évaluation paresseuse de $ou(True, x)$
    • élimination des coupures

  • Church : trilogie Logique - Circuits - Automates

    • ex: logique monadique faible du second ordre est aussi expressive que les automates de Buchy

  • Lien Circuits/Complexité : Circuits : calcul plus efficace, en complexité, que les MT (parallélisation, etc..)

  • Bases de données : une requête = une formule ⟶ trouver toutes les instances des variables libres de la requête qui satisfont la requête

  • Complexité descriptive : quels sont les problèmes qui sont dans NP ⟶ ceux qu’on peut décrire par une formule existentielle du second ordre : théorème d’Immermann

  • Logique de Hoare en algo ⟶ Preuves de programmes, Spécification

  • Intelligence artificielle :

    • ex: représentation des connaissances, ontologie du web, …
    • logiques de description

  • Programmation en logique :

    • ex: Prolog, …

Objectif du cours : comprendre la distinction profonde entre syntaxe et sémantique.

Ex : quand on écrit une preuve en maths, on ne fait pas cette distinction.

NB : on ne formalisera pas la logique dans laquelle le cours est formulé, au début du cours

Calcul propositionnel

Logiques propositionnelles : décidables ⟶ pas très expressives.

1. Syntaxe

  • $𝒫$ : ensemble des variables propositionnelles (peut être infini)
Formules du calcul propositionnel :

le plus petit ensemble tq :

  • Si $P∈𝒫$, $P$ est une formule
  • $\bot, \top$ sont des formules
  • Si $𝜑, 𝜓$ sont des formules,
\[𝜑∧𝜓, 𝜑⟹𝜓, 𝜑∨𝜓, \lnot 𝜑\]

NB : cet ensemble existe : c’est un point fixe dans un trellis complet trivial.

2. Sémantique classique

Interprétation :

sous-ensemble de $𝒫$

$I$ satisfait $𝜑$ (noté $I \vDash 𝜑$) :

si :

  • $𝜑=\top$
  • $𝜑∈𝒫$ et $𝜑∈I$

  • Par induction :

    $𝜑=𝜑_1 ∧ 𝜑_2$ et : $I \vDash 𝜑_1$ et $I \vDash 𝜑_2$

  • etc…

$S$ : ensemble de formules

$I \vDash S$ :

si c’est le cas pour toutes les formules de $S$

NB : $I$ est alors un modèle de $S$.

$S$ est satisfaisable si $S$ a un modèle.

$𝜑$ est valide si tout interprétation $I$ satisfait $𝜑$.

$𝜑$ est conséquence logique de $S$ si :

pour tout $I∈2^𝒫$, $I \vDash S$ entraîne $I \vDash 𝜑$

Équivalence logique :

si $𝜑 \vDash 𝜓$ et $𝜓 \vDash 𝜑$

Exercice : Si $𝒫$ est fini, la relation “être des formules équivalentes” est une relation d’équivalence d’indice fini sur les formules : cardinal du quotient ?

Th de Compacité : Si $S$ est insatisfaisable, alors $S$ contient un sous-ensemble fini insatisfaisable.

Dém :

  • M1 : Compacité d’un espace topologique

  • M2 :

Preuve dans le cas où $𝒫 = \lbrace P_i \mid i∈ℕ \rbrace$

Arbres sémantiques :

Interprétation partielle : sous-ensemble finis de $𝒫$, application de $\lbrace P_0 ⋯ P_n \rbrace⟶ \lbrace 0,1 \rbrace$

On les ordonne partiellement par :

\[I≤J ⟺ \begin{cases} Dom(I)⊆Dom(J) \\ J_{\mid Dom(I)} = I \end{cases}\]

On peut représenter une interprétation partielle à l’aide d’un arbre de hauteur $n$ :

  digraph {
    rankdir=TB;
    a[label="P_1"];
    b[label="¬P_1"];
    ∅ -> a[label="1"];
    ∅ -> b[label="0"];
  }

$A(S)$ : arbre sémantique de $S$ = ens. des interprétations partielles qui ne falsifient aucune formule de $S$.

$I$ falsifie $𝜑$ si $VarProp(𝜑) ⊆ Dom(I)$ et $I \not\vDash 𝜑$

Ex :

$S = \lbrace P_0 ∨ P_1 \rbrace ∪ \lbrace P_i ⟹ P_{i+1} \mid i∈ℕ \rbrace$

$A(S)$ :

  digraph {
    rankdir=TB;
    subgraph cluster1 {
      label="P_0 ⟹ P_1";
      d[label="¬P_1"];
    }

    subgraph cluster2 {
      label="P_0 ∨ P_1";
      f[label="¬P_1"];
    }
    a[label="P_0"];
    b[label="¬P_0"];
    c[label="P_1"];
    e[label="P_1"];
    ∅ -> a[label="1"];
    ∅ -> b[label="0"];
    a -> c[label="1"];
    a -> d[label="0"];
    b -> e[label="1"];
    b -> f[label="0"];
  }

(Les sous-arbres encadrés sont supprimés, car ils contredisent la formule indiquée dans le cadre)

Si $A(S)$ est infini : il existe un chemin infini

\[\lbrace I_n \mid n∈ℕ \rbrace\]

où $(I_n)$ est croissante d’interprétations telles qu’aucune de falsifie une formule $S$, et

\[Dom(I_n) = \lbrace P_0, ⋯, P_n \rbrace\]

Soit $I$ tel que :

\[I(P_n) ≝ I_n(P_n)\]

alors :

\[I \vDash S\]

(sinon : il existe un $I_n$ tel que $I_n \not\vDash S$)

Par contraposée : si $S$ est insatisfaisable, alors l’arbre sémantique $A(S)$ est fini.

Donc toutes les feuilles sont des noeuds d’échec : on note

\[𝜑_1, ⋯, 𝜑_m∈S\]

qui étiquettent les noeuds d’échec.

Alors :

\[A(\lbrace 𝜑_1, ⋯, 𝜑_m \rbrace) = A(S)\]

et comme

$A(S)$ fini et toutes ses feuilles sont des noeuds d’échec ⟹ $S$ insatisfaisable (par contraposée)

il vient que

\[\lbrace 𝜑_1, ⋯, 𝜑_m \rbrace\]

est insatisfaisable.

Applications :

  • Si toute partie finie est $k$-coloriable, alors le graphe est $k$-coloriable.

Conséquence logique

Entscheidungsproblem : Problème de la déduction : est-ce qu’une formule est la conséquence d’un ensemble de formules ?

$S$, $𝜑$ : est-ce que $S \vDash 𝜑$ ?

i.e : est-ce que $S ∪ \lbrace \lnot 𝜑 \rbrace$ insatisfaisable ?

Résolution :

Clause :

disjonction de littéraux

Littéral :

Une variable propositionnelle ou sa négation

Simplifications classiques des formules, associativité, commutativité, de Morgan, distributivité du ET et du OU, etc ….

⟶ théorème de normalisation forte de ces règles : toute formule est équivalente à une formule CNF.

Prop : L’application des règles dans un ordre quelconque termine toujours.

\[𝛼: Formules ⟶ ℕ\]

tq si on peut simplifier $𝜑$ en $𝜓$,

\[𝛼(𝜑) > 𝛼(𝜓)\]
  • $𝛼(P)=2$ si $P∈𝒫$

Intuitivement : le NON et le OU rentrent à l’intérieur, le ET sort

  • $𝛼(𝜑∨𝜓)=𝛼(𝜑)𝛼(𝜓)$

  • $𝛼(𝜑∧𝜓)=𝛼(𝜑) + 𝛼(𝜓)+1$

  • $𝛼(\lnot 𝜑)=2^{𝛼(𝜑)}$

  • $𝛼(𝜑⟹𝜓)=2^{𝛼(𝜑)+𝛼(𝜓)}$

  • $𝛼(\top)=2$

  • $𝛼(\bot)=2$

Ex :

$𝛼(\lnot (𝜑 ∨ 𝜓)) = 2^{𝛼(𝜑)𝛼(𝜓)}$

⟶ $𝛼(\lnot 𝜑 ∧ \lnot 𝜓) = 2^{𝛼(𝜑)} + 2^{𝛼(𝜓)} + 1$

$𝛼(\lnot (𝜑 ∧ 𝜓)) = 2^{𝛼(𝜑)+𝛼(𝜓)+1}$

⟶ $𝛼(\lnot 𝜑 ∧ \lnot 𝜓) = 2^{𝛼(𝜑)} \times 2^{𝛼(𝜓)}$

$𝛼((𝜑 ∧ 𝜓) ∨ 𝜃) = (𝛼(𝜑) + 𝛼(𝜓)+1)𝛼(𝜃)$

⟶ $𝛼((𝜑 ∨ 𝜃) ∧ (𝜓 ∨ 𝜃)) = 𝛼(𝜑)𝛼(𝜃) + 𝛼(𝜓)𝛼(𝜃)+1$

Preuve :

Si $𝛼(𝜑) > 𝛼(𝜓)$ :

alors

  • $𝛼(𝜑 ∧ 𝜃) > 𝛼(𝜓∧ 𝜃)$
  • $𝛼(𝜑 ∨ 𝜃) > 𝛼(𝜓∨ 𝜃)$
  • $𝛼(𝜑 ∧ 𝜃) > 𝛼(𝜓∧ 𝜃)$

Pour tout $𝜑$, $𝛼(𝜑)≥2$

$∀x,y≥2$,

\[2^{xy} = 2^{\max(x,y) \min(x,y)} ≥ 2^{\max(x,y) + 2} > 2^{\max(x,y) + 1} + 1 > 2^{x} + 2^y + 1\]

Associativité + Commutativité ⟹ l’ordre d’application des règles n’a aucune importance

Prop : Les formules irréductibles sont des conjonctions des clauses.

Satisfaisabilité de $S$ se ramène à la satisfaisabilité d’un ensemble de clauses.

NB :

  1. “La” forme clausale n’est pas unique.
  • ex: $p ∨ \lnot p$ VS $q ∨ \lnot q$
  1. Complexité algorithmique optimale : exponentielle (spatialement, et temporellement), et on ne peut pas faire mieux.

Preuves

$I$ système d’inférence (résolution, déduction naturelle, calcul des séquents)

Arbres de preuves :

  • prémisses, conclusion

Ens. récursif de tuples $(𝜑_1, ⋯, 𝜑_n, 𝜑)$, où les $𝜑_i$ et $𝜑$ sont des formules

Preuve dans le système d’inférence $I$ avec hypothèses $H$ et conclusion $𝜑$ :

c’est un arbre fini étiqueté par des formules tq :

  • les feuilles sont étiquetées par les hypothèses
  • la racine est étiquetée par la conclusion
  • si un noeud interne est étiqueté par $𝜓$, il a $n$ fils étiquetés $𝜓_1, ⋯, 𝜓_n$ tq
$𝜓_1$ $⋯$ $𝜓_n$  
    $𝜓$  

est une instance d’une règle de $I$

NB : en logique, la racine d’un arbre de preuves est en bas.

Ex :

  • $L$ : littéral

  • $H ≝ \lbrace P∨Q, \lnot P∨Q, P ∨ \lnot Q, \lnot P ∨ \lnot Q \rbrace$

  • $I ≝ \lbrace Res, Fact \rbrace$ : deux règles :

Factorisation (Fact) :

$L∨L∨C$  
  $L∨C$

Résolution (Rés) :

$C∨\lnot P$ $C’∨ P$
  $C’∨C$

Alors :

$\lnot P ∨ \lnot Q$   $\lnot P ∨ Q$    
    $\lnot P ∨ \lnot P$    
    $\lnot P$    
        $\bot$

(idem à droite)

$I$ est correct (dan sla sémantique donnée):

si $\vdash_I ⊆ \vDash$

Prop : \(I = \lbrace Res, Fact\rbrace\)

est correct

Dém :

Mq

Si $H \vdash_I 𝜑$, soit $𝜋$ une preuve.

alors \(H \vDash 𝜑\)

Par réc sur $𝜋$ :

  • Cas de base : arbre réduit à une feuille : celle-ci est étiquetée par une formle $𝜑∈H$, et donc $H \vDash 𝜑$

  • Hérédité : La racine est étiquetée par $𝜑$.

    • Si elle a 1 fils :

    $𝜋 = $

    $𝜋_1$
    $𝜑$

$𝜋_1$ est une preuve de $𝜓$ par récurrence, avec les hypothèses $H$, et comme la règle de dérivation de $𝜑$ à partir de $𝜓$ ne peut être que Fact : le résultat est acquis (car tout modèle de $𝜓 = C∨L∨L$ est un modèle de $𝜑 = C∨L$ (facile)).

  • Si elle a deux fils :

$𝜋 = $ (Rec)

$𝜋_1$ $𝜋_2$
$𝜑$  

Par H.R :

\[\begin{cases} H \vDash 𝜓_1 \\ H \vDash 𝜓_2 \\ \end{cases}\]

et

(Rec)

$𝜓_1$ $𝜓_2$
$𝜑$  

Il vient alors que :

\[\begin{cases} 𝜓_1 = C∨ \lnot P \\ 𝜓_2 = C'∨ P \\ 𝜑 = C∨C' \end{cases}\]

Pour tout $I$ : si $I \vDash H$, alors

\[\begin{cases} I \vDash 𝜓_1 \\ I \vDash 𝜓_2 \\ \end{cases}\]

et

\[\begin{cases} I \vDash C \text{ OU } I \vDash \lnot P \\ I \vDash C' \text{ OU } I \vDash P \\ \end{cases}\]

  • Si $I \vDash C$ : alors $I \vDash C ∨ C’$

  • Sinon : $I \vDash \lnot P$ : d’où $I \not\vDash P$, et $I \vDash C’$. Donc $I \vDash C ∨ C’$

Dans tous les cas : $C \vDash C ∨ C’$

Leave a comment