Library Logics
This module declares signature for reasoning with abstract logics. It also
defines negated translation and A-translation, thus providing a basis
for interpreting classical logic.
Abstract Higher-Order Logic
Formulas
Parameter
(prop : Type)
(TT FF : prop)
(Not : prop -> prop)
(Imp And Or : prop -> prop -> prop)
(Forall Exist: ∀ {A}, (A -> prop) -> prop)
(Ex2 : ∀ {A}, (A -> prop) -> (A -> prop) -> prop).
(prop : Type)
(TT FF : prop)
(Not : prop -> prop)
(Imp And Or : prop -> prop -> prop)
(Forall Exist: ∀ {A}, (A -> prop) -> prop)
(Ex2 : ∀ {A}, (A -> prop) -> (A -> prop) -> prop).
Inference rules
Parameter
(holds : prop -> Prop)
(rTT : holds TT)
(rFF : ∀ P, holds FF -> holds P)
(rAnd : ∀ P Q, (holds (And P Q) <-> holds P /\ holds Q))
(rImp : ∀ P Q, (holds (Imp P Q) <-> (holds P -> holds Q)))
(rForall : ∀ A P, (holds (Forall P) <-> ∀ x:A, holds (P x)))
(rNot : ∀ P, holds (Not P) <-> (holds P -> holds FF))
(rOrI : ∀ P Q, holds P \/ holds Q -> holds (Or P Q))
(rOrE : ∀ P Q C, (holds P \/ holds Q -> holds C) -> holds (Or P Q) -> holds C)
(rExI : ∀ A P, (exists (x:A), holds (P x)) -> holds (Exist P))
(rExE : ∀ A P C, (∀ x:A, holds (P x) -> holds C) -> holds (Exist P) -> holds C)
(rEx2I : ∀ A (P Q:A->prop), (exists2 x, holds (P x) & holds (Q x)) -> holds (Ex2 P Q))
(rEx2E : ∀ A P Q C, (∀ x:A, holds (P x) -> holds (Q x) -> holds C) ->
holds (Ex2 P Q) -> holds C).
End HOLogic.
(holds : prop -> Prop)
(rTT : holds TT)
(rFF : ∀ P, holds FF -> holds P)
(rAnd : ∀ P Q, (holds (And P Q) <-> holds P /\ holds Q))
(rImp : ∀ P Q, (holds (Imp P Q) <-> (holds P -> holds Q)))
(rForall : ∀ A P, (holds (Forall P) <-> ∀ x:A, holds (P x)))
(rNot : ∀ P, holds (Not P) <-> (holds P -> holds FF))
(rOrI : ∀ P Q, holds P \/ holds Q -> holds (Or P Q))
(rOrE : ∀ P Q C, (holds P \/ holds Q -> holds C) -> holds (Or P Q) -> holds C)
(rExI : ∀ A P, (exists (x:A), holds (P x)) -> holds (Exist P))
(rExE : ∀ A P C, (∀ x:A, holds (P x) -> holds C) -> holds (Exist P) -> holds C)
(rEx2I : ∀ A (P Q:A->prop), (exists2 x, holds (P x) & holds (Q x)) -> holds (Ex2 P Q))
(rEx2E : ∀ A P Q C, (∀ x:A, holds (P x) -> holds (Q x) -> holds C) ->
holds (Ex2 P Q) -> holds C).
End HOLogic.
A logic is consistent if FF cannot be derived
An intuitionistic logic is a logic that embeds all of Prop
prop is isomorphic to Prop up to <->
Parameter Atom : Prop -> prop.
Parameter rAtom : ∀ P, holds (Atom P) <-> P.
End IntuitionisticLogic.
Parameter rAtom : ∀ P, holds (Atom P) <-> P.
End IntuitionisticLogic.
A classical logic is a logic that derives ~~P->P forall all P.
Given a logic, the set of propositions s.t. ~~P->P can be embedded.
Module Type ClassicalLogic (L:HOLogic).
Include HOLogic.
Parameter Atom : ∀ P:L.prop, (((L.holds P->L.holds L.FF)->L.holds L.FF)->L.holds P) -> prop.
Parameter rAtom : ∀ P h, holds (@Atom P h) <-> L.holds P.
Parameter rClassic : ∀ P, holds (Not (Not P)) -> holds P.
End ClassicalLogic.
Negated translation: interpretation of classical propositions in intuitionistic ones.
Require Import Setoid.
Module NegatedTranslation (L:HOLogic) <: ClassicalLogic L.
Notation Fa := (L.holds L.FF).
Record _prop : Type := mkp { nnf : L.prop; nnh : ((L.holds nnf->Fa)->Fa) -> L.holds nnf }.
Definition prop := _prop.
Definition Atom := mkp.
Definition holds P := L.holds(nnf P).
Lemma rAtom P h : holds (@Atom P h) <-> L.holds P.
Definition TT : prop.
exists L.TT.
Defined.
Definition FF : prop.
exists L.FF; auto.
Defined.
Definition Imp (P Q:prop) : prop.
exists (L.Imp (nnf P) (nnf Q)).
Defined.
Definition Not P := Imp P FF.
Definition And (P Q:prop) : prop.
exists (L.And (nnf P) (nnf Q)).
Defined.
Definition Forall {A} (P:A -> prop) : prop.
exists (L.Forall(fun x=> nnf(P x))).
Defined.
Disjunction: alternative def ~(~P/\~Q)
Equivalent since ~~(P\/Q) <-> ~(~P/\~Q) is an
intuitionistic tautology.
Existential: alternative def ~forall x, ~ P x
Equivalent since ~~(exists x, P x) <-> ~forall x, ~ P x is an
intuitionistic tautology.
Definition Exist {A} (P:A->prop) : prop.
exists (L.Not (L.Not (L.Exist(fun x => nnf (P x))))).
Defined.
Definition Ex2 {A} P Q := Exist (fun x:A => And (P x) (Q x)).
Lemma rTT : holds TT.
Lemma rFF P : holds FF -> holds P.
Lemma rAnd : ∀ P Q, (holds (And P Q) <-> holds P /\ holds Q).
Lemma rImp : ∀ P Q, (holds (Imp P Q) <-> (holds P -> holds Q)).
Lemma rForall : ∀ A P, (holds (Forall P) <-> ∀ x:A, holds (P x)).
Lemma rNot P : holds (Not P) <-> (holds P -> Fa).
Lemma rOrI : ∀ P Q, holds P \/ holds Q -> holds (Or P Q).
Lemma rOrE : ∀ P Q C, (holds P \/ holds Q -> holds C) -> holds (Or P Q) -> holds C.
Lemma rExI : ∀ A P, (exists (x:A), holds (P x)) -> holds (Exist P).
Lemma rExE : ∀ A P C,
(∀ x:A, holds (P x) -> holds C) -> holds (Exist P) -> holds C.
Lemma rEx2I : ∀ A (P Q:A->prop),
(exists2 x, holds (P x) & holds (Q x)) -> holds (Ex2 P Q).
Lemma rEx2E : ∀ A P Q C,
(∀ x:A, holds (P x) -> holds (Q x) -> holds C) ->
holds (Ex2 P Q) ->
holds C.
Lemma rClassic : ∀ P, holds (Not (Not P)) -> holds P.
Lemma equiCons : ~ holds FF <-> ~ L.holds L.FF.
End NegatedTranslation.
exists (L.Not (L.Not (L.Exist(fun x => nnf (P x))))).
Defined.
Definition Ex2 {A} P Q := Exist (fun x:A => And (P x) (Q x)).
Lemma rTT : holds TT.
Lemma rFF P : holds FF -> holds P.
Lemma rAnd : ∀ P Q, (holds (And P Q) <-> holds P /\ holds Q).
Lemma rImp : ∀ P Q, (holds (Imp P Q) <-> (holds P -> holds Q)).
Lemma rForall : ∀ A P, (holds (Forall P) <-> ∀ x:A, holds (P x)).
Lemma rNot P : holds (Not P) <-> (holds P -> Fa).
Lemma rOrI : ∀ P Q, holds P \/ holds Q -> holds (Or P Q).
Lemma rOrE : ∀ P Q C, (holds P \/ holds Q -> holds C) -> holds (Or P Q) -> holds C.
Lemma rExI : ∀ A P, (exists (x:A), holds (P x)) -> holds (Exist P).
Lemma rExE : ∀ A P C,
(∀ x:A, holds (P x) -> holds C) -> holds (Exist P) -> holds C.
Lemma rEx2I : ∀ A (P Q:A->prop),
(exists2 x, holds (P x) & holds (Q x)) -> holds (Ex2 P Q).
Lemma rEx2E : ∀ A P Q C,
(∀ x:A, holds (P x) -> holds (Q x) -> holds C) ->
holds (Ex2 P Q) ->
holds C.
Lemma rClassic : ∀ P, holds (Not (Not P)) -> holds P.
Lemma equiCons : ~ holds FF <-> ~ L.holds L.FF.
End NegatedTranslation.
Module CoqLogic <: IntuitionisticLogic.
Definition prop := Prop.
Definition holds (P:prop) := P.
Definition TT := True.
Definition FF := False.
Definition Not P := ~ P.
Definition Imp (P Q:prop) := P->Q.
Definition And P Q := P /\ Q.
Definition Or P Q := P \/ Q.
Definition Forall {A} (P:A->Prop) := ∀ x:A, P x.
Definition Exist {A} P := exists x:A, P x.
Definition Ex2 {A} (P Q:A->prop) := exists2 x, P x & Q x.
Definition Iff := iff.
Definition Atom (P:Prop) := P.
Lemma rAtom : ∀ P, holds (Atom P) <-> P.
Lemma rTT : holds TT.
Lemma rFF P : holds FF -> holds P.
Lemma rAnd P Q : (holds (And P Q) <-> holds P /\ holds Q).
Lemma rImp P Q : (holds (Imp P Q) <-> (holds P -> holds Q)).
Lemma rForall A P : (holds (Forall P) <-> ∀ x:A, holds (P x)).
Lemma rNot P : holds (Not P) <-> ~ holds P.
Lemma rOrI P Q : holds P \/ holds Q -> holds (Or P Q).
Lemma rOrE P Q C : (holds P \/ holds Q -> holds C) -> holds (Or P Q) -> holds C.
Lemma rExI A P : (exists (x:A), holds (P x)) -> holds (Exist P).
Lemma rExE A P C : (∀ x:A, holds (P x) -> holds C) -> holds (Exist P) -> holds C.
Lemma rEx2I A (P Q:A->Prop): (exists2 x, holds (P x) & holds (Q x)) -> holds (Ex2 P Q).
Lemma rEx2E A P Q C : (∀ x:A, holds (P x) -> holds (Q x) -> holds C) -> holds (Ex2 P Q) -> holds C.
Lemma rIff P Q : holds (Iff P Q) <-> (holds P <-> holds Q).
Lemma rCons : ~ holds FF.
End CoqLogic.
Definition prop := Prop.
Definition holds (P:prop) := P.
Definition TT := True.
Definition FF := False.
Definition Not P := ~ P.
Definition Imp (P Q:prop) := P->Q.
Definition And P Q := P /\ Q.
Definition Or P Q := P \/ Q.
Definition Forall {A} (P:A->Prop) := ∀ x:A, P x.
Definition Exist {A} P := exists x:A, P x.
Definition Ex2 {A} (P Q:A->prop) := exists2 x, P x & Q x.
Definition Iff := iff.
Definition Atom (P:Prop) := P.
Lemma rAtom : ∀ P, holds (Atom P) <-> P.
Lemma rTT : holds TT.
Lemma rFF P : holds FF -> holds P.
Lemma rAnd P Q : (holds (And P Q) <-> holds P /\ holds Q).
Lemma rImp P Q : (holds (Imp P Q) <-> (holds P -> holds Q)).
Lemma rForall A P : (holds (Forall P) <-> ∀ x:A, holds (P x)).
Lemma rNot P : holds (Not P) <-> ~ holds P.
Lemma rOrI P Q : holds P \/ holds Q -> holds (Or P Q).
Lemma rOrE P Q C : (holds P \/ holds Q -> holds C) -> holds (Or P Q) -> holds C.
Lemma rExI A P : (exists (x:A), holds (P x)) -> holds (Exist P).
Lemma rExE A P C : (∀ x:A, holds (P x) -> holds C) -> holds (Exist P) -> holds C.
Lemma rEx2I A (P Q:A->Prop): (exists2 x, holds (P x) & holds (Q x)) -> holds (Ex2 P Q).
Lemma rEx2E A P Q C : (∀ x:A, holds (P x) -> holds (Q x) -> holds C) -> holds (Ex2 P Q) -> holds C.
Lemma rIff P Q : holds (Iff P Q) <-> (holds P <-> holds Q).
Lemma rCons : ~ holds FF.
End CoqLogic.
Classical logic as the negated translation of intuitionisitc logic
Module Atranslation (L:HOLogic) .
Record _prop : Type := Prop_inj
{ Atr : L.prop->L.prop;
Aimpl : ∀ A:L.prop, L.holds A -> L.holds (Atr A) }.
Definition prop := _prop.
Definition TT : prop := Prop_inj (fun _ => L.TT) (fun _ _ => L.rTT).
Definition FF : prop := Prop_inj (fun A => A) (fun _ a => a).
Definition Atom (P:L.prop) : prop.
exists (fun A => L.Or P A).
Defined.
Definition Imp (P Q:prop) : prop.
exists (fun A => L.Imp (Atr P A) (Atr Q A)).
Defined.
Definition Not P := Imp P FF.
Definition And (P Q:prop) : prop.
exists (fun A => L.And (Atr P A) (Atr Q A)).
Defined.
Definition Forall {B} (P:B -> prop) : prop.
exists (fun A => L.Forall(fun x => Atr (P x) A)).
Defined.
Definition Or (P Q:prop) : prop.
exists (fun A => L.Or (Atr P A) (Atr Q A)).
Defined.
Existential: we need to add an extra disjunction to accomodate
higher-order logics, when the quantified domain might be empty:
we need (forall x:B. P(x)) -> (exists x:B. P(x)).
Either we can provide an t:B, or we put an extra disjunction.
Definition Exist {B} (P:B->prop) : prop.
exists (fun A => L.Or (L.Exist(fun x => Atr (P x) A)) A).
Defined.
Definition Ex2 {B} (P Q:B->prop) := Exist(fun x => And (P x) (Q x)).
Section Make.
Variable A : L.prop.
Definition holds P := L.holds (Atr P A).
Lemma rTT : holds TT.
Lemma rFF : ∀ Q, holds FF -> holds Q.
Lemma rAnd : ∀ P Q, holds (And P Q) <-> holds P /\ holds Q.
Lemma rImp : ∀ P Q, (holds (Imp P Q) <-> (holds P -> holds Q)).
Lemma rForall : ∀ T P, (holds (Forall P) <-> ∀ x:T, holds (P x)).
Lemma rNot : ∀ P, holds (Not P) <-> (holds P -> L.holds A).
Lemma rOrI : ∀ P Q, holds P \/ holds Q -> holds (Or P Q).
Lemma rOrE : ∀ P Q C, (holds P \/ holds Q -> holds C) -> holds (Or P Q) -> holds C.
Lemma rExI : ∀ T P, (exists (x:T), holds (P x)) -> holds (Exist P).
Lemma rExE : ∀ T P C, (∀ x:T, holds (P x) -> holds C) -> holds (Exist P) -> holds C.
Lemma rEx2I : ∀ T (P Q:T->prop), (exists2 x, holds (P x) & holds (Q x)) -> holds (Ex2 P Q).
Lemma rEx2E : ∀ T P Q C, (∀ x:T, holds (P x) -> holds (Q x) -> holds C) -> holds (Ex2 P Q) -> holds C.
exists (fun A => L.Or (L.Exist(fun x => Atr (P x) A)) A).
Defined.
Definition Ex2 {B} (P Q:B->prop) := Exist(fun x => And (P x) (Q x)).
Section Make.
Variable A : L.prop.
Definition holds P := L.holds (Atr P A).
Lemma rTT : holds TT.
Lemma rFF : ∀ Q, holds FF -> holds Q.
Lemma rAnd : ∀ P Q, holds (And P Q) <-> holds P /\ holds Q.
Lemma rImp : ∀ P Q, (holds (Imp P Q) <-> (holds P -> holds Q)).
Lemma rForall : ∀ T P, (holds (Forall P) <-> ∀ x:T, holds (P x)).
Lemma rNot : ∀ P, holds (Not P) <-> (holds P -> L.holds A).
Lemma rOrI : ∀ P Q, holds P \/ holds Q -> holds (Or P Q).
Lemma rOrE : ∀ P Q C, (holds P \/ holds Q -> holds C) -> holds (Or P Q) -> holds C.
Lemma rExI : ∀ T P, (exists (x:T), holds (P x)) -> holds (Exist P).
Lemma rExE : ∀ T P C, (∀ x:T, holds (P x) -> holds C) -> holds (Exist P) -> holds C.
Lemma rEx2I : ∀ T (P Q:T->prop), (exists2 x, holds (P x) & holds (Q x)) -> holds (Ex2 P Q).
Lemma rEx2E : ∀ T P Q C, (∀ x:T, holds (P x) -> holds (Q x) -> holds C) -> holds (Ex2 P Q) -> holds C.
Specific properties of A-translation
- it is consistent only for non-derivable A
- the embedding of atomic propositions adds a disjunction with A
Lemma rA : holds FF <-> L.holds A.
Lemma rAtom P : holds (Atom P) <-> L.holds (L.Or P A).
Lemma rAtomI P : L.holds P -> holds (Atom P).
End Make.
Definition holdsA P := ∀ A, holds A P.
Lemma rConsA : holdsA FF <-> L.holds L.FF.
If ~~exists x, P x is derivable in the A-translated logic,
then we have a derivation of exists x, P x in the original
logic.
Lemma rNotNot T (P:T->L.prop) :
holdsA (Not (Not (Exist (fun x => Atom (P x))))) ->
L.holds (L.Exist(fun x => P x)).
If forall x, P x => ~~exists y, Q x y is derivable (in the
A-translated logic) then forall x, Px -> exists y, Q x y
is derivable in the original logic.