deduction_naturelle

On redéfinit la notiation ⊧ pour correspondre à la conséquance logique entre une ensemble de formule Γ et une formule f. Dans les développement précédents f₁ ⊧ f₂ correspondait à la conséquence logique entre deux formule.

Notation "Γ ⊧ f" := (consequence_set Γ f).

Ce module définit le système de preuve de la déduction naturelle pour la logique propositionnelle. Il établit les propriétés suivantes de ce système:

correction vis-à-vis de la sémantique des propriétés
complétude vis-à-vis de la sémantique des propriétés. Cette preuve est directement inspirée de celle Michel Levy dans son polycopié de cours "Introduction à la logique" et dans le livre correspondant.

Préliminaires

Lemma not_ex_contradictoire_2:
  ∀ Γ,
    ~(∃ n, Var n ∈ Γ ∧ ((¬Var n) ∈ Γ ∨ (Var n ⇒⊥) ∈ Γ ))
    → ∀ n, (Var n) ∈ Γ → ~((¬Var n) ∈ Γ ∨ (Var n ⇒⊥) ∈ Γ ).

Lemma not_ex_contradictoire_3:
  ∀ Γ,
    ~(∃ n, (Var n) ∈ Γ ∧ ((¬Var n) ∈ Γ ∨ (Var n ⇒⊥) ∈ Γ ))
    → ∀ n, (¬Var n) ∈ Γ → ¬ (Var n) ∈ Γ.

Lemma not_ex_contradictoire_4:
  ∀ Γ,
    ~(∃ n, (Var n) ∈ Γ ∧ ((¬Var n) ∈ Γ ∨(Var n ⇒⊥) ∈ Γ ))
    → ∀ n, (Var n ⇒ ⊥) ∈ Γ → ¬(Var n) ∈ Γ.

Déduction naturelle: Définition

Définition inductive d'une preuve en deduction naturelle

Inductive pf : env →formule → Prop :=
ax : ∀ Γ φ, φ ∈ Γ → Γ ⊢ φ
| true_ax : ∀ Γ, Γ ⊢ ⊤
| impe: ∀ Γ φ₁ φ₂, Γ ⊢ φ ₁ ⇒ φ ₂ → Γ ⊢ φ ₁ → Γ ⊢ φ ₂
| impi: ∀ Γ φ₁ φ₂, φ ₁ :: Γ ⊢ φ ₂ → Γ ⊢ φ ₁ ⇒ φ ₂
| andi: ∀ Γ φ₁ φ₂, Γ ⊢ φ ₁ → Γ ⊢ φ ₂ → Γ ⊢ φ ₁ ∧ φ ₂
| ande1: ∀ Γ φ₁ φ₂, Γ ⊢ φ ₁ ∧ φ ₂ → Γ ⊢ φ ₁
| ande2: ∀ Γ φ₁ φ₂, Γ ⊢ φ ₁ ∧ φ ₂ → Γ ⊢ φ ₂
| noti: ∀ Γ φ₁, φ ₁ :: Γ ⊢ ⊥ → Γ ⊢ ¬ φ ₁
| note: ∀ Γ φ₁ φ₂, Γ ⊢ φ ₁ → Γ ⊢ ¬ φ ₁ → Γ ⊢ φ ₂
| ore: ∀ Γ φ₁ φ₂ φ₃,
Γ ⊢ φ ₁ ∨ φ ₂ → φ ₁::Γ ⊢ φ ₃ → φ ₂::Γ ⊢ φ ₃ → Γ ⊢ φ ₃
| ori1: ∀ Γ φ₁ φ₂, Γ ⊢ φ ₁ → Γ ⊢ φ ₁ ∨ φ ₂
| ori2: ∀ Γ φ₁ φ₂, Γ ⊢ φ ₂ → Γ ⊢ φ ₁ ∨ φ ₂
| fale: ∀ Γ φ₁, (¬ φ ₁) :: Γ ⊢ ⊥ → Γ ⊢ φ ₁
where " X ⊢ Y" := (pf X Y).

Exemples de preuve en déduction naturelle

