ICL.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).

Proof. unfold dec. repeat decide equality. Qed.

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).

Proof.
  intros f s. induction s as [x|s IHs t IHt|]; simpl; auto.
Qed.

Generic Entailment Relations

Section F.

  Variable F:Type.
  (*** E is an entailment relation ***)
  Variable E:list F -> F -> Prop.

  (*** Structural Properties ***)
  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.
Proof.
  induction A; simpl; try tauto. split.
  - intros [B C] s [D|D]; try congruence. now apply IHA.
  - intros B. split.
    + apply B. tauto.
    + apply IHA. intros s C. apply B. tauto.
Qed.

Goal
  let E : list Prop -> Prop -> Prop := fun A s => andlist A -> s in
  Reflexivity E /\ Monotonicity E /\ Cut E /\ Consistency E.
Proof.
  intros E. repeat split.
  - intros A s B C. revert s B. now apply andlistEq.
  - intros A A' s B C D. apply C. apply andlistEq. intros t G. apply B in G. revert t G.
    now apply andlistEq.
  - intros A s t B C D. apply C. split; try assumption. now apply B.
  - exists False. unfold E. simpl. tauto.
Qed.

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

(*** Logical Properties ***)
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)).
Proof.
  intros A s t. apply ndII, ndII. apply ndE. apply ndIE with (s := s).
  - apply ndA. left. reflexivity.
  - apply ndA. right. left. reflexivity.
Qed.

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

Proof.
  intros A s t.
  assert (B:Not s el Not s::s::A) by auto.
  assert (C:s el Not s::s::A) by auto.
  exact (ndII (ndII (ndE t (ndIE (ndA B) (ndA C))))).
Qed.

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

Proof.
  intros E F. apply ndIE with (s := s).
  - apply ndA, E.
  - exact F.
Qed.

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

Proof. apply ndapp. auto. Qed.

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

Proof. apply ndapp. auto. Qed.

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

Proof. apply ndapp. auto. Qed.

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

Proof.
  intros E F. revert A' E.
  induction F as [A s F|A s t F IHF|A s t F1 IHF1 F2 IHF2|A s F IHF] ; intros A' E.
  - apply ndA, E. assumption.
  - apply ndII, IHF. apply incl_shift, E.
  - apply ndIE with (s:=s) ; auto.
  - apply ndE, IHF, E.
Qed.

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

Proof. apply nd_weak; auto. Qed.

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

Proof.
  intros E F G. apply ndIE with (s:=s).
  - exact (nd_weak F E).
  - exact G.
Qed.

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

Proof. intros E. apply ndII, ndapp1, ndW, E. Qed.

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

Proof.
  intros B f.
  induction B as [A s B|A s t B IHB|A s t B1 IHB1 B2 IHB2|A s B IHB]; simpl in *|-*; auto; try tauto.
  intros C D. apply IHB. intros u [E|E]; auto. congruence.
Qed.

Lemma nd_con : ~ nd nil Fal.

Proof.
  intros B. change (satis (fun _ => false) Fal). apply (nd_bool_sound B); simpl; tauto.
Qed.

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

Proof.
  intros B. induction B as [A s B|A s t B IHB|A s t B1 IHB1 B2 IHB2|A s B IHB].
  - apply ndA. apply in_map_iff. eauto.
  - simpl. apply ndII. exact IHB.
  - apply ndIE with (s := subst sigma s); tauto.
  - apply ndE. exact IHB.
Qed.

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.

Proof.
  intros E F. revert A' E.
  induction F as [A s F|A s t F IHF|A s t F1 IHF1 F2 IHF2|A s F IHF] ; intros A' E.
  - apply ndcA, E. assumption.
  - apply ndcII, IHF. apply incl_shift, E.
  - apply ndcIE with (s:=s) ; auto.
  - apply ndcC, IHF. intros t [G|G].
    + rewrite G. left. reflexivity.
    + right. apply E. exact G.
Qed.

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

Proof. apply ndc_weak; auto. Qed.

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

Proof. intros E. apply ndcC, ndcW, E. Qed.

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

