Creative Commons License Copyright Pierre Courtieu et Olivier Pons. This work is licensed under a Creative Commons Attribution-NonCommercial-ShareAlike 4.0 International public License.

logique_propositionnelle_avec_variables







Ce module formalise la logique propositionnelle (avec variable propositionnelle).


Le formules propositionnelle avec variables propositionnelles

Définition des formules

Les formules sont définies (par induction) par la grammaire suivante.

Inductive formule : Type :=
| Vrai: formule
| Faux: formule
| Var: ℕ ⟶ formule
On désigne les variables par des entiers.
| Non: formule ⟶ formule
| Ou: formule ⟶ formule ⟶ formule
| Et: formule ⟶ formule ⟶ formule
| Implique: formule ⟶ formule ⟶ formule.

Exemples de formules sans notation


Check Vrai.
Check Faux.
Check (Var 23).
Check (Ou Vrai Vrai).
Check (Ou Faux Vrai).
Check (Ou (Ou Vrai Faux) Vrai).

Notations usuelles



Notation "⊤":= Vrai.
Notation "⊥":= Faux.
Notation "¬ X":= (Non X).
Notation "X ∨ Y":= (Ou X Y).
Notation "X ∧ Y":= (Et X Y).
Notation "X ⇒ Y":= (Implique X Y).

Les variables seront également plus lisibles en notant le numéro de la variable en indice de la lettre X ('x' majuscule).

Notation "´X1´":= (Var 1).
Notation "´X2´":= (Var 2).

Exemples avec les notations usuelles


Check ⊤.
Check ⊥.
Check X7.
Check (⊤ ∨ ⊤).
Check (⊤ ∨ X3).
Check (X9 ∨ X2).
Check ((⊤ ∨ X4) ∨ ⊤).

Interprétation d'une formule (Sémantique)

Définition de l'interprétation d'une formule

Définition de l'interprétation d'une formule. Pour interpréter les variables propositionnelles on a besoin d'une valuation v des variables vers les valeurs de vérité (bool), ensuite on applique les tables de vérité des feuilles jusqu'à la racine comme le calcul propositionnel.

Function interp_def (v:nat ⟶ bool) (f:formule) : bool :=
  match f with
    | ⊤ => table_Vrai
    | ⊥ => table_Faux
    | Var i => v i
    | ¬ f => table_Non (interp_def v f)
    | f1 ∨ f2 => table_Ou (interp_def v f1) (interp_def v f2)
    | f1 ∧ f2 => table_Et (interp_def v f1) (interp_def v f2)
    | f1 ⇒ f2 => table_Implique (interp_def v f1) (interp_def v f2)
  end.

quelques exemples

Voir plus bas pour plus d'exemples.

  Eval compute in interp_def (fun x => true) (Implique ⊤ (Ou ⊤ ⊥)).
→ true

  Eval compute in interp_def (fun x => false) (Implique ⊤ (Ou ⊤ ⊥)).
→ true

  Eval compute in interp_def (fun x => false) (Implique ⊤ (Ou ⊥ ⊥)).
→ false

  Definition val_X1_true := (fun x => match x with 1 => true | _ => false end).

  Definition val_X1_false := (fun x => match x with 1 => false | _ => false end).

  Eval compute in interp_def val_X1_true (Implique ⊤ (Ou ⊥ X1)).
→ true

  Eval compute in interp_def val_X1_false (Implique ⊤ (Ou ⊥ X1)).
→ false


Version optimisée qui n'évalue la sous-formule de droite que si nécessaire.

Function interp (v:nat ⟶ bool) (f:formule) : bool :=
  match f with
    | ⊤ => true
    | ⊥ => false
    | Var i => v i
    | ¬f => if interp v f then false else true
    | f1 ∨ f2 => if interp v f1 then true else interp v f2
    | f1 ∧ f2 => if interp v f1 then interp v f2 else false
    | f1 ⇒ f2 => if interp v f1 then interp v f2 else true
  end.

Preuve de correction de la version optimisée.


Lemma interp_correct: forall I:ℕ ⟶ bool,forall f:formule, interp_def I f = interp I f.

Exemples d'interprétations

  Definition v1 (n:nat): bool :=
    match n with
      | 1 => true
      | 2 => false
      | 3 => true
      | _ => false
    end.

  Definition v2 (n:nat): bool :=
    match n with
      | 1 => false
      | 2 => true
      | 3 => true
      | _ => false
    end.

  Eval compute in interp_def v1 (Implique Vrai (Ou Vrai Faux)).
