logique_generique

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 notion aux environnements, c'est-à-dire aux (multi-)ensembles de formules.

Les données nécessaires

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

Un type des formules

Parameter formule:Type.

Un type des valuation

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:
∀ 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

f₁ a pour conséquence logique f₂ si toute valuation v rendant f₁ vraie rend égalemet f₂ vraie. Autrement tout modèle de f₁ est aussi un modèle de f₂. Et cela se note f₁ ⊧ f₂. On peut également trouver: f₁, f₂,...,f_n ⊧ 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 à f₁ ∧ f₂∧...∧f_n ⊧ f.

Definition consequence f₁ f₂ := ∀ v, (⊧[v ] f₁) → (⊧[v ] f₂).
Notation "f₁ ⊧ f₂" := (consequence f₁ f₂).

Équivalence logique

f₁ est équivalente à f₂ si f₁ ⊧ f₂ et f₂ ⊧ f₁. Et cela se note f₁ ≡ f₂.

Definition equiv f₁ f₂ := (f₁ ⊧ f₂ ) ∧ (f₂ ⊧ f₁ ).
Notation "f₁ ≡ f₂" := (equiv f₁ f₂) (at level 180).

Tautologie, formule satisfaisable, insatisfaisable...

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

Definition tautologie (f₁:formule) := ∀ v, ⊧[v ] f₁.
Notation valide := tautologie (only parsing).

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

Definition satisfiable (f₁:formule) := ∃ v, ⊧[v ] f₁.
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 (f₁:formule) := ∀ v, interpretation v f₁ 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 Γ := ∀ f, ENV.In f Γ → ⊧[v ] f.
Notation " ´⊧[[´ v ´]]´ G" := (est_modele_set v G).

conséquence

Definition consequence_set (Γ: env) f₂ := ∀ v, ⊧[[ v ]] Γ → ⊧[v ] f₂.
Notation "Γ ´⊧{}´ f" := (consequence_set Γ f).

(in)Satisfiabilité

Definition satisfiable_set Γ := ∃ v, ⊧[[v ]] Γ.
Definition insatisfiable_set Γ := ∀ 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: ∀ v φ Γ, ⊧[[v ]] (ENV.add φ Γ ) → ⊧[[v ]] Γ.

This page has been generated by coqdoc