Cours 5 : Logique du premier ordre

Theories

Elementary arithmetics

  • $∀x, 0+x =x$
  • $∀x, ∀y, S(x)+y = S(x+y)$
  • $∀x, 0*x = 0$
  • $∀x, ∀y, S(x) = S(y) ⇒ x=y$
  • $∀x, x≠0 ⇒ ∃ y, x=S(y)$
  • $∀x, ∀y, S(x)*y = (x*y)+y$
  • $∀x, ¬(S(x)=0)$

Group theory

  • $∀x, ∀y, ∀z, (xy)z = x(yz)$
  • $∃e, ∀x, xe = ex ∧ xx^{-1} = e ∧ x^{-1}x = e$ </span>

A theory equivalent to group theory

  • $∀x, ∀y, x^{-1}*(xy)=y$

Syntax

Let $F$ be a set of symbols of functions $f∈F$, each one having arity $a(f) ∈ℕ$

Let $X$ be a set of variables.

Terms $t∈T(F,X)$ :
  • $x∈X$
  • or $f(t_1, ⋯, t_n)$ where the $t_i$ a are terms and $a(f)=n$

Ex :

$F ≝ \lbrace z (0), + (2), × (3), s (1) \rbrace$

Formulas of the first-order predicate calculus

Let $𝒫$ be a set of relation symbols s.t $P∈𝒫$ has arity $a(P)∈ℕ$

Formula $𝜑∈CP_1 (F, 𝒫)$ :
  • an atomic formula $P(t_1, ⋯, t_n)$, where $a(P) = n$ and $t_1, ⋯, t_n$ are terms

  • if $𝜑, 𝜓 ∈ CP_1(F, 𝒫)$, then

    • $¬𝜑, 𝜑⇒𝜓, 𝜑∧𝜓, 𝜑∨𝜓$

$F$-algebra

$F$-algebra :
  • a given non empty set $D_A$
  • for all $f∈F$, $f_A : D_A^{a(f)} ⟶ D_A$

Exs :

$(ℕ, +_ℕ, ×_ℕ, 0_ℕ, S_ℕ)$ is an $F$-algebra where $F ≝ \lbrace +(2), *(2), 0(0), s(1) \rbrace$