Proof.
  intros F ; induction F as [A s F|A s t F IHF|A s t F1 IHF1 F2 IHF2|A s F IHF].
  - apply ndcA. assumption.
  - apply ndcII, IHF.
  - apply ndcIE with (s:=s) ; auto.
  - apply ndcE, IHF.
Qed.

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

Proof.
  split ; intros E.
  - apply ndcIE with (s:=s).
    + apply ndcA. auto.
    + apply ndcW, E.
  - apply ndcC, E.
Qed.

Lemma ndcapp A s u :
  Imp s u el A -> ndc A s -> ndc A u.

Proof.
  intros E F. apply ndcIE with (s := s).
  - apply ndcA, E.
  - exact F.
Qed.

Lemma ndcapp1 A s u :
  ndc (Imp s u :: A) s -> ndc (Imp s u :: A) u.

Proof. apply ndcapp. auto. Qed.

Lemma ndcapp2 A s t u :
  ndc (t :: Imp s u :: A) s -> ndc (t :: Imp s u :: A) u.

Proof. apply ndcapp. auto. Qed.

Lemma ndcapp3 A s t u v :
  ndc (t :: v :: Imp s u :: A) s -> ndc (t :: v :: Imp s u :: A) u.

Proof. apply ndcapp. auto. Qed.

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

Proof.
  intros A s. apply ndcII, ndcC. apply ndcIE with (s:= Not s).
  - apply ndcW, ndcA. auto.
  - apply ndcA. auto.
Qed.

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)).

Proof.
  intros E. induction E as [A s E|A s t E IHE|A s t E1 IHE1 E2 IHE2|A s E IHE].
  - apply ndDN, ndA. assumption.
  - apply ndII, ndapp1.
    apply ndII, ndE. apply (ndIE_weak IHE).
    + auto.
    + apply ndII. apply ndapp3. apply ndII. apply ndA. auto.
  - apply ndII. apply (ndIE_weak IHE2).
    + auto.
    + apply ndII. apply (ndIE_weak IHE1).
      * auto.
      * apply ndII. apply ndapp3. apply ndapp1. apply ndA. auto.
  - apply ndII. apply (ndIE IHE). apply ndII, ndA. auto.
Qed.

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

Proof.
  split.
  - apply nd_ndc.
  - intros E. apply Glivenko in E. apply (ndIE E). apply ndII, ndA. auto.
Qed.

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

Proof. setoid_rewrite ndc_refute. symmetry. apply Glivenko_refute. Qed.

Intuitionistic Hilbert system

The Hilbert system consists of Modus Ponens and the axioms
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.

Proof.
  intros E. induction E as [s E|s t|s t u|s|s t E1 IHE1 E2 IHE2].
  - apply ndA. assumption.
  - apply ndII, ndII, ndA. auto.
  - apply ndII, ndII, ndII.
    apply ndIE with (s:= Imp t u).
    + apply ndII. apply ndapp1. apply ndapp3. apply ndA. auto.
    + apply ndapp3, ndA. auto.
  - apply ndII. apply ndE, ndA. auto.
  - exact (ndIE IHE1 IHE2).
Qed.

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

Proof. apply hilMP. apply hilK. Qed.

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

Proof. intros B. apply hilMP. revert B. apply hilMP. apply hilS. Qed.

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

Proof.
  assert (E:= hilS A s (Imp s s) s).
  assert (F:= hilK A s (Imp s s)).
  assert (G:= hilK A s s).
  unfold FS, FK in *.
  exact (hilMP (hilMP E F) G).
Qed.

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

Proof.
  intros E. induction E as [t E|t u|t u v|t|t u E1 IHE1 E2 IHE2].
  - destruct E as [E|E].
    + subst t. apply hilI.
    + apply hilAK. apply hilA, E.
  - apply hilAK, hilK.
  - apply hilAK, hilS.
  - apply hilAK, hilE.
  - apply hilAS with (t:=t) ; assumption.
Qed.

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

Proof.
  intros E. induction E as [A s E|A s t E IHE|A s t E1 IHE1 E2 IHE2|A s E IHE].
  - apply hilA. assumption.
  - apply hilD, IHE.
  - exact (hilMP IHE1 IHE2).
  - exact (hilMP (hilE A s) IHE).
Qed.

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

Proof. split. apply hil_nd. apply nd_hil. Qed.