→ true

  Eval compute in interp_def v2 (Implique Vrai (Ou Vrai Faux)).
→ true

  Eval compute in interp_def v1 (Implique Vrai (Ou Faux Faux)).
→ false

  Eval compute in interp_def v2 (Implique Vrai (Ou Faux Faux)).
→ false

  Eval compute in interp_def v1 X2.
→ false

  Eval compute in interp_def v1 X2.
→ false

  Eval compute in interp_def v2 X2.
→ true

  Eval compute in interp_def v1 (Implique X1 (Ou Faux Faux)).
→ false

  Eval compute in interp_def v2 (Implique X1 (Ou Faux Faux)).
→ true

  Eval compute in interp v1 (Implique Vrai (Ou Vrai Faux)).
→ true

  Eval compute in interp v2 (Implique Vrai (Ou Vrai Faux)).
→ true

  Eval compute in interp v1 (Implique Vrai (Ou Faux Faux)).
→ false

  Eval compute in interp v2 (Implique Vrai (Ou Faux Faux)).
→ false

  Eval compute in interp v1 X2.
→ false

  Eval compute in interp v1 X2.
→ false

  Eval compute in interp v2 X2.
→ true

  Eval compute in interp v1 (Implique X1 (Ou Faux Faux)).
→ false

  Eval compute in interp v2 (Implique X1 (Ou Faux Faux)).
→ true


Conséquence, modèle etc

On applique les définitions de conséquence, modèle etc du chapitre logique_generique avec les notions de valuation et d'interprétation ci-dessous.


  Definition valuation: Type:= ℕ ⟶ bool.

Dans la suite on écrira interpretation v φ b plutôt que interp_def v φ = b.

  Definition interpretation := fun v φ b => interp_def v φ = b.


Résultat supplémentaire: l'interprétation est décidable. Ce ne sera pas le cas pour la logique des prédicats avec quantificateurs

  Lemma interpretation_dec:
    forall v φ, interpretation v φ true ∨ interpretation v φ false.


Une autre définition pour l'équivalence: l'interprétation des deux formules est toujours identique.

Definition equivalent φ1 φ2 :=
  forall I b, (interpretation I φ1 b)<->(interpretation I φ2 b).

Preuve d'equivalence entre les deux notions d'équivalence.

Lemma equivEquivalence :forall φ1 φ2,(DEFS.equiv φ1 φ2) ↔ (equivalent φ1 φ2).

Exemple de modèles et de conséquences


  Lemma modele1 : forall v, ⊧[v] X1 ∨ ¬ X1.

  Lemma modele2 : forall v, ⊧[v] (X1 ∨ ¬ X2) ∨ X2.

  Lemma conseq1: (X1∨¬X2) ∧ X2 ⊧ X1.


Preuves d'équivalences entre formules


Lemma eq_implique : forall φ ψ : formule, φ ⇒ ψ ≡ ¬φ ∨ ψ.

Lemma eq_et : forall φ ψ: formule, (φ ∧ ψ) ≡ ¬ (¬φ ∨ ¬ψ).

Lemma eq_not_true : ⊥ ≡ ¬ ⊤.

Lemma eq_not_false : ⊤ ≡ ¬ ⊥.


Réduction des connecteurs au sous-ensemble {⊤,¬,∨}

Fonction qui remplace les formules contenant les autres connecteurs par des formule équivalentes.

Function reduce (f:formule) : formule :=
  match f with
    | ⊤ => ⊤
    | ⊥ => ¬ ⊤
    | Var i => Var i
    | ¬ f => ¬ (reduce f)
    | f1 ∨ f2 => (reduce f1) ∨ (reduce f2)
    | f1 ∧ f2 => ¬ (¬ (reduce f1) ∨ ¬ (reduce f2))
    | f1 ⇒ f2 => ¬ (reduce f1) ∨ (reduce f2)
  end.

Lemma reduce_correct:
  forall v, forall f:formule, interp_def v f = interp_def v (reduce f).

Lemma reduce_equiv : forall f:formule, f ≡ (reduce f).

Propriété d'être formé uniquement avec des ¬, ∨ et ⊤ ou Var.

