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.

loglangcoq.logique.logique_generique






Require Import DecidableType.
Require Import Morphisms.
Require Import Setoid.
Require multiset.

Les sytèmes logiques

Ce chapitre décrit des notions communes à toutes les logiques (hormis la logique propositionnelle sans variable qui est trop simple). On se donne une notion de formule, de valuation et d'interprétation et on définit les notions suivantes:
  • modèle
  • conséquence
  • équivalence
  • (in)satisfiabilité
  • tautologie.
On étend ensuite ces notions aux environnements, c'est-à-dire aux (multi-)ensembles de formules.


Les données nécessaires

Une logique consiste en un type des formules et des notions de valuation et d'interprétation.

Un type des formules

  Parameter formule:Type.

Un type des valuations

  Parameter valuation: Type.

Un propriété d'interprétation

Cette propriété prend en paramètre une valuation et attribue une valeur de vérité à une formule.
  Parameter Inline interpretation: valuation ⟶ formule ⟶ bool ⟶ Prop.

La seule propriété exigée est qu'une formule ne peut pas avoir plus d'une interprétation possible.
  Parameter interpretation_unique:
    forall v f b1 b2, interpretation v f b1 ⟶ interpretation v f b2 ⟶ b1= b2.

Vocabulaire: modèle, conséquence logique, équivalence



modèle

la valuation v est un modèle de la formule f si elle permet d'interpréter f en true. Et cela se note "⊧[v] f", en mathématique le v est en indice du symbole ⊧ (⊧ᵥ).

  Definition est_modele v f:= interpretation v f true.
  Notation " '⊧[' v ']' f" := (est_modele v f).


Conséquence logique

f1 a pour conséquence logique f2 si toute valuation v rendant f1 vraie rend égalemet f2 vraie. Autrement tout modèle de f1 est aussi un modèle de f2. Et cela se note f1 ⊧ f2. On peut également trouver: f1, f2,...,fn ⊧ f, qui signifie que toute interprétation rendant simultanément toutes les fᵢ vraies rendent aussi f vraie. Ce qui est donc équivalent en principe à f1 ∧ f2∧...∧fn ⊧ f.

  Definition consequence f1 f2 := forall v, (⊧[v] f1) ⟶ (⊧[v] f2).
  Notation "f1 ⊧ f2" := (consequence f1 f2).

Équivalence logique

f1 est équivalente à f2 si f1 ⊧ f2 et f2 ⊧ f1. Et cela se note f1 ≡ f2.

  Definition equiv f1 f2 := (f1 ⊧ f2) ∧ (f2 ⊧ f1).
  Notation "f1 ≡ f2" := (equiv f1 f2) (at level 180).

Tautologie, formule satisfaisable, insatisfaisable...

Une formule vraie dans toute interprétation est une tautologie, ou formule valide.

  Definition tautologie (f1:formule) := forall v, ⊧[v] f1.
  Notation valide := tautologie (only parsing).

Une formule pour laquelle il existe un modèle est dite satifiable, satisfaisable ou réalisable.

  Definition satisfiable (f1:formule) := exists v, ⊧[v] f1.
  Notation realisable := satisfiable (only parsing).

Si une telle interprétation n'existe pas, c'est-à-dire si la formule est fausse dans toute interprétation, elle est dite insatisfiable, insatisfaisable, ou encore on dit que c'est une antilogie.

  Definition insatisfiable (f1:formule) := forall v, interpretation v f1 false.
  Notation antilogie := insatisfiable (only parsing).

Environnements

Cette partie définit la notion d'environnement c'est-à-dire un ensemble de formule (plus exactement un multi-ensemble: la même formule peut apparaître plusieurs fois. Cette notion sera utilisée par exemple pour la définition de la déduction naturelle, où les jugements sont de la forme Γ ⊢ φ, où Γ est un environnement et φ une formule. On définit les notions de modèle, conséquence, satisfiabilité et insatisfiabilité pour un ensemble de formules.

  Module ENV := multiset.MakeList(F).

Un environnement est un multi-ensemble de formules.

  Definition env := ENV.t.

modèle


  Definition est_modele_set v Γ := forall f, ENV.In f Γ ⟶ ⊧[v] f.
  Notation " '⊧[[' v ']]' G" := (est_modele_set v G).

conséquence


  Definition consequence_set (Γ: env) f2 := forall v, ⊧[[ v ]] Γ ⟶ ⊧[v] f2.
  Notation "Γ '⊧{}' f" := (consequence_set Γ f).

(in)Satisfiabilité


  Definition satisfiable_set Γ := exists v, ⊧[[v]] Γ.
  Definition insatisfiable_set Γ := forall v, ~(⊧[v] Γ).

Un modèle d'une ensemble Γ de formules est également un modèle d'un sous-ensemble de Γ.

  Lemma est_model_set_subset: forall v φ Γ, ⊧[[v]] (ENV.add φ Γ) ⟶ ⊧[[v]] Γ.
  Proof.
    intros v φ Γ H.
    intros φ' h'.
    apply H.
    destruct (F.eq_dec φ' φ).
    - subst.
      apply ENV.in_add_eq.
      assumption.
    - apply <- ENV.in_add_neq;auto.
  Qed.

This page has been generated by coqdoc