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. 

*)


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

(*
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. 

*)


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