Inductive is_reduced : formule ⟶ Prop :=
  Vrai_is_red: is_reduced ⊤
| Var_is_red: forall i, is_reduced (Var i)
| Non_is_red: forall f,is_reduced f ⟶ is_reduced (¬ f)
| Or_is_red: forall f g,is_reduced f ⟶ is_reduced g ⟶ is_reduced (f ∨ g).

la fonction reduce retourne bien une formule de cette forme.

Lemma reduce_complete : forall f, is_reduced (reduce f).

Preuve par réfutation (Utile pour la preuve par tableau plus loin).


Lemma conseq_by_contradiction´: forall f1 f2: formule, f1 ⊧ f2 ⟶ f1 ∧ ¬f2 ⊧ ⊥.

Pour prouver f ⊧ g on peut prouver f ∧ ¬g ⊧ ⊥.

Lemma conseq_by_contradiction: forall f1 f2: formule, f1 ∧ ¬f2 ⊧ ⊥ ⟶ f1 ⊧ f2.

Preuve par la méthode des tableaux

Lemmes auxilaires


Lemma and_affaiblissement_conseq : forall v f1 f2, ⊧[v] f1∧f2 ⟶ ⊧[v]f1.

Lemma and_affaiblissement_contr : forall f1 f2, f1 ⊧ ⊥ ⟶ f1∧f2 ⊧ ⊥.

Lemma Et_sym : forall f1 f2, f1 ∧ f2 ≡ f2 ∧ f1.

Lemma Et_assoc : forall f1 f2 f3, f1 ∧ (f2 ∧ f3) ≡ (f1 ∧ f2) ∧ f3.

Function extraction_disjuntion (f F: formule): option formule :=
  match F with
    | g ∧ F´ =>
      if formule_eq_dec f g then Some F´
      else
        if formule_eq_dec f F´ then Some g
        else
          match extraction_disjuntion f F´ with
              None => None
            | Some F´´ => Some (g ∧ F´´)
          end
    | g => if formule_eq_dec f g then Some ⊤ else None
  end.

Eval compute in (extraction_disjuntion (¬X1) (((X1 ∨ ¬X2) ∧ X2) ∧ ¬X1 ∧ X2)).
Eval compute in (extraction_disjuntion (¬X1) (((X1 ∨ ¬X2) ∧ X2) ∧ ¬X1)).
Eval compute in (extraction_disjuntion ((X1 ∨ ¬X2) ∧ X2) (((X1 ∨ ¬X2) ∧ X2) ∧ ¬X1)).

Lemma Et_et_true : forall f, f ≡ f ∧ ⊤.

Lemma extraction_disjuntion_ok :
  forall f F F´, extraction_disjuntion f F = Some F´ ⟶ (F ≡ f ∧ F´).

Les règles des tableaux


Lemma tableau_Ou :
  forall F f1 f2, ((f1 ∧ F ⊧ ⊥) ∧ (f2 ∧ F ⊧ ⊥)) ⟶ (f1 ∨ f2) ∧ F ⊧ ⊥.

Lemma tableau_Ou´ : forall f1 f2, (f1 ⊧ ⊥) ∧ (f2 ⊧ ⊥) ⟶ (f1 ∨ f2) ⊧ ⊥.

Lemma tableau_nonEt:
  forall F f1 f2, (¬f1 ∧ F ⊧ ⊥) ∧ (¬f2 ∧ F ⊧ ⊥) ⟶ ¬(f1 ∧ f2) ∧ F ⊧ ⊥.

Lemma tableau_nonEt´ : forall f1 f2, (¬f1 ⊧ ⊥) ∧ (¬f2 ⊧ ⊥) ⟶ ¬(f1 ∧ f2) ⊧ ⊥.

Lemma tableau_implique :
  forall F f1 f2, (¬f1 ∧ F ⊧ ⊥) ∧ (f2 ∧ F ⊧ ⊥) ⟶ (f1 ⇒ f2) ∧ F ⊧ ⊥.

Lemma tableau_implique´ : forall f1 f2, (¬f1 ⊧ ⊥) ∧ (f2 ⊧ ⊥) ⟶ (f1 ⇒ f2) ⊧ ⊥.

Lemma tableau_Et: forall F f1 f2, f1 ∧ f2 ∧ F ⊧ ⊥ ⟶ (f1 ∧ f2) ∧ F ⊧ ⊥.


