Logique du premier ordre

Théories et modèles

Florent Capelli

14 Février 2024

Rappels

Langages et interprétations

  • Langage ℒ = (𝒞,𝒫,ℱ)
    • 𝒞 constantes “Médor”, “0” etc.
    • 𝒫 prédicats avec arité : “Aime(2)”, “Chien(1)”, “=(2)”
    • ℱ fonctions avec arité : “+(2)”, “cos(1)”, “sqrt(1)”
  • ℒ-interprétation :
    • un domaine U
    • un élément cℐ ∈ U pour chaque c ∈ 𝒞
    • une relation Pℐ ⊆ Uk pour chaque P ∈ 𝒫
    • une fonction fℐ: Uk → U pour chaque f ∈ ℱ

Termes et formules

LPO(ℒ): logique du premier ordre sur le langage ℒ

  • Termes : composer des fonctions et des constantes, s’interprétera comme une valeur du domaine
    • f(0,x,y,g(2,z))
  • Atomes : appliquer un prédicat à des termes, s’interprétera par une valeur booléenne vrai/faux
    • P(t1,…,tk) par exemple 2x + y < 3z.
    • t1 = t2
  • Formules : construites depuis les atomes avec des quantificateurs, connecteurs logiques ou atomes
    • P(t1,…,tk)
    • F▫G où ▫ ∈ {∧,∨, ⇒ }
    • ¬F
    • ∀x(F),
    • ∃x(F)

Valeur d’une formule

On définit inductivement la valeur val(Φ,e,I) ∈ {0, 1} d’une formule Φ par rapport à une interprétation ℐ et un environnement e

  • Atomes
    • val(P(t1,…,tk),e,ℐ) = 1 ssi (val(t1,e,ℐ),…,val(tk,e,ℐ)) ∈ Pℐ.
    • val(t1=t2,e,ℐ) = 1 ssi val(t1,e,ℐ) = val(t2,e,ℐ).
  • Connecteurs logiques
    • val(F∧G,e,ℐ) = 1 ssi val(F,e,ℐ) = 1 et val(G,e,ℐ) = 1
    • val(F∨G,e,ℐ) = 1 ssi val(F,e,ℐ) = 1 ou bien val(G,e,ℐ) = 1
    • val(¬F,e,ℐ) = 1 ssi val(F,e,ℐ) = 0
    • val(F⇒G,e,ℐ) = 1 ssi val(F,e,ℐ) = 0 ou bien val(G,e,ℐ) = 1.
  • Quantificateurs
    • val(∀x(F),e,ℐ) = 1 ssi val(F,e[x:=a],ℐ) = 1 quelque soit a ∈ U
    • val(∃x(F),e,ℐ) = 1 ssi val(F,e[x:=a],ℐ) = 1 pour au moins un a ∈ U.

Exercice d’échauffement

On définit l’interprétation I:

  • le domaine est ℤ
  • + est interprété par f(a,b) = a × b
  • × est interprété par g(a,b) = ab
  • a ≺ b est interprété par a2 + b ≥ 1

Question :

  • Que vaut val((3+(2×x))×y,[x=2,y=3],I) ?
  • Et val(Φ,I) où Φ = ∃x(∀y(x+y≺x×y)) ?

Quelques observations sur LPO

Dualité ∀,∃

D’un point de vue expressivité, on a besoin que d’un quantificateur :

 ⊨ ∀x(F) ⇔ ¬∃x(¬F)  ⊨ ∃x(F) ⇔ ¬∀x(¬F)

Autrement dit, pour toute interprétation ℐ,

  • ℐ ⊨ ∀x(F) si et seulement si ℐ ⊨ ¬∃x(¬F)
  • ℐ ⊨ ∃x(F) si et seulement si ℐ ⊨ ¬∀x(¬F)

Démonstration : ces formules ont la même valeur.

Logique propositionnelle

Soit ℒ = (𝒞,𝒫,ℱ) un langage avec:

  • ℱ = ∅
  • 𝒞 = ∅
  • 𝒫  ne contient que des prédicats d’arité 0.

LPO(ℒ) c’est la logique propositionnelle (voir exercice 3)!

Quelque soit l’interprétation ℐ :

  • Valeur d’un prédicat P d’arité 0 c’est 0 si Pℐ = ∅, soit 1 si Pℐ = {∅}.
  • Valeur de F ∧ G, F ∨ G, F ⇒ G, ¬F: pareil qu’en logique propositionnelle
  • ∀x(F), ∃x(F)? x n’apparaît pas dans F donc val(∀x(F),e,ℐ) = val(F,ℐ)

Substitution : un exemple côté modèle

Constantes 0, 1, prédicat ≤. I une interprétation sur le domaine U.

Si I ⊨ ∀x(0≤x) alors I ⊨ (0≤1) ?

  • Oui : si val(∀x(0≤x)) alors pour toute valeur u ∈ U, 0I≤Iu. En particulier u = 1I.
  • Peut-on le voir directement dans les formules ?

Substitution : côté formule

On a envie de dire : si I ⊨ ∀x(F) alors on peut remplacer x par n’importe quel terme dans la formule ! Notion de substitution

  • F = (0≤x)
  • t = f(0,1)

