Library PropL

Require Export Base.

Formulas and contexts

Definition var := nat.

Inductive form : Type :=
| Var : var -> form
| Imp : form -> form -> form
| Fal : form.

Definition Not s := Imp s Fal.

Instance form_eq_dec : forall s t:form, dec (s = t).

Fixpoint vars (s : form) : list var :=
  match s with
    | Var x => [x]
    | Imp s t => vars s ++ vars t
    | Fal => nil
  end.

Assignments and Satisfaction

Definition assn := var -> bool.

Fixpoint satis (f : assn) (s : form) : Prop :=
  match s with
    | Var x => f x = true
    | Imp s1 s2 => satis f s1 -> satis f s2
    | Fal => False
  end.

Instance satis_dec : forall f s, dec (satis f s).

Generic Entailment Relations

Section F.

  Variable F:Type.
  Variable E:list F -> F -> Prop.

  Definition Monotonicity : Prop :=
    forall A A' s, A <<= A' -> E A s -> E A' s.

  Definition Reflexivity : Prop :=
    forall A s, s el A -> E A s.

  Definition Cut : Prop :=
    forall A s t, E A s -> E (s ::A) t -> E A t.

  Definition Consistency : Prop :=
    exists s:F , ~E nil s.

End F.

Fixpoint andlist (A:list Prop) : Prop :=
match A with
| P::A' => P /\ andlist A'
| nil => True
end.

Lemma andlistEq (A:list Prop) : andlist A <-> forall s, s el A -> s.

Goal
  let E : list Prop -> Prop -> Prop := fun A s => andlist A -> s in
  Reflexivity E /\ Monotonicity E /\ Cut E /\ Consistency E.

Definition context := list form.

Definition CharImp (E:context -> form -> Prop) : Prop :=
forall A s t, E A (Imp s t) <-> E (s ::A) t.

Definition CharFal (E:context -> form -> Prop) : Prop :=
forall A, E A Fal <-> forall s, E A s.

Definition bsc A s : Prop := forall f, (forall u, u el A -> satis f u) -> satis f s.

Fixpoint subst (sigma : var -> form) (s : form) : form :=
match s with
| Var x => sigma x
| Imp s t => Imp (subst sigma s) (subst sigma t)
| Fal => Fal
end.

Definition Substitution (E:context -> form -> Prop) :=
forall A s sigma, E A s -> E (map (subst sigma) A) (subst sigma s).

Definition EntailRelAllProps (E:context -> form -> Prop) :=
Reflexivity E /\ Monotonicity E /\ Cut E /\ Consistency E
/\ CharImp E /\ CharFal E /\ Substitution E.

Intuitionistic system

Inductive nd : context -> form -> Prop :=
| ndA A s : s el A -> nd A s
| ndII A s t : nd (s ::A) t -> nd A (Imp s t)
| ndIE A s t : nd A (Imp s t) -> nd A s -> nd A t
| ndE A s : nd A Fal -> nd A s.

Goal forall A s t, nd A (Imp s (Imp (Not s) t)).

Goal forall A s t, nd A (Imp s (Imp (Not s) t)).

Lemma ndapp A s u :
  Imp s u el A -> nd A s -> nd A u.

Lemma ndapp1 A s u :
  nd (Imp s u :: A) s -> nd (Imp s u :: A) u.

Lemma ndapp2 A s t u :
  nd (t :: Imp s u :: A) s -> nd (t :: Imp s u :: A) u.

Lemma ndapp3 A s t u v :
  nd (t :: v :: Imp s u :: A) s -> nd (t :: v :: Imp s u :: A) u.

Lemma nd_weak A A' s :
  A <<= A' -> nd A s -> nd A' s.

Lemma ndW A s t :
nd A s -> nd (t ::A) s.

Lemma ndIE_weak A B s t :
  nd B (Imp s t) -> B <<= A -> nd A s -> nd A t.

Lemma ndDN A s :
  nd A s -> nd A (Not (Not s)).

Lemma nd_bool_sound A s :
  nd A s -> bsc A s.

Lemma nd_con : ~ nd nil Fal.

Lemma nd_subst A s sigma : nd A s -> nd (map (subst sigma) A) (subst sigma s).

Classical system

Inductive ndc : context -> form -> Prop :=
| ndcA A s : s el A -> ndc A s
| ndcII A s t : ndc (s ::A) t -> ndc A (Imp s t)
| ndcIE A s t : ndc A (Imp s t) -> ndc A s -> ndc A t
| ndcC A s : ndc (Not s :: A) Fal -> ndc A s.

Lemma ndc_weak A A' s :
  A <<= A' -> ndc A s -> ndc A' s.

Lemma ndcW A s t :
ndc A s -> ndc (t ::A) s.

Lemma ndcE A s :
  ndc A Fal -> ndc A s.

Lemma nd_ndc A s :
  nd A s -> ndc A s.

Lemma ndc_refute A s :
  ndc A s <-> ndc (Not s :: A) Fal.

Goal forall A s, ndc A (Imp (Not (Not s)) s).

Glivenko's theorem

says that from a classical proof of a formula one can obtain an intuitionistic proof of the double negation of the formula. It follows that intuitionistic and classical refutation coincide. The proof is by induction on ndc. For each case one has to show an intuitionistic tautology. Proving the tautologies first in Coq is very helpful. The two more involved tautologies are:

(s -> ~~ t) -> ~~ (s -> t)
~~ (s -> t) -> ~~ s -> ~~ t

Lemma Glivenko A s :
  ndc A s -> nd A (Not (Not s)).

Corollary Glivenko_refute A :
  nd A Fal <-> ndc A Fal.

Corollary nd_embeds_ndc A s :
  ndc A s <-> nd (Not s :: A) Fal.

Intuitionistic Hilbert system

The Hilbert system consists of Modus Ponens and the axioms

K : s -> t -> s
S : (s -> t -> u) -> (s -> t) -> s -> u
E : Fal -> s

We show that Hilbert derivability agrees with ND derivability. The easy direction is from Hilbert to ND. For the other direction we use the deduction theorem hilD.

Definition FK (s t : form) : form :=
  Imp s (Imp t s).

Definition FS (s t u : form) : form :=
  (Imp (Imp s (Imp t u))
       (Imp (Imp s t)
            (Imp s u))).

Inductive hil (A : context) : form -> Prop :=
| hilA s : s el A -> hil A s
| hilK s t : hil A (FK s t)
| hilS s t u : hil A (FS s t u)
| hilE s : hil A (Imp Fal s)
| hilMP s t : hil A (Imp s t) -> hil A s -> hil A t.

Lemma hil_nd A s :
  hil A s -> nd A s.

Lemma hilAK A s t :
  hil A s -> hil A (Imp t s).

Lemma hilAS A s t u :
  hil A (Imp s (Imp t u)) -> hil A (Imp s t) -> hil A (Imp s u).

Lemma hilI A s :
  hil A (Imp s s).

Lemma hilD s A t :
  hil (s ::A) t -> hil A (Imp s t).

Lemma nd_hil A s :
  nd A s -> hil A s.

Theorem hil_iff_nd A s :
  hil A s <-> nd A s.