Certaines de ces preuves sont réutilisées plus bas. On utilise une tactic dédiée pour la règle ax: tax. Cette tactique applique ax puis essaie de prouver sa prémisse p ∈ Γ automatiquement.

Module Exemple_DN.
  Lemma ex_DN_1: pf ([X₁]) X₁.
    tax.
  Qed.

  Lemma ex_DN_2: [X₁ , X₂] ⊢ X₁.
    tax.
  Qed.

  Lemma ex_DN_3: [X₂ , X₁] ⊢ X₁.
    tax.
  Qed.

Cette propriété est connue sous le nom « Tiers exclu ». Le tiers exclu est prouvable en déduction naturelle pour toute formule A.

  Lemma a_or_nota : ∀ A Γ, Γ ⊢ A ∨¬A.
  Proof.
    intros A Γ.
    apply fale.
    apply note with (A∨¬A).
    - apply ori2.
      apply noti.
      apply note with (A∨¬A).
      + apply ori1.
        tax.
      + tax.
    - tax.
  Qed.
End Exemple_DN.

Propriétés remarquables de la déduction naturelles

Ces propriétés sont nécessaires à la preuve de complétude de la déduction naturelle.

Compatibilité de la preuve avec la notion d'égalité sur les environnements.

Lemma equiv_gamma : ∀ Γ Γ' f, ENV.eq Γ Γ' → Γ ⊢ f → Γ' ⊢ f.

Le morphisme associé

Add Parametric Morphism: pf
with signature ENV.eq ==> Logic.eq ==> iff as pf_morphism.

Règles supplémentaires déductible des règles de base

Lemma or_imp: ∀ B C Γ, ((B ⇒ ⊥) ⇒ C) :: Γ ⊢ (B ∨C ).

Lemma weakening: ∀ Γ φ ψ, Γ ⊢ ψ → φ :: Γ ⊢ ψ.

Lemma impe_impi_add: ∀ Γ φ φ' ψ, φ :: Γ ⊢ ψ → φ' :: Γ ⊢ φ → φ' :: Γ ⊢ ψ.

Lemma impe_impi: ∀ Γ φ ψ, φ :: Γ ⊢ ψ → Γ ⊢ φ → Γ ⊢ ψ.

Lemma impe_impi_add_double: ∀ Γ φ φ' φ'' ψ,
                              φ :: φ' :: Γ ⊢ ψ →
                              φ'' :: Γ ⊢ φ →
                              φ'' :: Γ ⊢ φ' →
                              φ'' :: Γ ⊢ ψ.

Plusieurs des ces lemmes sont en exercices dans la preuve de M. Levy.

Exercie 46 Levy

Lemma and_false_false_or : ∀ B C Γ, ((B ∧C )⇒⊥) :: Γ ⊢ (B ⇒⊥)∨(C ⇒⊥).

Lemma not_not_eq: ∀ Γ A, Γ ⊢ A → Γ ⊢ ¬(¬A ).

Lemma not_not_eq'': ∀ Γ A, (¬(¬A )) :: Γ ⊢ A.