$A’$, with :

  • $D_{A’} = 𝛴^\ast$
  • $+_{A’}$ is the concatenation

  • $×_{A’}$ is defined by

    \[w ×_{A'} w' ≝ w[a \mapsto w']\]

    for $a∈𝛴$

  • $S_{A’}(w) = w\cdot a$

Ex :

$T(F,X)$ is a $F$-algebra, where functions are trivially interpreted :

\[f_{T(F, X)}(t_1, ⋯, t_n) ≝ f(t_1, ⋯, t_n)\]

As it happens, the domain is $T(F, X)$

Morphisms

A morphism of $A ⟶ A’$, where $A, A’$ are $F$-algebras :

it is an application $h: D_A ⟶ D_{A’}$ s.t

  • for all $f∈F, e_1, ⋯, e_n∈D_A$ where $a(f)=n$ :

    \[h(f_A(e_1, ⋯, e_n)) = f_{A'}(h(e_1), ⋯, h(e_n))\]

Ex :

\[h ≝ \begin{cases} A_𝛴 ⟶ ℕ \\ w \mapsto \vert w \vert_a \end{cases}\]
  • $h(z_A) = h(𝜀) = 0 = z_ℕ$
  • $h(w+_A w’) = h(ww’) = \vert ww’ \vert_a = \vert w \vert_a + \vert w’ \vert_a = h(w) +_ℕ h(w’)$
  • $h(w×_A w’) = h(w[a \mapsto w’]) = \vert w \vert_a \vert w’ \vert_a$
  • $h(s_A(w)) = h(w \cdot a) = \vert w \vert_a +1 = S_ℕ(h(w))$

Birkhoff Theorem

Th (Birkhoff) :

If $𝜎 : X ⟶ A$, where $A$ is a $F$-algebra, then there exists a unique morphism $\widehat{𝜎} : T(F, X) ⟶ A$ s.t $\widehat{𝜎}(x) = 𝜎(x)$ for all $x∈X$

Proof :

$\widehat{𝜎}(t)$ is constructed by structural induction on $t$, with

  • $\widehat{𝜎}(x) = 𝜎(x)$
  • $\widehat{𝜎}(f(t_1, ⋯, t_n)) = f_A(\widehat{𝜎}(t_1), ⋯, \widehat{𝜎}(t_n))$

Ex :

$x + s(y)$

\[𝜎 ≝ \begin{cases} X ⟶ A_𝛴\\ x \mapsto ab \\ y \mapsto b \end{cases}\]

$\widehat{𝜎}(x+s(y)) = abba$

\[𝜎' ≝ \begin{cases} X ⟶ ℕ \\ x \mapsto 1 \\ y \mapsto 2 \end{cases}\]

$\widehat{𝜎}(x+s(y)) = 4$

$\widehat{𝜎}(t)$ is denoted $⟦t⟧{𝜎,A}$, or $t𝜎$

$𝜎 : X ⟶A$ is called an interpretation.

$𝜎 : X ⟶ T(F, X)$ is a substitution

\[Dom(𝜎) ≝ \lbrace x \mid x𝜎 ≠ x \rbrace\]

If $Dom(𝜎) = \lbrace x_1, ⋯, x_n \rbrace$, $𝜎$ is denoted $\lbrace x_1 \mapsto t_1, ⋯, x_n \mapsto t_n\rbrace$

where $t_i = x_i 𝜎$

Herbrand Theorem

A Hebrand model :

a ${\cal F, P}$-structure on the ${\cal F}$-algebra $T({\cal F})$ (closed terms).

NB : to avoid the emptiness of $T({\cal F})$, ${\cal F}$ is supposed to comprise at least one constant symbol.

$H$ is identified to a subset of the set of the closed terms, by defining :

\[P_H = \lbrace (t_1, ⋯, t_n) \mid P(t_1, ⋯, t_n) ∈ H \rbrace\]

Ex :

${\cal F}≝ \lbrace z:0, s:1 \rbrace$

$P≝ \lbrace E:2 \rbrace$

is a Herbrand model that is isomorph to $ℕ$,

where $E$ is interpreted by $=_ℕ$.

($s_H(t) = s(t)$)

Hebrand theorem : Let $S$ be a set of universally quantified closed formulas.

Then $S$ is satisfiable iff $S$ has a Herbrand model.

NB : “universally quantified” is a necessary prerequisite.

Counter-example :

${\cal F}≝ \lbrace c:0\rbrace$

$P≝ \lbrace E:2 \rbrace$

$S$ comprises the theory of equality, and $∃x; ¬E(x, c)$.

$S$ is sat., but the two Herbrand-models $∅$ and $\lbrace E(c,c) \rbrace$ don’t statisfy $S$.

Th : If ${\cal F}$ is recursively enumerable, the set of valid formulas is recursively enumerable.

$T({\cal F})$ is rec. en.

Let $X$ be a finite set.

Then $\lbrace 𝜎 \mid dom(𝜎) = X \rbrace$ is rec. en.

Algorithm
Is_valid(𝜑):

  𝜓 = Sk(¬𝜑)
  𝜓 = ∀x_1, ⋯, x_n, 𝜓'
  n = 0
  S = ∅
  n +=1 (L)
  S ∪= {𝜓' 𝜎_n}
    where 𝜎_n is the n-th substitution with dom(𝜎) = {x_1, ⋯, x_n}

  If S is insat. (propositionally) alors renvoie "Valide"

  Else
    return (L)

$𝜑$ valid ⟺ $¬𝜑$ unsatisfiable (≠ not valid)

valid : all models satisfy it

satisfiable : there exists one model that satisfies it

First order resolution :

Example :

\[S = \lbrace ∀x, y. P(x, f(y)) ∨ P(f(y), x), \\ ∀x, y. ¬ P(x, f(y)) ∨ ¬ P(f(y), x) \rbrace\]

Let’s show that $S \vDash \bot$ by resolution.

Factorization :

 
$P(x, f(y)) ∨ P(f(y), x)$
$P(f(z), f(z))$
\[mgu(⟨x, f(y)⟩, ⟨f(y), x⟩) = \lbrace x \mapsto f(z), y \mapsto z \rbrace\]

Idem for $¬ P(x, f(y)) ∨ ¬ P(f(y), x) ⟶_{Fact} ¬ P(f(z’), f(z’))$

And finally :

Resolution :

   
$P(f(z), f(z))$ $¬P(f(z’), f(z’))$
$\bot$  

Leave a comment