Module TraditionalLogic.
Parameter Thing : Type.
Parameter Socrates : Thing.
Parameter humans : Thing -> Prop.
Definition Term := Thing -> Prop.
Parameter Greeks : Term.
Parameter mortal : Term.
Definition GreeksMortal : Prop :=
forall x,
(Greeks x) -> ( mortal x).
Notation "'All' subject 'are' object " :=
(forall x, (subject x) -> (object x)) (at level 50).
Definition GreeksMortal2 : Prop :=
All Greeks are mortal.
Notation "'No' subject 'are' object " :=
(forall x, (subject x) -> ~(object x)) (at level 50).
Notation "'Some' subject 'are' object " :=
(exists x, (subject x) /\ (object x)) (at level 50).
Notation "'Some' subject 'are' 'not' object " :=
(exists x, (subject x) /\ ~(object x)) (at level 50).
Parameter cats : Term.
Definition NoExample: Prop :=
No Greeks are cats.
Parameter animals : Term.
Definition SomeExample: Prop :=
Some animals are cats.
Parameter brave : Term.
Definition SomeNotExample: Prop :=
Some cats are not brave.
Axiom HumansMortality: All humans are mortal.
Axiom GreeksHumanity: All Greeks are humans.
Lemma HumansMortality2: All humans are mortal.
Proof.
apply HumansMortality.
Qed.
Parameter non: Term -> Term.
Definition immortal: Term := non mortal.
Definition SomeHumansAreImmortal : Prop :=
Some humans are immortal.
Axiom NonNon: forall t, non (non t) = t.
Lemma HumansNonImmortality: All humans are non immortal.
Proof.
unfold immortal.
rewrite NonNon.
apply HumansMortality.
Qed.
Axiom ConvE1:
forall subject object: Term,
(Some object are subject)
->
(Some subject are object).
Axiom ConvE2:
forall subject object: Term,
(No object are subject)
->
(No subject are object).
Axiom SomeAnimalsAreCats : Some animals are cats.
Lemma SomeCatsAreAnimals : Some cats are animals.
Proof.
apply ConvE1.
apply SomeAnimalsAreCats.
Qed.
Axiom NoGreeksAreCats : No Greeks are cats.
Lemma NoCatsAreGreeks : No cats are Greeks.
Proof.
apply ConvE2.
apply NoGreeksAreCats.
Qed.
Axiom ContrE1:
forall subject object: Term,
All (non object) are (non subject)
->
All subject are object.
Axiom ContrE2:
forall subject object: Term,
Some (non object) are not (non subject)
->
Some subject are not object.
Axiom AllCatsAreAnimals : All cats are animals.
Lemma AllNonAnimalsAreNonCats : All (non animals) are (non cats).
Proof.
admit.
Qed.
Axiom SomeAnimalsAreNotCats : Some animals are not cats.
Lemma SomeNonCatsAreNotNonAnimals : Some (non cats) are not (non animals).
Proof.
admit.
Qed.
Axiom ObvE1:
forall subject object: Term,
All subject are non object
->
No subject are object.
Axiom ObvE2:
forall subject object: Term,
No subject are non object
->
All subject are object.
Axiom ObvE3:
forall subject object: Term,
Some subject are non object
->
Some subject are not object.
Axiom ObvE4:
forall subject object: Term,
Some subject are not non object
->
Some subject are object.
Parameter vegetarians : Term.
Axiom SomeHumansVegetarians : Some humans are vegetarians.
Lemma SomeHumansAreNotNonVegetarians :
Some humans are not (non vegetarians).
Proof.
apply ObvE3.
rewrite NonNon.
apply SomeHumansVegetarians.
Qed.
Lemma SomeNon: forall subject object,
Some non object are non subject
-> Some non subject are not object.
Proof.
intros.
apply ObvE3.
apply ConvE1.
apply H.
Qed.
Axiom Barbara : forall major minor middle: Thing -> Prop,
All middle are major
/\ All minor are middle
-> All minor are major.
Lemma GreeksMortality : All Greeks are mortal.
Proof.
apply Barbara with (middle := humans).
split.
apply HumansMortality.
apply GreeksHumanity.
Qed.
Parameter ducks : Term.
Parameter things_that_waltz : Term.
Parameter officers : Term.
Parameter my_poultry : Term.
Lemma No_Officers_Are_My_Poulty :
No ducks are things_that_waltz /\
No officers are non things_that_waltz /\
All my_poultry are ducks
->
No officers are my_poultry.
Proof.
intro.
destruct H.
destruct H0.
apply ObvE1.
apply Barbara with (middle := things_that_waltz).
split.
apply Barbara with (middle := non ducks).
split.
apply ContrE1.
rewrite NonNon.
rewrite NonNon.
apply H1.
apply ObvE2.
rewrite NonNon.
apply ConvE2.
apply H.
apply ObvE2.
apply H0.
Qed.
Parameter babies : Term.
Parameter logical_persons : Term.
Parameter despised_persons : Term.
Parameter persons_who_can_manage_a_crocodile : Term.
Lemma No_baby_can_manage_a_crocodile :
All babies are non logical_persons /\
No persons_who_can_manage_a_crocodile are despised_persons /\
All non logical_persons are despised_persons
->
No babies are persons_who_can_manage_a_crocodile.
Proof.
admit.
Qed.
Parameter boys_under_12 : Term.
Parameter boys_admitted_as_boarders : Term.
Parameter industrious_boys : Term.
Parameter red_haired_boys : Term.
Parameter boys_who_learn_Greek : Term.
Lemma All_Boys_Who_learn_Greek_are_red_haired :
No boys_under_12 are boys_admitted_as_boarders /\
All industrious_boys are red_haired_boys /\
No non boys_admitted_as_boarders are boys_who_learn_Greek /\
No non boys_under_12 are non industrious_boys
->
All boys_who_learn_Greek are red_haired_boys.
Proof.
admit.
Qed.
End TraditionalLogic.