Lemma tableau_nonimplique : forall F f1 f2, f1 ∧ ¬f2 ∧ F ⊧ ⊥ ⟶ ¬(f1 ⇒ f2) ∧ F ⊧ ⊥.

Lemma tableau_nonimplique´ : forall f1 f2, f1 ∧ ¬f2 ⊧ ⊥ ⟶ ¬(f1 ⇒ f2) ⊧ ⊥.

Lemma tableau_nonOu : forall F f1 f2, ¬f1 ∧ ¬f2 ∧ F ⊧ ⊥ ⟶ ¬(f1 ∨ f2) ∧ F ⊧ ⊥.

Lemma tableau_nonOu´ : forall f1 f2, ¬f1 ∧ ¬f2 ⊧ ⊥ ⟶ ¬(f1 ∨ f2) ⊧ ⊥.

Lemma tableau_ferme_branche : forall F f, (F ∧ f) ∧ ¬f ⊧ ⊥.

Lemma tableau_ferme_branche´ : forall F f, f ∧ ¬f ∧ F ⊧ ⊥.

Lemma tableau_ferme_branche´´ : forall F f, (f ∧ ¬f) ∧ F ⊧ ⊥.

Lemma p_et_p_eq : forall p, p∧p ≡ p.


Exemples d'application des tableaux.


Lemma conseq1: (X1∨¬X2) ∧ X2 ⊧ X1.
Proof.
  apply conseq_by_contradiction.
  do_Et (X1 ∨ ¬X2) X2.
  do_Ou X1 (¬X2).
  - do_ferme X1.
  - do_ferme X2.
Qed.

  Lemma conseq2 : (X1 ∧ X3 ) ∧ (¬X1 ∨ X2) ⊧ ⊥.
Proof.
  do_Ou (¬X1) X2.
  - do_ferme X1.
Echec
Abort.

Lemma conseq3 : (¬ (X1 ⇒ (X2 ⇒ X1))) ∧ ⊤ ⊧ ⊥.
Proof.
  do_NonImplique X1 (X2 ⇒ X1).
  do_NonImplique X2 X1.
  do_ferme X1.
Qed.

Lemma conseq4 : (¬ (X1 ∨ X2)) ∧ X1 ⊧ ⊥.
Proof.
  do_nonOu X1 X2.
  do_ferme X1.
Qed.

Lemma conseq5 : (¬ (X1 ∧ X2)) ∧ X1 ∧ X2 ⊧ ⊥.
Proof.
  do_nonEt X1 X2.
  - do_ferme X1.
  - do_ferme X2.
Qed.

Lemma conseq_exam_2014 : (¬X2∨¬X3) ⊧ (X2 ∧ X3) ⇒ X1.
Proof.
  apply conseq_by_contradiction.
  do_NonImplique (X2 ∧ X3) (X1).
  do_Et (X2)(X3).
  do_Ou (¬X2) (¬X3).
  - do_ferme X2.
  - do_ferme X3.
Qed.

Lemma conseq6 : (X1 ∨ X2)∧(¬X1 ∧ ¬X2) ⊧ ⊥.
Proof.

    do_Ou X1 X2.
    - do_ferme X1.
    - do_ferme X2.
Qed.

Lemma conseq7 : ⊤ ⊧ (X1 ⇒ (X2 ⇒ X3)) ⇒ ((X1 ⇒ X2) ⇒ (X1 ⇒ X3)).
  Proof.
  apply conseq_by_contradiction.
  do_NonImplique (X1 ⇒ (X2 ⇒ X3)) ((X1 ⇒ X2) ⇒ (X1 ⇒ X3)).
  do_Implique X1 (X2 ⇒ X3).
  - do_NonImplique (X1 ⇒ X2) (X1 ⇒ X3).
    do_Implique X1 X2.
    + do_NonImplique X1 X3.
      do_ferme X1.
    + do_NonImplique X1 X3.
      do_ferme X1.
  - do_NonImplique (X1 ⇒ X2) (X1 ⇒ X3).
    do_Implique X1 X2.
    + do_NonImplique X1 X3.
      do_ferme X1.
    + do_Implique X2 X3.
       × do_ferme X2.
       × do_NonImplique X1 X3.
         do_ferme X3.
Qed.

This page has been generated by coqdoc