(* PR-002: Nothing gives existence to itself (self-creation is impossible).

   Rests on:
   - the law of non-contradiction, which is proved below from logic alone;
   - meaning postulates MP-001 and MP-002, which appear as explicit
     conditions of the theorem.
   No axiom is used.  Nothing is assumed to exist.  No notion of time appears:
   "has its existence through" means dependence in the order of being, not
   succession in time. *)

Section SelfCreation.

(* Primitive vocabulary.  Nothing is assumed about any of these. *)
Variable Thing : Type.
Variable Gives : Thing -> Thing -> Prop.    (* Gives y x   : y gives existence to x *)
Variable Through : Thing -> Thing -> Prop.  (* Through x y : x has its existence through y *)

(* Link to the vocabulary of PR-001: x depends on y for its existence
   means y gives existence to x. *)
Definition DependsOn (x y : Thing) : Prop := Gives y x.

(* MP-001, "what lacks a thing cannot give it" (faqid al-shay' la yu'tih):
   whatever gives existence to x does not have its own existence through x. *)
Definition MP001_Giver : Prop := forall x y, Gives y x -> ~ Through y x.

(* MP-002, "receiving": whatever is given existence by y has its existence
   through y. *)
Definition MP002_Receiver : Prop := forall x y, Gives y x -> Through x y.

(* The law of non-contradiction: no statement is both true and not true.
   Proved from logic alone; it is a theorem here, not an axiom. *)
Theorem non_contradiction : forall P : Prop, ~ (P /\ ~ P).
Proof.
  intros P [Hp Hnp]. exact (Hnp Hp).
Qed.

(* Premise 2: nothing gives existence to itself. *)
Theorem no_self_creation :
  MP001_Giver -> MP002_Receiver -> forall x, ~ Gives x x.
Proof.
  intros M1 M2 x Hxx.
  apply (non_contradiction (Through x x)).
  split.
  - exact (M2 x x Hxx).
  - exact (M1 x x Hxx).
Qed.

(* The same, in the vocabulary of PR-001: nothing depends on itself. *)
Corollary no_self_dependence :
  MP001_Giver -> MP002_Receiver -> forall x, ~ DependsOn x x.
Proof.
  intros M1 M2 x. exact (no_self_creation M1 M2 x).
Qed.

End SelfCreation.

(* ------------------------------------------------------------------ *)
(* Checks.  These are illustrations of logical possibility only; they make
   no claim about what exists. *)

(* 1. Non-vacuity: both postulates can hold while giving really occurs.
      Two things: A (true) gives existence to B (false). *)
Example postulates_allow_giving :
  let G := fun (y x : bool) => y = true /\ x = false in
  let T := fun (x y : bool) => x = false /\ y = true in
  MP001_Giver bool G T /\ MP002_Receiver bool G T /\ G true false.
Proof.
  simpl. cbv delta [MP001_Giver MP002_Receiver]. split; [| split].
  - intros x y [Hy _] [HyF _]. subst y. discriminate.
  - intros x y [Hy Hx]. split; assumption.
  - split; reflexivity.
Qed.

(* 2. Countermodel without MP-001: one thing that gives existence to itself and
      has its existence through itself.  MP-002 holds; self-creation occurs. *)
Example without_MP001_self_creation_is_consistent :
  let G := fun (_ _ : unit) => True in
  let T := fun (_ _ : unit) => True in
  MP002_Receiver unit G T /\ G tt tt.
Proof.
  simpl. cbv delta [MP001_Giver MP002_Receiver]. split.
  - intros; exact I.
  - exact I.
Qed.

(* 3. Countermodel without MP-002: one thing that gives existence to itself but
      has its existence through nothing.  MP-001 holds; self-creation occurs. *)
Example without_MP002_self_creation_is_consistent :
  let G := fun (_ _ : unit) => True in
  let T := fun (_ _ : unit) => False in
  MP001_Giver unit G T /\ G tt tt.
Proof.
  simpl. cbv delta [MP001_Giver MP002_Receiver]. split.
  - intros x y _ H. exact H.
  - exact I.
Qed.

(* 4. Eternal-universe compatibility.  Time is introduced ONLY for this check
      and appears nowhere in the premise.  Both things exist at every moment
      (neither has a beginning), A gives existence to B, and both postulates
      hold.  So the postulates never require anything to have a beginning. *)
Example compatible_with_eternal_existence :
  let G := fun (y x : bool) => y = true /\ x = false in
  let T := fun (x y : bool) => x = false /\ y = true in
  let ExistsAt := fun (_ : bool) (_ : nat) => True in
  (forall t, ExistsAt true t /\ ExistsAt false t) /\
  MP001_Giver bool G T /\ MP002_Receiver bool G T /\ G true false.
Proof.
  simpl. cbv delta [MP001_Giver MP002_Receiver]. split; [| split; [| split]].
  - intros t. split; exact I.
  - intros x y [Hy _] [HyF _]. subst y. discriminate.
  - intros x y [Hy Hx]. split; assumption.
  - split; reflexivity.
Qed.

Print Assumptions non_contradiction.
Print Assumptions no_self_creation.
Print Assumptions no_self_dependence.
Print Assumptions postulates_allow_giving.
Print Assumptions without_MP001_self_creation_is_consistent.
Print Assumptions without_MP002_self_creation_is_consistent.
Print Assumptions compatible_with_eternal_existence.