Require Import NaturalDeduction. (* Formulate and proof the following in first order logic: (a) All babies are illogical. (b) Anyone who can manage a crocodile is not despised. (c) All illogical people are despised. Therefore, no baby can manage a crocodile. B x = x is a baby L x = x is logical M x = x can manage a crocodile D x = x is despised (a) forall x, B x -> ~L x (b) forall x, M x -> ~D x (c) forall x, ~L x -> D x Therefore, ~exists x, B x /\ M x. *) Lemma LC1 (A : Type) (B L M D : A -> Prop) : (forall x, B x -> ~L x) /\ (forall x, M x -> ~D x) /\ (forall x, ~L x -> D x) -> ~exists x, B x /\ M x. Proof. Impl_Intro. Not_Intro. And_Elim_all in H. Exists_Elim in H0. And_Elim_all in H3. Forall_Elim in H with x. Impl_Elim in H6 and H3. Forall_Elim in H2 with x. Impl_Elim in H8 and H7. Forall_Elim in H1 with x. Impl_Elim in H10 and H4. Not_Elim in H11 and H9. assumption. Qed. (* Formulate and proof the following in first order logic: (a) None of the unnoticed things, met with at sea, are mermaids. (b) Things entered in the log, as met with at sea, are sure to be worth remembering. (c) I have never met with anything worth remembering, when on a voyage. (d) Things met with at sea, that are noticed, are sure to be recorded in the log. Therefore, if I have met with it at sea then it is not a mermaid. N x = x is noticed when met with at sea M x = x is a mermaid L x = x is entered in the log when met with at sea R x = x is worth remembering when met with at sea I x = I have met x at sea (a) ~exists x, ~N x /\ M x (b) forall x, L x -> R x (c) ~exists x, I x /\ R x (d) forall x, N x -> L x Therefore, forall x, I x -> ~M x *) Lemma LC2 (A : Type) (N M L R I : A -> Prop): (~exists x, ~N x /\ M x) /\ (forall x, L x -> R x) /\ (~exists x, I x /\ R x) /\ (forall x, N x -> L x) -> forall x, I x -> ~M x. Proof. Impl_Intro. And_Elim_all in H. Forall_Intro. Impl_Intro. Not_Intro. assume(forall x, I x -> ~R x). Forall_Elim in H5 with x. Impl_Elim in H7 and H3. assume(forall x, M x -> N x). Forall_Elim in H6 with x. Impl_Elim in H10 and H4. Forall_Elim in H2 with x. Impl_Elim in H12 and H11. Forall_Elim in H0 with x. Impl_Elim in H14 and H13. Not_Elim in H8 and H15. assumption. Forall_Intro. Impl_Intro. PBC. assume(exists x : A, ~ N x /\ M x). Not_Elim in H and H10. assumption. Exists_Intro with x0. And_Intro. assumption. assumption. Forall_Intro. Impl_Intro. Not_Intro. assume(exists x : A, I x /\ R x). Not_Elim in H1 and H7. assumption. Exists_Intro with x0. And_Intro. assumption. assumption. Qed.