(* The eight held-out tasks given to the neural-symbolic prover: vocabulary,
   definitions, approved postulates, and the statements only. No proofs. *)
From Stdlib Require Import Classical Relations.

Section Pilot.
(* 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 *)
Variable Exists : Thing -> Prop.             (* x exists *)
Variable Ess : Thing -> Prop.                (* x's existence is from its own nature *)
Variable PartOf : Thing -> Thing -> Prop.    (* p is a part of u *)
Variable Universe : Thing.                   (* the universe *)

(* Definitions. *)
Definition DependsOn (x y : Thing) : Prop := Gives y x.            (* x depends on y *)
Definition ThroughAnother (x : Thing) : Prop := exists y, Gives y x.
Definition OfItself (x : Thing) : Prop := Exists x /\ ~ ThroughAnother x.
Definition Necessary (x : Thing) : Prop := Exists x /\ Ess x.
Definition Possible (x : Thing) : Prop := Exists x /\ ~ Ess x.
Definition InUniverse (x : Thing) : Prop := x = Universe \/ PartOf x Universe.

(* Approved postulates, written as definitions: a theorem uses one only when
   its statement lists it as a condition. *)
Definition MP001 : Prop := forall x y, Gives y x -> ~ Through y x.   (* a giver does not have its existence through what it gives existence to *)
Definition MP002 : Prop := forall x y, Gives y x -> Through x y.     (* the receiver has its existence through the giver *)
Definition MP003 : Prop := forall x y z, Through x y -> Through y z -> Through x z.  (* existence-through is inherited *)
Definition MP008 : Prop := forall x, Exists x -> ~ ThroughAnother x -> Ess x.       (* existence comes from one's nature or from a giver *)
Definition OP001 : Prop := forall x y, Gives y x -> OfItself y.      (* only what exists of itself gives existence *)
Definition OP006 : Prop := exists x, InUniverse x /\ Possible x.     (* the universe is not wholly necessary *)
Definition SP001 : Prop := exists x, Exists x.                       (* something exists *)

(* pr002_no_self_creation *)
Definition task_pr002_no_self_creation : Prop :=
  MP001 -> MP002 -> forall x, ~ Gives x x.

(* pr004_no_two_step_giving *)
Definition task_pr004_no_two_step_giving : Prop :=
  OP001 -> forall x y z, Gives y x -> ~ Gives z y.

(* pr003_no_circle *)
Definition task_pr003_no_circle : Prop :=
  MP001 -> MP002 -> MP003 -> forall x, ~ clos_trans Thing DependsOn x x.

(* pr001_relational_exhaustive *)
Definition task_pr001_relational_exhaustive : Prop :=
  forall x, (exists y, (x = y \/ clos_trans Thing DependsOn x y) /\ DependsOn y y) \/ (exists y, (x = y \/ clos_trans Thing DependsOn x y) /\ clos_trans Thing DependsOn y y /\ ~ DependsOn y y) \/ (exists S : Thing -> Prop, S x /\ forall a, S a -> exists b, S b /\ DependsOn a b) \/ ((forall y, ~ DependsOn x y) \/ exists y, clos_trans Thing DependsOn x y /\ forall z, ~ DependsOn y z).

(* pr011_something_caused *)
Definition task_pr011_something_caused : Prop :=
  MP008 -> OP006 -> exists x, InUniverse x /\ Possible x /\ ThroughAnother x.

(* kalima_first_cause *)
Definition task_kalima_first_cause : Prop :=
  OP001 -> ThroughAnother Universe -> exists b, Gives b Universe /\ OfItself b /\ (forall y, ~ Gives y b).

(* step3_possible_needs_cause *)
Definition task_step3_possible_needs_cause : Prop :=
  MP008 -> forall x, Possible x -> ThroughAnother x.

(* imkan_b_necessary_exists *)
Definition task_imkan_b_necessary_exists : Prop :=
  MP008 -> OP001 -> SP001 -> exists n, Necessary n.

End Pilot.