Lemma not_not_eq'''': ∀ Γ A, ((¬A )⇒⊥) :: Γ ⊢ A.

Lemma and_false_false_or' : ∀ B C Γ, (¬(B ∧C )) :: Γ ⊢ (¬B )∨(¬C ).

Exo 47, partie 1

Lemma not_or_and_not_1 : ∀ B C Γ, (B ∨ C ⇒ ⊥):: Γ ⊢ B ⇒⊥.

Exo 47, partie 2

Lemma not_or_and_not_2 : ∀ B C Γ, (B ∨ C ⇒ ⊥) :: Γ ⊢ C ⇒⊥.

Exo 47, partie 1, avec le not

Lemma not_or_and_not_1' : ∀ B C Γ, (¬(B ∨ C )) :: Γ ⊢ ¬B.

Exo 47, partie 2

Lemma not_or_and_not_2' : ∀ B C Γ, (¬(B ∨ C )) :: Γ ⊢ ¬C.

exo 48 Levy (1)

Lemma not_imp: ∀ B C Δ, ((B ⇒ C ) ⇒ ⊥) :: Δ ⊢ B.

exo 48 Levy (2)

Lemma not_imp2: ∀ B C Δ, ((B ⇒ C ) ⇒ ⊥) :: Δ ⊢ C ⇒ ⊥.

exo 48 Levy (1)

Lemma not_imp': ∀ B C Δ, (¬(B ⇒ C )) :: Δ ⊢ B.

exo 48 Levy (2)

Lemma not_imp2': ∀ B C Δ, (¬(B ⇒ C )) :: Δ ⊢ ¬C.

Correction de la déduction naturelle

Preuve de correction de la déduction naturelle vis-à-vis de la sémantique définie dans le chapitre Logique propositionnelle avec variables.

Lemma soundness : ∀ Γ p, Γ ⊢ p → Γ ⊧ p.

Préliminaires de la Preuve de complétude de la déduction naturelle

Mesure sur une formule seule

Function mesure (p :formule){struct p}:nat :=
  match p with
      ⊤ ⇒ 1
    | ⊥ ⇒ 0
    | Var _ =>1
    | ¬ φ₂ ⇒ mesure(φ₂)+1
    | φ₂ ⇒ p2 ⇒ mesure(φ₂)+mesure(p2)+1
    | φ₂ ∨ p2 ⇒ mesure(φ₂)+mesure(p2)+2
    | φ₂ ∧ p2 ⇒ mesure(φ₂)+mesure(p2)+1
  end.

Définition de la mesure sur Γ⊢φ en vue de l'induction

Fonctino uxiliaire à la suivante.

Definition add_mesure := (fun e acc ⇒ mesure e + acc).

Mesure sur un environnement. On utilisera cette définition sur φ::Γ pour définir la mesure sur Γ⊢φ. On additionne les mesures de toutes les formules de Γ.

Definition gammaMesure (gamma :env):nat :=
ENV.fold _ add_mesure gamma 0.

Definition de la relation d'ordre sur les environnement induite par la mesure.

Definition gammaLt (n m:env) := gammaMesure n < gammaMesure m.

Cette relation est bien fondée.

Lemma gammaLt_wf : well_founded gammaLt.

⊥ est le minimum pour cette mesure.

Lemma mesure_not_false : ∀ C, C ≠ ⊥ → mesure C > 0.

Quelques preuve de compatibilité de la mesure

en vue de permettre les opérations de remplacement (rewrite, symmetry etc)}

L'ordre des formules dans Γ n'est pas significatif.

Lemma add_mesure_comm:
  ∀ (k k' : formule) (a : ℕ),
    add_mesure k (add_mesure k' a) = add_mesure k' (add_mesure k a).

Add Morphism add_mesure
    with signature Logic.eq ==> Logic.eq ==> Logic.eq as add_mesure_morphism.

Add Morphism gammaMesure
    with signature ENV.eq ==> Logic.eq as gamma_mesure_morphism.

Lemma transp_add_mesure : ENV.transpose_neqkey nat Logic.eq add_mesure.

Lemma gammaMesure_congru:
  ∀ A Γ, gammaMesure (A :: Γ) = add_mesure A (gammaMesure Γ) .

Lemmes auxiliaires sur consequance_set.

Lemma conseqset_andl: ∀ {Γ B C}, Γ ⊧ B ∧C → Γ ⊧ B.

Lemma conseqset_andr: ∀ {Γ B C}, Γ ⊧ B ∧C → Γ ⊧ C.

Lemma conseqset_impe2: ∀ {Γ B C}, Γ ⊧ B ⇒C → B :: Γ ⊧ C.

Lemma conseqset_or_notl: ∀ {Γ B C}, Γ ⊧ B ∨C → (B ⇒⊥) :: Γ ⊧ C.

Lemma conseqset_lande:
  ∀ {Γ Γ' B C D},
    Γ' == (B ∧C) :: Γ → Γ' ⊧ D → (B :: (C :: Γ)) ⊧ D.

Lemma conseqset_neg: ∀ Γ φ, Γ ⊧ ¬φ → (φ :: Γ ) ⊧ ⊥.

Lemma conseqset_or_l:
  ∀ {Γ Γ' B C D}, Γ' == (B ∨C) :: Γ → Γ' ⊧ D → B :: Γ ⊧ D.

Lemma conseqset_or_r:
  ∀ {Γ Γ' B C D}, Γ' == (B ∨C) :: Γ → Γ' ⊧ D → C :: Γ ⊧ D.

Lemma conseqset_imp_l:
  ∀ {Γ Γ' B C D}, Γ' == (B ⇒C) :: Γ → Γ' ⊧ D → C :: Γ ⊧ D.

Lemma conseqset_imp_r:
  ∀ {Γ Γ' B C D}, Γ' == (B ⇒C) :: Γ → Γ' ⊧ D → (¬B) :: Γ ⊧ D.

Lemma conseqset_notand_l':
  ∀ {Γ Γ' B C D}, Γ' == (¬(B ∧C )) :: Γ → Γ' ⊧ D → (¬B) :: Γ ⊧ D.

Lemma conseqset_notand_r':
  ∀ {Γ Γ' B C D}, Γ' == (¬(B ∧C )) :: Γ → Γ' ⊧ D → (¬C) :: Γ ⊧ D.

Lemma conseqset_notor':
  ∀ {Γ Γ' B C D}, Γ' == (¬(B ∨C )) :: Γ → Γ' ⊧ D → (¬B) :: (¬C) :: Γ ⊧ D.

Lemma conseqset_notimp':
  ∀ {Γ' B C A}, (¬(B ⇒ C )) :: Γ' ⊧ A → B :: (¬C) :: Γ' ⊧ A.

Lemma conseqset_notimp'':
  ∀ {Γ' B C A}, (¬¬B) :: Γ' ⊧ A → B :: (¬C) :: Γ' ⊧ A.

Lemma conseqset_notimp''':
  ∀ {Γ' B C A}, ((¬B ) ⇒⊥) :: Γ' ⊧ A → B :: (¬C) :: Γ' ⊧ A.

Lemma conseqset_notand_l:
  ∀ {Γ Γ' B C D}, Γ' == ((B ∧C )⇒⊥) :: Γ → Γ' ⊧ D → (B ⇒ ⊥) :: Γ ⊧ D.

Lemma conseqset_notand_r:
  ∀ {Γ Γ' B C D}, Γ' == ((B ∧C )⇒⊥) :: Γ → Γ' ⊧ D → (C ⇒ ⊥) :: Γ ⊧ D.

Lemma conseqset_notor:
  ∀ {Γ Γ' B C D},
    Γ' == ((B ∨C )⇒⊥) :: Γ
    → Γ' ⊧ D
    → (B ⇒ ⊥) :: (C ⇒ ⊥) :: Γ ⊧ D.

Lemma conseqset_notimp:
  ∀ {Γ' B C A}, ((B ⇒ C ) ⇒ ⊥) :: Γ' ⊧ A → B :: (C ⇒ ⊥) :: Γ' ⊧ A.

Notion de formule atomique, litéral, etc

La preuve de complétude de la déduction naturelle fait appel à de nombreux cas de base sur les litéraus et formules atomiques. Les notions nécessaires sont définies dans cette section.

Toutes les formes atomiques de formules, sur-ensemble des litéraux au sens de Levy. les deux définitions ci-après forment une partition de celui-ci.

Le sous-ensemble des atomes qui ne sont pas des litéraux au sens de Levy. Il s'agit des trois versions atomiques de false.

Inductive is_atom_non_literal: formule → Prop :=
| Atomnl_not_true: is_atom_non_literal (¬⊤)
| Atomnl_false: is_atom_non_literal ⊥
| Atomnl_not_true2: is_atom_non_literal (⊤ ⇒ ⊥).

Les littéraux au sens de Levy, un sous ensemble des atomes.

Inductive is_literal: formule → Prop :=
| Literal_var: ∀ n, is_literal (Var n)
| Literal_not: ∀ n, is_literal (¬ (Var n ))
| Literal_not2: ∀ n, is_literal ((Var n ) ⇒ ⊥)
| Literal_true: is_literal ⊤
| Literal_not_false: is_literal (¬⊥)
| Literal_not_false2: is_literal (⊥ ⇒ ⊥).

Lemma literal_in_atom : ∀ φ, is_literal φ → is_atom φ.

Les atomes sont soit des is_literal soit des is_atom_non_literal.

Lemma atom_in_literal_ln :
∀ φ,
is_atom φ → is_literal φ ∨ is_atom_non_literal φ.

la disjonction correspondant aux formules non atomiques.

Definition disjunction_non_literal_formula φ :=
  (∃ ψ, ∃ ψ',
              φ = (ψ ∧ ψ')
              ∨ φ = (ψ ∨ ψ')
              ∨ (φ = (ψ ⇒ ψ') ∧ ψ' ≠ ⊥)
              ∨ φ = ((ψ ∧ ψ') ⇒ ⊥)
              ∨ φ = ((ψ ∨ ψ') ⇒ ⊥)
              ∨ φ = ((ψ ⇒ ψ') ⇒ ⊥)
              ∨ φ = (¬(ψ ∧ ψ'))
              ∨ φ = (¬(ψ ∨ ψ'))
              ∨ φ = (¬(ψ ⇒ ψ')))
  ∨ (∃ ψ, φ = (¬ (¬ ψ )) ∨ φ = ((¬ ψ ) ⇒ ⊥)).

Preuve que disjunction_non_literal_formula contient bien les formule non-atomique.

Lemma disjunction_non_literal_formula_ok:
  ∀ φ,
    is_atom φ ∨
    disjunction_non_literal_formula φ.

Décision de la propriété is_literal

Lemma is_literal_dec : ∀ φ, is_literal φ ∨ ¬ is_literal φ.

Différentes disjonctions sur les termes

La preuve de complétude de la déduction naturelle fait appel à une décomposition par cas sur les termes et sur l'environnement, cette section définit plusieurs disjonctions et propriétés associées.

Definition disjunction_formula φ :=
  (∃ ψ, ∃ ψ', φ = (ψ ∧ ψ') ∨ φ = (ψ ⇒ ψ') ∨ φ = (ψ ∨ ψ'))
  ∨ ((¬ is_literal φ ) ∧ (∃ ψ, φ = ¬ ψ ))
  ∨ is_atom_non_literal φ
  ∨ is_literal φ.
Lemma disjunction_formula_ok : ∀ φ, disjunction_formula φ.

Definition env_disjunction2 Γ :=
  (∃ φ, φ ∈ Γ ∧ disjunction_non_literal_formula φ )
  ∨ (∃ φ, φ ∈ Γ ∧ is_atom_non_literal φ )
  ∨ (∀ ψ, ψ ∈ Γ → is_literal ψ )
  ∨ ENV.Empty Γ.

Lemma env_disjunction_stable_add2 :
  ∀ Γ Γ' n φ, ENV.Add_multiple φ n Γ Γ'
                   → env_disjunction2 Γ
                   → env_disjunction2 Γ'.

Lemma disjunction_gamma2 :
  ∀ Γ:env, env_disjunction2 Γ.

Ceci est plus ou moins la disjonction de Levy utilisé dans la preuve de complétude. Dans le couple Γ⊢φ, nous avons les cas suivants:

Soit φ est une formule composée (∨, ∧, ⇒, négation d'un non litéral)
Soit il existe dans Γ une formule composée (légèrement différente: disjunction_non_literal_formula)
Soit il existe un litéral faux dans Γ (is_atom_non_literal, trois versions , une seule chez Levy)
Γ ne contient que des litéraux et la formule est atomique (litéral ou faux).

Lemma disjunction_gamma_formule :
  ∀ (Γ:env) (φ:formule),
    (∃ ψ ψ', (φ = (ψ ∧ ψ')) ∨ (φ = (ψ ⇒ ψ'))\/ (φ = (ψ ∨ ψ')))
    ∨ ((¬ is_literal φ ) ∧ (∃ ψ, φ = ¬ ψ ))
    ∨ (∃ ψ, ψ ∈ Γ ∧ disjunction_non_literal_formula ψ )
    ∨ (∃ ψ, ψ ∈ Γ ∧ is_atom_non_literal ψ )
    ∨ ((∀ ψ, ψ ∈ Γ → is_literal ψ ) ∧ (is_atom_non_literal φ ))
    ∨ ((∀ ψ, ψ ∈Γ → is_literal ψ ) ∧ is_literal φ ).

Notion d'interprétation caractéristique d'un environnement

Définition de l'interpétation caractéristique d'un environnement Γ

Definition interp_caracteristique (Γ:ENV.t) : nat → bool := fun n⇒ENV.mem (Var n) Γ.
Definition interp_anticaracteristique (Γ:ENV.t) : nat → bool :=
  fun n⇒negb(orb(ENV.mem (¬Var n) Γ) (ENV.mem (Var n ⇒ ⊥) Γ)).

Lemma interp_caracteristique_1_new :
  ∀ Γ,
    (∀ ψ, ψ ∈ Γ → is_literal ψ)
    → ~(∃ n, (Var n)∈ Γ ∧ ((¬Var n) ∈ Γ ∨ (Var n ⇒⊥) ∈ Γ ))
    → est_modele_set (interp_caracteristique Γ) Γ.

Lemma interp_caracteristique_6_new :
  ∀ Γ n, ¬ (Var n) ∈ Γ → interpretation (interp_caracteristique Γ) (Var n) false.

Lemma interp_caracteristique_5_new :
  ∀ Γ n, ¬ (Var n) ∈ Γ → ¬est_modele (interp_caracteristique Γ) (Var n).

Lemma interp_anticaracteristique_1_new :
  ∀ Γ,
    (∀ ψ, ψ ∈ Γ → is_literal ψ)
    → ~(∃ n, (Var n) ∈ Γ
                   ∧ ((¬Var n) ∈ Γ ∨ (Var n ⇒⊥) ∈ Γ ))
    → est_modele_set (interp_anticaracteristique Γ) Γ.

Lemma interp_anticaracteristique_6_new :
  ∀ Γ n, ¬ (¬Var n) ∈ Γ → ¬ (Var n ⇒ ⊥) ∈ Γ
              → ⊧[interp_anticaracteristique Γ ] (Var n ).

Lemma interp_anticaracteristique_not_negb:
  ∀ Γ k,
  interp_def (interp_anticaracteristique Γ) (¬Var k) =
  negb (interp_def (interp_anticaracteristique Γ) (Var k)).

Propriétés des environnements ne contenant que des litéraux

Lemma ex_listeral_contradictoire_dec_new: ∀ Γ,
  (∃ n, (Var n) ∈ Γ ∧ ((¬Var n) ∈ Γ ∨ (Var n ⇒⊥) ∈ Γ ))
  ∨ ~(∃ n, (Var n) ∈ Γ ∧ ((¬Var n)∈ Γ ∨ (Var n ⇒⊥) ∈ Γ )).
Lemma literaux_conseq_false_new:
  ∀ Γ,
    (∀ ψ, ψ ∈ Γ → is_literal ψ)
    → Γ ⊧ ⊥
    → (∃ n, (Var n) ∈ Γ ∧ ((¬ Var n) ∈ Γ ∨ (Var n ⇒⊥) ∈ Γ )).

Lemma literaux_conseq:
  ∀ Γ k,
    (∀ ψ, ψ ∈ Γ → is_literal ψ)
    → Γ ⊧ (Var k )
    → (∃ n, (Var n) ∈ Γ ∧ ((¬ Var n) ∈ Γ ∨ (Var n ⇒ ⊥) ∈ Γ ))
       ∨ (Var k) ∈ Γ.

Lemma literaux_conseq_neg:
  ∀ Γ k,
    (∀ ψ, ψ ∈ Γ → is_literal ψ)
    → Γ ⊧ (¬Var k )
    → (∃ n, (Var n) ∈ Γ ∧ ((¬ Var n) ∈ Γ ∨ (Var n ⇒ ⊥) ∈ Γ ))
       ∨ (¬Var k) ∈ Γ ∨ (Var k ⇒ ⊥) ∈ Γ.

Preuve de la complétude de la déduction naturelle

Preuve de complétude de la déduction naturelle.

Lemma completness : ∀ Γ A, Γ ⊧ A → Γ ⊢ A.
Print Assumptions completness.

This page has been generated by coqdoc