(* PR-008 (dalil al-imkan, step 3): if an existent is possible in itself, its
   existence and non-existence are both possible [in itself]; therefore its
   existence requires a determining cause (murajjih).

   (3a) the equipoise is definitional: under PR-006, "possible in itself"
        means that nothing in its essence secures its existence, while its
        existence is not ruled out (it exists).
   (3b) the need for a murajjih is substantive: it follows from meaning
        postulate MP-008, "no preponderance without a preponderator"
        (la tarjih bi-la murajjih).  This is Ibn Sina's thesis that the
        ground of need is possibility (illat al-ihtiyaj hiya al-imkan):
        nothing about time is used.

   Rests on:
   - PR-006 (definitions of necessary and possible in itself);
   - PR-004 (definition of "has its existence through another");
   - MP-008, an explicit condition of the theorem;
   - excluded middle (classic), in (3b) only.
   Nothing is assumed to exist.  No notion of time appears. *)

From Stdlib Require Import Classical.
Require PR006.Division PR004.NoRegressOfGiving.

Section Step3.

(* Primitive vocabulary.  Nothing is assumed about any of these. *)
Variable Thing : Type.
Variable Exists : Thing -> Prop.                    (* x exists *)
Variable EssenceIncludesExistence : Thing -> Prop.  (* x's existence is from its essence *)
Variable Gives : Thing -> Thing -> Prop.            (* Gives y x : y gives existence to x *)

(* Reused definitions. *)
Definition PossibleInItself : Thing -> Prop :=
  Division.PossibleInItself Thing Exists EssenceIncludesExistence.
Definition ThroughAnother : Thing -> Prop :=
  NoRegressOfGiving.ThroughAnother Thing Gives.

(* MP-008, no preponderance without a preponderator: whatever exists, with
   nothing giving it existence, has its existence from its essence.  Existence
   comes either from what a thing is, or from something that gives it. *)
Definition MP008_NoPreponderanceWithoutPreponderator : Prop :=
  forall x, Exists x -> ~ ThroughAnother x -> EssenceIncludesExistence x.

(* (3a) Equipoise: for the possible in itself, nothing in its essence secures
   its existence, and its existence is not ruled out, since it exists. *)
Theorem possible_equipoise : forall x,
  PossibleInItself x -> ~ EssenceIncludesExistence x /\ Exists x.
Proof.
  intros x [Hx Hne]. split; assumption.
Qed.

(* (3b) Step 3: the possible in itself requires a murajjih. *)
Theorem possible_requires_murajjih :
  MP008_NoPreponderanceWithoutPreponderator ->
  forall x, PossibleInItself x -> ThroughAnother x.
Proof.
  intros M8 x [Hx Hne]. apply NNPP. intro Hn.
  exact (Hne (M8 x Hx Hn)).
Qed.

End Step3.

(* ------------------------------------------------------------------ *)
(* Checks.  Illustrations of logical possibility only; no claim about what
   exists. *)

(* 1. Countermodel without MP-008 (the "brute fact"): a thing that exists,
      whose existence is not from its essence, and which nothing gives
      existence to.  It is possible in itself yet has no murajjih.  So MP-008
      is needed. *)
Example without_MP008_possible_without_cause :
  let E := fun (_ : unit) => True in
  let Ess := fun (_ : unit) => False in
  let G := fun (_ _ : unit) => False in
  PossibleInItself unit E Ess tt /\ ~ ThroughAnother unit G tt.
Proof.
  simpl. split.
  - split; [exact I | intro H; exact H].
  - intros [y H]. exact H.
Qed.

(* 2. Non-vacuity: MP-008 holds in a world with a necessary thing (true),
      whose existence is from its essence, giving existence to a possible
      thing (false). *)
Example mp008_allows_possibles :
  let E := fun (_ : bool) => True in
  let Ess := fun (x : bool) => x = true in
  let G := fun (y x : bool) => y = true /\ x = false in
  MP008_NoPreponderanceWithoutPreponderator bool E Ess G /\
  PossibleInItself bool E Ess false /\ ThroughAnother bool G false.
Proof.
  unfold MP008_NoPreponderanceWithoutPreponderator, ThroughAnother,
         NoRegressOfGiving.ThroughAnother.
  simpl. split; [| split].
  - intros [] _ Hn; [reflexivity |].
    exfalso. apply Hn. exists true. split; reflexivity.
  - split; [exact I | discriminate].
  - exists true. split; reflexivity.
Qed.

Print Assumptions possible_equipoise.
Print Assumptions possible_requires_murajjih.
Print Assumptions without_MP008_possible_without_cause.
Print Assumptions mp008_allows_possibles.