Logique du premier ordre

Formes normales de la logique propositionnelle

En logique propositionnelle, toute formule F(X) peut se mettre sous forme :

• CNF ⋀_i⋁_jℓ_i, j où ℓ est un litéral de la forme x ∈ X ou ¬x ∈ X.
• DNF ⋁_i⋀_jℓ_i, j où ℓ est un litéral de la forme x ∈ X ou ¬x ∈ X.

Démonstration

1. soit par la table de vérité
2. soit algorithmiquement :
   • pousser les négations vers le bas (Negation Normal Form via De Morgan)
   • trouver les arbres de preuves (voir tableau)

Forme Prénexe

Une formule de la LPO est sous forme prénexe si les quantificateurs sont au début :

Q₁x₁, …, Q_nx_n.G(x₁,…,x_n,y₁,…,y_p)

où Q_i vaut soit ∀ soit ∃.

Avantages

• Lecture plus facile des variables libres et liées
• Interprétation : sémantique liée aux jeux (alterner entre blocs ∀ et ∃)
• Nombre d’alternances ∀,∃: mesure de complexité d’une formule (hiérarchie polynomiale PH)

Mise sous forme normale prénexe

Pour tout Φ ∈ LPO, il existe Ψ en forme prénexe telle que  ⊨ Φ ⇔ Ψ

Algorithme

On fait remonter les quantificateurs syntaxiquement :

Same old shit

∀x(x∨y) ∧ (x⇒z) ≢ ∀x((x∨y) ∧ (x ⇒ z))

Mais

∀x(x∨y) ∧ (x⇒z) ≡ ∀u(u∨y) ∧ (x⇒z) ≡ ∀u((u∨y)∧(x⇒z))

Exercice

Mettre sous forme prénexe

1. ∀x(P(x)) ⇒ ∃x(Q(x))
2. ∃x(Q(x)) ⇒ (∀x(∀z(P(x,z))∧∃z(R(x,z))))

Application : Skolemisation

On peut “enlever” les variables existentiellement quantifiées d’une formule prénexe :

Φ ≡ ∀x₁, …, ∀x_n, ∃y, ∀z.ϕ(x₁,…,x_n,y,z)

Est “équivalent” à

Φ′ ≡ ∀x₁, …, ∀x_n, ∀z.ϕ(x₁, …, x_n, f_y(x₁,…,x_n) , z)

où f_y est un symbole de fonction frais.

Rappel : théorie

Une théorie T est un ensemble de formule de la LPO appelés axiomes.

Rappel : Modèles et théorème

Pour Φ ∈ LPO sur le langage ℒ

Théorème de la logique propositionnelle

Comment prouver que F = (p∧q) ⇒ (p∨q) est un théorème ?

• On peut montrer que c’est vrai dans toutes les interprétations

• On peut montrer que ¬F est contradictoire en utilisant la résolution

¬F = p ∧ q ∧ ¬p ∧ ¬q : contradiction sur p et ¬p.

Théorème de la logique du premier ordre

Comment prouver que ∀x∀y(p(x)∧q(x,y)) ⇒ (p(x)∨q(x,y)) est un théorème ?

• Vrai dans toutes les interprétations ? Il y en a une infinité !

• On peut :

  • fixer une interprétation I
  • calculer val(F,I)?
    • Choisir x := a, y := b.
    • Valeur de (p(a)∧q(a,b)) ⇒ (p(a)∨q(a,b)) ?
    • Toujours 1 quelque soit la valeur de p(a) ∈ {0, 1} et q(a,b) ∈ {0, 1} puisque c’est une formule propositionnelle!

Un système de preuve

On souhaiterait manipuler uniquement la syntaxe de la formule en utilisant un système de preuve :

• Déduction naturelle (Gentzen, 1934) : se généralise à LPO
• Calcul des séquents (LK)
• Résolution du premier ordre

Calcul des séquences

On manipule logiquement des séquents:

A₁, …, A_m ⊢ B₁, …, B_n

Intuitivement cela veut dire : A₁ ∧ … ∧ A_m ⇒ B₁ ∨ … ∨ B_n.

Les règles

Axiome

Groupe structurel

Groupe Logique

Connecteurs logiques

Quantificateur

La coupure

En gros: A → B et A implique B!

C’est en général là que la “création” mathématique se passe !

Démonstration !

Complétude et correction

• LK est correct: si  ⊢ Φ a une preuve alors Φ est un théorème de LPO!
• LK est complet: tout théorème de LPO a une preuve dans LK.

Complétude et théories

Soit T une théorie (un ensemble d’axiome, pas forcément finis).

• on dit que T est contradictoire si on peut trouver un ensemble fini d’axiomes T′ ⊆ T tels que T′ ⊢ False, ie, on peut prouver syntaxiquement que T est “absurde”

Autrement dit, on peut prouver syntaxiquement tous les théorèmes d’une théorie (ie les choses vraies dans tous les modèles de T !)

Théorème de compacité

La complétude permet d’établir un résultat intéressant :

Le théorème d’incomplétude

Soit T une théorie

• récursive (on sait énumérer ses atomes)
• suffisamment “puissante” pour encoder l’arithmétique.

• Φ est donc vraie dans au moins un modèle de T et fausse dans un autre.
• En particulier, Φ peut être choisie comme une formule disant “T est consistante”.

TP

TP d’aujourd’hui : forme prénexe et preuve dans LK!