Require Export Base.

Formulas and contexts

Definition var := nat.

Inductive form : Type :=
| Var : varform
| Imp : formformform
| Fal : form.

Definition Not s := Imp s Fal.

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

Fixpoint vars (s : form) : list var :=
  match s with
    | Var x[x]
    | Imp s tvars s ++ vars t
    | Falnil

Assignments and Satisfaction

Definition assn := varbool.

Fixpoint satis (f : assn) (s : form) : Prop :=
  match s with
    | Var xf x = true
    | Imp s1 s2satis f s1satis f s2
    | FalFalse

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

Generic Entailment Relations

Section F.

  Variable F:Type.
  (*** E is an entailment relation ***)
  Variable E:list FFProp.

  (*** Structural Properties ***)
  Definition Monotonicity : Prop :=
     A A' s, A <<= A'E A sE A' s.

  Definition Reflexivity : Prop :=
     A s, s el AE A s.

  Definition Cut : Prop :=
     A s t, E A sE (s::A) tE A t.

  Definition Consistency : Prop :=
     s:F, ¬E nil s.

End F.

Fixpoint andlist (A:list Prop) : Prop :=
match A with
| P::A'P andlist A'
| nilTrue

Lemma andlistEq (A:list Prop) : andlist A s, s el As.

  let E : list PropPropProp := fun A sandlist As in
  Reflexivity E Monotonicity E Cut E Consistency E.

(*** Entailment Relations for form ***)
Definition context := list form.

(*** Logical Properties ***)
Definition CharImp (E:contextformProp) : Prop :=
A s t, E A (Imp s t) E (s::A) t.

Definition CharFal (E:contextformProp) : Prop :=
A, E A Fal s, E A s.

Definition bsc A s : Prop := f, ( u, u el Asatis f u) → satis f s.

Fixpoint subst (sigma : varform) (s : form) : form :=
match s with
| Var xsigma x
| Imp s tImp (subst sigma s) (subst sigma t)
| FalFal

Definition Substitution (E:contextformProp) :=
A s sigma, E A sE (map (subst sigma) A) (subst sigma s).

Definition EntailRelAllProps (E:contextformProp) :=
Reflexivity E Monotonicity E Cut E Consistency E
  CharImp E CharFal E Substitution E.

Intuitionistic system

Inductive nd : contextformProp :=
| ndA A s : s el And A s
| ndII A s t : nd (s::A) tnd A (Imp s t)
| ndIE A s t : nd A (Imp s t) → nd A snd A t
| ndE A s : nd A Falnd A s.

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

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

Lemma ndapp A s u :
  Imp s u el And A snd A u.

Lemma ndapp1 A s u :
  nd (Imp s u :: A) snd (Imp s u :: A) u.

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

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

Lemma nd_weak A A' s :
  A <<= A'nd A snd A' s.

Lemma ndW A s t :
 nd A snd (t::A) s.

Lemma ndIE_weak A B s t :
  nd B (Imp s t) → B <<= And A snd A t.

Lemma ndDN A s :
  nd A snd A (Not (Not s)).

Lemma nd_bool_sound A s :
  nd A sbsc A s.

Lemma nd_con : ¬ nd nil Fal.

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

Classical system

Inductive ndc : contextformProp :=
| ndcA A s : s el Andc A s
| ndcII A s t : ndc (s::A) tndc A (Imp s t)
| ndcIE A s t : ndc A (Imp s t) → ndc A sndc A t
| ndcC A s : ndc (Not s :: A) Falndc A s.

Lemma ndc_weak A A' s :
  A <<= A'ndc A sndc A' s.

Lemma ndcW A s t :
 ndc A sndc (t::A) s.

Lemma ndcE A s :
  ndc A Falndc A s.

Lemma nd_ndc A s :
  nd A sndc A s.

Lemma ndc_refute A s :
  ndc A s ndc (Not s :: A) Fal.

(*** Exercise ***)
Goal 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 snd 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) : formProp :=
| hilA s : s el Ahil 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 shil A t.

Lemma hil_nd A s :
  hil A snd A s.

Lemma hilAK A s t :
  hil A shil 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) thil A (Imp s t).

Lemma nd_hil A s :
  nd A shil A s.

Theorem hil_iff_nd A s :
  hil A s nd A s.