Require Export PropL.

Clauses

Inductive sform : Type :=
| Pos : form → sform
| Neg : form → sform.

Definition clause := list sform.

Notation "+ s" := (Pos s) (at level 35).
Notation "- s" := (Neg s).

Instance eq_sform_dec S T :
dec (S = T :> sform).

Definition positive (S : sform) : Prop :=
  match S with +s ⇒ True | -s ⇒ False end.

Fixpoint pos (C : clause) : clause :=
  match C with
    | nil ⇒ nil
    | + s :: C' ⇒ + s :: pos C'
    | - s :: C' ⇒ pos C'
  end.

Lemma pos_iff S C :
  S ∊ pos C ↔ S ∊ C ∧ positive S.

Lemma pos_mono C D :
  C ⊆ D → pos C ⊆ pos D.

Lemma pos_idempotent C :
  pos (pos C) = pos C.

Lemma pos_incl C :
  pos C ⊆ C.

Lemma pos_incl_pos A B :
  pos A ⊆ B → pos A ⊆ pos B.

Models and satisfaction

We consider finite Kripke models whose states are clauses. There is a transition from A to B iff all positive formulas in A are in B. A state is labelled with a variable x if it contains the signed formula +x. We will show that nd is sound and complete for this class of models.

Definition state := clause.
Definition model := list state.

Section Model.
  Variable M : model.
  Implicit Types A B C : state.

  Definition before (A B : state) : Prop :=
    A ∊ M ∧ B ∊ M ∧ pos A ⊆ B.

  Lemma before_refl A :
    A ∊ M → before A A.

  Lemma before_tran A B C :
    before A B → before B C → before A C.

  Lemma before_in s A B :
    before A B → +s ∊ A → +s ∊ B.

  Fixpoint satis (A : state) (s : form) : Prop :=
    match s with
      | Var x ⇒ +Var x ∊ A
      | Imp s t ⇒ ∀ B, before A B → satis B s → satis B t
      | Fal ⇒ False
    end.

  Lemma satis_not A s :
    A ∊ M → satis A (Not s) → ¬ satis A s.

  Lemma satis_mono A B s :
    before A B → satis A s → satis B s.

  Fixpoint satis' (A : state) (C : clause) : Prop :=
    match C with
      | nil ⇒ True
      | +s :: C' ⇒ satis A s ∧ satis' A C'
      | -s :: C' ⇒ ¬ satis A s ∧ satis' A C'
    end.

  Lemma satis_iff A C :
    satis' A C ↔ ∀ S, S ∊ C →
                     match S with
                       | +s ⇒ satis A s
                       | -s ⇒ ¬ satis A s
                     end.

  Lemma satis_in A C S :
    satis' A C → S ∊ C → match S with
                          | +s ⇒ satis A s
                          | -s ⇒ ¬ satis A s
                         end.

  Lemma satis_weak C D A :
    C ⊆ D → satis' A D → satis' A C.

  Global Instance before_forall_dec A p :
    (∀ B, dec (p B)) → dec (∀ B, before A B → p B).

  Global Instance satis_dec A s :
    dec (satis A s).

End Model.

Semantic entailment and soundness

Definition sem (A : context) (s : form) : Prop :=
∀ M B, B ∊ M → (∀ t, t ∊ A → satis M B t) → satis M B s.

Lemma nd_sem A s :
nd A s → sem A s.

Satisfiability

Definition sat (C : clause) : Prop :=
  ∃ M A, A ∊ M ∧ satis' M A C.

Lemma sat_weak C D :
  C ⊆ D → sat D → sat C.

Lemma sem_unsat A s :
  sem A s → ¬ sat (-s :: map Pos A).

Lemma sem_iff_unsat A s :
sem A s ↔ ¬ sat (-s :: map Pos A).

Demos

A demo is a model satisfying certain consistency properties. We will show that every state A of a demo satifies every positive formula in A and dissatifies every negative formula in A.

Definition demo' (M : model) (A : clause) (S : sform) : Prop :=
  match S with
    | - Var x ⇒ ¬ +Var x ∊ A
    | + Imp s t ⇒ -s ∊ A ∨ +t ∊ A
    | - Imp s t ⇒ ∃ B, before M A B ∧ +s ∊ B ∧ -t ∊ B
    | + Fal ⇒ False
    | _ ⇒ True
  end.

Definition demo (M : model) : Prop :=
  ∀ A, A ∊ M → ∀ S, S ∊ A → demo' M A S.

Definition sign (b : bool) :=
  if b then Pos else Neg.

Lemma demo_satis M A b s :
  demo M → A ∊ M → sign b s ∊ A →
  if b then satis M A s else ¬ satis M A s.

Lemma demo_satis' M A :
  demo M → A ∊ M → satis' M A A.

Intuitionistic ND cannot prove double negation

Definition DN x := Imp (Not (Not (Var x))) (Var x).

Section ND_not_DN.
  Variable x : var.
  Let A := [-DN x ; + Not (Not (Var x)); - Not (Var x); -Var x ].
  Let B := [+ Not (Not (Var x)); - Not (Var x); +Var x ; -Fal].
  Let M := [A ; B ].
  Let D : demo M.
  Qed.

  Lemma not_nd_DN : ¬ nd nil (DN x).

End ND_not_DN.

Tableaux

Inductive tab : clause → Prop :=
| tabF C : tab (+Fal :: C)
| tabC (x : var) C : tab (-Var x :: +Var x :: C)
| tabIP s t C : tab (-s :: C) → tab (+ t :: C) → tab (+Imp s t :: C)
| tabIN s t C : tab (+s :: -t :: pos C) → tab (-Imp s t :: C)
| tabW C C' : C' ⊆ C → tab C' → tab C.

Definition uns (S : sform) : form :=
  match S with +s ⇒ s | -s ⇒ Not s end.

Definition ndr (C : clause) : Prop :=
  nd (map uns (pos C)) Fal ∨ ∃ s, -s ∊ C ∧ nd (map uns (pos C)) s.

Lemma tab_ndr C :
  tab C → ndr C.

Lemma uns_Pos A :
  map uns (map Pos A) = A.

Lemma pos_map_Pos A :
  pos (map Pos A) = map Pos A.

Lemma tab_nd A s :
  tab (-s :: map Pos A) → nd A s.

Main results assuming main lemma

Section MainResults.
  Variable main : ∀ C, {sat C } + {tab C }.

  Lemma nd_plus_not_sem A s :
    {nd A s } + {¬ sem A s }.

  Lemma nd_dec A s :
    dec (nd A s).

  Lemma nd_iff_sem A s :
    nd A s ↔ sem A s.

End MainResults.