Require Export PropL.

Clauses

Inductive sform : Type :=
| Pos : formsform
| Neg : formsform.

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 +sTrue | -sFalse end.

Fixpoint pos (C : clause) : clause :=
match C with
| nilnil
| + 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 Dpos 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 Bpos 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 Mbefore A A.

Lemma before_tran A B C :
before A Bbefore B Cbefore 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 Bsatis B ssatis B t
| FalFalse
end.

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

Lemma satis_mono A B s :
before A Bsatis A ssatis B s.

Fixpoint satis' (A : state) (C : clause) : Prop :=
match C with
| nilTrue
| +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
| +ssatis A s
| -s¬ satis A s
end.

Lemma satis_in A C S :
satis' A CS Cmatch S with
| +ssatis A s
| -s¬ satis A s
end.

Lemma satis_weak C D A :
C Dsatis' A Dsatis' A C.

Global Instance before_forall_dec A p :
( B, dec (p B)) → dec ( B, before A Bp 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 Asatis M B t) → satis M B s.

Lemma nd_sem A s :
nd A ssem A s.

Satisfiability

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

Lemma sat_weak C D :
C Dsat Dsat 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
| + FalFalse
| _True
end.

Definition demo (M : model) : Prop :=
A, A M S, S Ademo' M A S.

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

Lemma demo_satis M A b s :
demo MA Msign b s A
if b then satis M A s else ¬ satis M A s.

Lemma demo_satis' M A :
demo MA Msatis' 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 : clauseProp :=
| 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' Ctab C'tab C.

Definition uns (S : sform) : form :=
match S with +ss | -sNot 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 Cndr 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.