On note F[x:=t] pour 0 ≤ f(0,1)

Tentative: Soit F une formule, x une variable libre de F et t un terme. On note F[x:=t] la formule obtenue en remplaçant toutes les occurrences de x par le terme t.

Attention aux captures

F = ∀x(P(x,y)).

Qu’est-ce que F[y:=f(x)]?

On serait tenter d’écrire F[y:=f(x)] ≡ ∀x(P(x,f(x))).

On a une capture de la variable x du terme f(x) par le quantificateur universel.

On évite cela en renommant le quantificateur : F[y:=f(x)] ≡ ∀z(P(z,f(x))).

Pour y une variable libre de F et t un terme, on note F[x:=t] la formule obtenue en renommant toutes les variables liées de F qui sont libres dans t par des noms de variables distincts et qui n’apparaissent pas ailleurs dans la formule ni dans t puis on remplace toutes les occurrence de x par t.

Petit exercice

Soit F une formule du premier ordre, XF les variables libres de F, y ∈ XF et t un terme dont les variables (libres) sont Xt.

Quelles sont les variables libres de F[x:=t] ?

  1. Cela dépend des variables liées de F.
  2. (XF\{x})
  3. (XF∪Xt) \ {x}
  4. (XF\{x}) ∪ Xt

Substitution et universalité

Si  ⊨ ∀x(F) alors  ⊨ ∀Xt(F[x:=t])

Cela ne serait pas vrai si on autorisait à remplacer avec capture :

  • ∃y(P(x,y)
  • On peut avoir ∀x∃yP(x,y) sans avoir ∀y∃yP(y,y)

Théories

Pertinence des choix de symboles

Soit ℒ le langage avec les constantes {P, F, C} et le prédicat <.

On définit l’interprétation I sur {0, 1, 2} par

  • PI = 0
  • FI = 1
  • CI = 2
  • 0 < 1, 1 < 2 et 2 < 0.

A-t-on I ⊨ ∀x∀y∀z.(x<y∧y<z) ⇒ x < z ?

Non: PI < FI et FI < CI mais PI ≮ CI.

Un problème de spécification

Choix du symbole < : on veut imposer que < soit un ordre total !

  1. Transitivité : Tr = ∀x∀y∀z.(x<y∧y<z) ⇒ x < z.
  2. Totalité : Tot = ∀x∀y.(x<y∨y<x∨x=y)
  3. Antisymétrie : Ant = ∀x∀y.¬(x<y∧y<x)

Tous les modèles qui respectent Tr, Tot et Ant interprète < comme un ordre total !

On dit que T = {Tr, Tot, Ant} est la théorie des ordres totaux.

Théories : définitions

Une ℒ-théorie T est un ensemble (pas nécessairement fini) de LPO(ℒ).

  • Un élément A ∈ T s’appelle un axiome
  • Un modèle I de T est une interprétation de ℒ telle que I ⊨ A pour tout A ∈ T (noté I ⊨ T).

Une théorie T peut être comprise comme une spécification des éléments de ℒ. Un modèle de T comme une implémentation de cette spécification.

Par exemple: ℕ ⊨ T où T est la théorie des ordres totaux (interprétation “naturelle”), mais aussi (ℕ2,<lex) etc.

Théorie des ordres denses

Langage : prédicat <, pas de fonction, pas de constantes.

  • < est un ordre total
    1. Transitivité : Tr = ∀x∀y∀z.(x<y∧y<z) ⇒ x < z.
    2. Totalité : Tot = ∀x∀y.(x<y∨y<x∨x=y)
    3. Antisymétrie : Ant = ∀x∀y.¬(x<y∧y<x)
  • < est dense
    1. ∀x∀y∃z.x < y ⇒ (x<z∧z<y)
  • < est non borné
    1. ∀x∃y.x < y
    2. ∀x∃y.y < x

L’ensemble de ces axiomes forment To, la théorie des ordres denses.

(ℚ,<) ⊨ To mais pas (ℤ,<) ⊨ To

Arithmétique

Un certain nombre de théories ont eu pour but de formaliser l’arithmétique dans ℕ.

  • Arithmétique de Presburger
  • Arithmétique de Robinson
  • Arithmétique de Peano

Exemple : Arithmétique de Presburger

Arithmétique sans multiplication, Pres :

  • ∀x¬(0=x+1)
  • ∀x∀y.x + 1 = y + 1 ⇒ x = y
  • ∀x.x + 0 = x
  • ∀x∀y.(x+y) + 1 = x + (y+1)
  • Schéma de récursion : pour toute formule P(x) (x variable libre), on a un axiome (P(0)∧∀x(P(x)⇒P(x+1))) ⇒ ∀y.P(y)

On a une infinité d’axiomes !

Cela suffit à prouver que + est commutatif, associatif ie:

  • Pres ⊨ ∀x∀y.x + y = y + x
  • Pres ⊨ ∀x∀y∀z.(x+y) + z = x + (y+z)

Théories et décidabilité

On s’intéresse au problème suivant : étant donné une théorie T et une formule F, peut-on décider si T ⊨ F ?

La plupart du temps : indécidable

Décidable pour certaines théories, notamment :

  • Ordre dense
  • Presburger

To be continued

…