The argument in Rocq

Logical principle

From Stdlib Require Import Classical PeanoNat Lia.

Load the standard library's classical logic, and its arithmetic on natural numbers. The only axiom this brings in is:

classic : forall P : Prop, P \/ ~ P

English: every statement is either true or not true (the law of excluded middle).

Primitive vocabulary

Variable Thing : Type.
Variable DependsOn : Thing -> Thing -> Prop.

English: let there be some kind of things, and some relation "x depends on y for its existence".

• Nothing is said about what the things are, how many there are, or whether any exist.
• Nothing is said about the relation: it need not involve time, and it need not be transitive or have any other property.
• Every result therefore holds for every choice of things and relation.

Definitions (all conditional; none asserts that anything exists)

Definition Independent (x : Thing) : Prop := forall y, ~ DependsOn x y.

English: if x depends on nothing at all, x is called independent.

Definition Chain := nat -> option Thing.

English: a chain is a numbered sequence of positions 0, 1, 2, …. Each position holds either a thing (Some x) or nothing (None), meaning the chain has stopped.

Definition MaximalChainFrom (u : Thing) (c : Chain) : Prop :=
  c 0 = Some u /\
  (forall n x y, c n = Some x -> c (S n) = Some y -> DependsOn x y) /\
  (forall n, c n = None -> c (S n) = None) /\
  (forall n x, c n = Some x -> c (S n) = None -> Independent x).

English: c is a maximal chain of dependence starting from u when all four of these hold:

1. position 0 holds u;
2. whenever position n holds x and position n+1 holds y, x depends on y;
3. once the chain has stopped, it stays stopped;
4. the chain stops after x only if x is independent. It is never cut short while there is still something to depend on.

Definition Repeats (c : Chain) : Prop :=
  exists i j x, i < j /\ c i = Some x /\ c j = Some x.

English: the chain repeats when the same thing x appears at two different positions i and j, with i earlier than j.

Definition SelfDependence (c : Chain) : Prop :=
  exists n x, c n = Some x /\ c (S n) = Some x.

English (case 1, self-dependence): some thing x is immediately followed by itself, so x depends on x.

Definition Circularity (c : Chain) : Prop :=
  Repeats c /\ ~ SelfDependence c.

English (case 2, circularity): some thing recurs in the chain, but never immediately after itself. For example: x depends on y, y depends on x.

Definition InfiniteRegress (c : Chain) : Prop :=
  (forall n, c n <> None) /\ ~ Repeats c.

English (case 3, infinite regress): the chain never stops, and no thing appears in it twice.

Definition EndsInIndependent (c : Chain) : Prop :=
  (exists n x, c n = Some x /\ c (S n) = None /\ Independent x) /\ ~ Repeats c.

English (case 4, ends in the independent): the chain reaches a last thing x, x is independent, and no thing appears in the chain twice.

Helper lemma

Lemma last_item : forall (c : Chain) (u : Thing) n,
  c 0 = Some u -> c n = None ->
  exists m x, c m = Some x /\ c (S m) = None.

English: if a chain starts with a thing and has stopped by some position, then it has a last thing: some position m holds a thing x, and position m+1 is empty.

How it is proved: by counting back from the empty position to the last full one (induction on n). No axiom is needed.

Main theorem: exhaustiveness

Theorem four_cases_exhaustive : forall u c,
  MaximalChainFrom u c ->
  SelfDependence c \/ Circularity c \/ InfiniteRegress c \/ EndsInIndependent c.

English: for every thing u and every maximal chain of dependence starting from u, the chain shows self-dependence, or circularity, or an infinite regress, or it ends in something independent.

How it is proved:

1. The chain either repeats or it does not (excluded middle).
2. If it repeats, some thing either immediately follows itself, which is case 1, or it does not, which is case 2 (excluded middle again).
3. If it does not repeat, the chain either stops somewhere or never stops (excluded middle again).
   • If it stops, the helper lemma gives a last thing. Clause 4 of "maximal" makes that thing independent, which is case 4.
   • If it never stops, that is case 3.

Second theorem: exclusivity

Lemma self_repeats : forall c, SelfDependence c -> Repeats c.

English: a chain with self-dependence repeats. The same thing sits at positions n and n+1.

Theorem four_cases_exclusive : forall c,
  (SelfDependence c -> ~ Circularity c /\ ~ InfiniteRegress c /\ ~ EndsInIndependent c) /\
  (Circularity c -> ~ InfiniteRegress c /\ ~ EndsInIndependent c) /\
  (InfiniteRegress c -> ~ EndsInIndependent c).

English: no chain falls under two cases at once:

• self-dependence rules out the other three;
• circularity rules out infinite regress and ending in the independent;
• infinite regress rules out ending in the independent.

How it is proved:

• Cases 2, 3 and 4 each exclude, by definition, either self-dependence or repetition. Self-dependence implies repetition.
• A chain that never stops cannot have a last thing.
• No axiom is needed.

Examples: each case really occurs

These show that none of the four definitions is empty or rigged. They are illustrations of logical possibility only and make no claim about what exists. None of them uses any axiom.

Example case1_occurs :
  let D := fun (_ _ : unit) => True in
  let c := fun (_ : nat) => Some tt in
  MaximalChainFrom unit D tt c /\ SelfDependence unit c.

English: take a single thing that depends on itself. The chain "it, it, it, …" is a maximal chain, and it shows self-dependence.

Example case2_occurs :
  let D := fun (x y : bool) => y = negb x in
  let c := fun (n : nat) => Some (Nat.odd n) in
  MaximalChainFrom bool D false c /\ Circularity bool c.

English: take two things, each depending on the other. The chain "A, B, A, B, …" is a maximal chain, and it shows circularity.

Example case3_occurs :
  let D := fun (x y : nat) => y = S x in
  let c := fun (n : nat) => Some n in
  MaximalChainFrom nat D 0 c /\ InfiniteRegress nat c.

English: take the numbers 0, 1, 2, …, each depending on the next. The chain "0, 1, 2, …" is a maximal chain, and it is an infinite regress.

Example case4_occurs :
  let D := fun (x y : bool) => x = false /\ y = true in
  let c := fun (n : nat) => match n with 0 => Some false | 1 => Some true | _ => None end in
  MaximalChainFrom bool D false c /\ EndsInIndependent bool D c.

English: take two things, A and B. A depends on B, and B depends on nothing. The chain "A, B, stop" is a maximal chain, and it ends in something independent.

Scope

• It establishes that the four cases are exhaustive and mutually exclusive, for every chain of dependence. Dependence may be temporal or not, for example dependence in the order of being among simultaneous things.
• It does not establish that any case is impossible. That is the job of other premises.
• Case 4 means "depends on nothing". It does not mean "necessary". Linking the two requires a separate premise.
• Case 4 includes a chain that stops at its starting point u. For example, the universe depending on nothing. Excluding this requires a separate premise, such as "the universe depends on something".
• **The theorem covers every chain. It does not prove that a chain from a given thing exists.** Constructing such a chain in general requires a choice principle. Any argument that needs this must state it as a premise.
• Branching is covered. A thing with several things it depends on is handled chain by chain.

Variable Thing : Type.
Variable Gives : Thing -> Thing -> Prop.

English: some kind of things, and the relation "y gives existence to x". Nothing is assumed about either.

Definition Dep (x y : Thing) : Prop := Gives y x.
Definition Independent (x : Thing) : Prop := forall y, ~ Dep x y.

English:

• x depends on y means y gives existence to x.
• x is independent if it depends on nothing.

Definition Reach (x y : Thing) : Prop :=
  forall P : Thing -> Thing -> Prop,
    ((forall a b, Dep a b -> P a b) /\
     (forall a b c, P a b -> P b c -> P a c)) -> P x y.

English: x ultimately depends on y when x stands in every transitive relation that contains dependence to y. This is Leo-III's definition, transcribed.

Definition Case1 (x : Thing) : Prop :=
  exists y, (x = y \/ Reach x y) /\ Dep y y.
Definition Case2 (x : Thing) : Prop :=
  exists y, (x = y \/ Reach x y) /\ Reach y y /\ ~ Dep y y.
Definition Case3 (x : Thing) : Prop :=
  exists S : Thing -> Prop, S x /\ (forall a, S a -> exists b, S b /\ Dep a b).
Definition Case4 (x : Thing) : Prop :=
  Independent x \/ exists y, Reach x y /\ Independent y.

English:

• Case 1, self-creation: x, or something x ultimately depends on, depends on itself.
• Case 2, circularity: x, or something x ultimately depends on, lies on a longer circle.
• Case 3, endless regress: x belongs to a collection in which every member depends on another member.
• Case 4, ends in the independent: x is independent, or ultimately depends on something independent.

Theorem reach_iff_clos_trans : forall x y, Reach x y <-> clos_trans Thing Dep x y.

English: Leo-III's "ultimately depends on" and Rocq's standard "one or more steps of dependence" are the same relation.

How it is proved: each is contained in the other.

• clos_trans is a transitive relation containing dependence, so Reach implies it.
• By induction on clos_trans, each of its steps belongs to every such relation.

No axiom is needed.

Theorem four_cases_exhaustive_relational : forall x,
  Case1 x \/ Case2 x \/ Case3 x \/ Case4 x.

English: everything falls under at least one of the four cases.

How it is proved: either case 4 holds or it doesn't (excluded middle). Suppose it doesn't. Take the collection made up of x and everything x ultimately depends on. No member is independent, since otherwise case 4 would hold. So each member depends on something, and that something is also in the collection. That is case 3.

Scope

• It establishes premise 1 in the form used by Leo-III's assembly.p. It also establishes that Leo-III's premise 3 states exactly what PR-003 proves.
• In this form the cases are not exclusive. A circle is also an endless regress. The exclusive, chain-based form is PR-001's first proof, rocq-chains.

Primitive vocabulary

Variable Thing : Type.
Variable Gives : Thing -> Thing -> Prop.
Variable Through : Thing -> Thing -> Prop.

English: let there be some kind of things, and two relations:

• Gives y x: "y gives existence to x";
• Through x y: "x has its existence through y".

Nothing is said about what the things are, how many there are, or whether any exist. Nothing is said about the relations. Neither relation involves time: both concern dependence in the order of being, not before and after.

Link to PR-001

Definition DependsOn (x y : Thing) : Prop := Gives y x.

English: "x depends on y for its existence" means "y gives existence to x". This is the relation used in PR-001.

Meaning postulates

Definition MP001_Giver : Prop := forall x y, Gives y x -> ~ Through y x.

English (MP-001, "what lacks a thing cannot give it", fāqid al-shayʾ lā yuʿṭīh): whatever gives existence to x does not itself have its existence through x. The giver must already have the existence it gives; it cannot receive that existence from the very thing it gives it to.

Definition MP002_Receiver : Prop := forall x y, Gives y x -> Through x y.

English (MP-002, "receiving"): whatever is given existence by y has its existence through y.

Both are written as definitions. They are not asserted to be true. A theorem depends on them only when its statement lists them as conditions.

The law of non-contradiction

Theorem non_contradiction : forall P : Prop, ~ (P /\ ~ P).

English: no statement is both true and not true.

How it is proved: suppose P and not-P. "Not-P" means "P leads to absurdity". Apply it to P, and absurdity follows. This is pure logic; no axiom is needed.

Main theorem: premise 2

Theorem no_self_creation :
  MP001_Giver -> MP002_Receiver -> forall x, ~ Gives x x.

English: if MP-001 and MP-002 hold, then nothing gives existence to itself.

How it is proved: suppose x gives existence to itself.

1. By MP-002, x is the receiver, so x has its existence through x.
2. By MP-001, x is the giver, so x does not have its existence through x.
3. x both has and does not have its existence through x, in the same respect. The law of non-contradiction rules this out.

This is the argument's own reasoning: the thing would be "both dependent upon itself for its existence and the source of the existence upon which it depends, which is contradictory".

Corollary no_self_dependence :
  MP001_Giver -> MP002_Receiver -> forall x, ~ DependsOn x x.

English: the same result in PR-001's vocabulary. If MP-001 and MP-002 hold, nothing depends on itself for its existence. This rules out case 1 of PR-001.

Checks

These are illustrations of logical possibility only. They make no claim about what exists.

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.

English (non-vacuity): take two things, A and B, where A gives existence to B. Both postulates hold. So the postulates do not simply forbid all giving; they forbid only self-giving.

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.

English (countermodel): drop MP-001. Now one thing can give existence to itself while MP-002 still holds. So MP-001 is necessary to the proof.

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.

English (countermodel): drop MP-002. Now one thing can give existence to itself while MP-001 still holds. So MP-002 is necessary to the proof.

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.

English (eternal-universe compatibility): introduce time only for this check. Take two things that exist at every moment, so neither has a beginning. The first gives existence to the second, and both postulates hold. So the postulates, and therefore premise 2, never require anything to have a beginning. They hold equally if the universe is eternal.

Scope

• It establishes that, given MP-001 and MP-002, nothing gives existence to itself. This excludes case 1 of PR-001. It holds whether or not the universe had a beginning.
• The premise is a direct special case of the postulates. MP-001 and MP-002, applied to x giving existence to x, yield it in one step. This is ordinary deduction from a general principle, not circularity. But it means the whole philosophical weight rests on MP-001, "what lacks a thing cannot give it". A critic who rejects self-creation's impossibility must reject MP-001 or MP-002. The countermodels show exactly this.
• MP-001 is broader than this premise. It also rules out two things giving existence to each other directly. Longer circles need more; that is premise 3.
• It does not establish that anything exists, or that anything gives existence to anything.

Imports

From Stdlib Require Import Relations PeanoNat Lia.
Require PR001.Exhaustiveness PR002.NoSelfCreation.

English: load the standard library's definitions of relations and its arithmetic, and load the proved premises PR-001 and PR-002. The standard library parts add no axioms.

Primitive vocabulary (the same as PR-002)

Variable Thing : Type.
Variable Gives : Thing -> Thing -> Prop.
Variable Through : Thing -> Thing -> Prop.

English: some kind of things, together with two relations:

• "y gives existence to x";
• "x has its existence through y".

Nothing is assumed about them.

Reused definitions

Definition DependsOn : Thing -> Thing -> Prop := NoSelfCreation.DependsOn Thing Gives.
Definition MP001 : Prop := NoSelfCreation.MP001_Giver Thing Gives Through.
Definition MP002 : Prop := NoSelfCreation.MP002_Receiver Thing Gives Through.

English: exactly the definitions from PR-002:

• "x depends on y" means "y gives existence to x";
• MP-001: whatever gives existence to x does not have its own existence through x;
• MP-002: whatever is given existence by y has its existence through y.

New meaning postulate

Definition MP003_Inherited : Prop :=
  forall x y z, Through x y -> Through y z -> Through x z.

English (MP-003, "existence-through is inherited"): if x has its existence through y, and y has its existence through z, then x has its existence through z.

Example: if a lamp's light exists through the lamp, and the lamp exists through its maker, then the light exists, ultimately, through the maker too. This is the argument's own step: "A ultimately depends upon itself".

New definition

Definition UltimatelyDependsOn : Thing -> Thing -> Prop := clos_trans Thing DependsOn.

English: x ultimately depends on y when there is a chain of one or more steps of dependence from x to y. For example: x depends on p, p depends on q, and q depends on y.

clos_trans is the standard library's definition of "one or more steps" of a relation. It is a definition, not an assumption.

Step 1: ultimate dependence means existence through

Lemma ultimate_dependence_is_through :
  MP002 -> MP003_Inherited ->
  forall x y, UltimatelyDependsOn x y -> Through x y.

English: if MP-002 and MP-003 hold, then whenever x ultimately depends on y, x has its existence through y.

How it is proved: by the length of the chain.

• For one step, MP-002 applies directly.
• For a longer chain, split it into two shorter parts and join them with MP-003.

Step 2: premise 3, no circle of any length

Theorem no_circular_dependence :
  MP001 -> MP002 -> MP003_Inherited ->
  forall x, ~ UltimatelyDependsOn x x.

English: if MP-001, MP-002 and MP-003 hold, then nothing ultimately depends on itself, however long the circle.

How it is proved: suppose x ultimately depends on x. Take the first step of the circle: x depends on some m, and m ultimately depends back on x.

• If the circle has only one step (m is x itself), x gives existence to itself. PR-002 already rules this out, so it is reused, not re-proved.
• Otherwise:
  1. By Step 1, m has its existence through x.
  2. But m gives existence to x, so by MP-001 m does not have its existence through x.
  3. The law of non-contradiction rules this out.

This is the argument's own reasoning. The circle "reduces to its constituent relations", and the giver would have its existence through what it gives existence to.

Step 3: link to the chains of PR-001

Lemma chain_segment : forall u c,
  Exhaustiveness.MaximalChainFrom Thing DependsOn u c ->
  forall i k a b, c i = Some a -> c (i + S k) = Some b -> UltimatelyDependsOn a b.

English: in any maximal chain of dependence (as defined in PR-001), if a stands at one position and b stands at a later position, then a ultimately depends on b.

How it is proved: by the distance between the two positions. Every position in between must be filled, because a stopped chain stays stopped. Consecutive positions are linked by dependence.

Step 4: no chain contains a thing twice

Theorem no_repetition_in_chains :
  MP001 -> MP002 -> MP003_Inherited ->
  forall u c, Exhaustiveness.MaximalChainFrom Thing DependsOn u c ->
  ~ Exhaustiveness.Repeats Thing c.

English: if the three postulates hold, then no maximal chain of dependence contains the same thing at two positions.

How it is proved: if x appeared at two positions, Step 3 would make x ultimately depend on x, which Step 2 rules out.

Step 5: cases 1 and 2 of PR-001 are eliminated

Corollary cases_1_and_2_eliminated :
  MP001 -> MP002 -> MP003_Inherited ->
  forall u c, Exhaustiveness.MaximalChainFrom Thing DependsOn u c ->
  ~ Exhaustiveness.SelfDependence Thing c /\ ~ Exhaustiveness.Circularity Thing c.

English: if the three postulates hold, then no maximal chain of dependence shows self-dependence (case 1) or circularity (case 2).

How it is proved: both cases require the chain to repeat a thing, and Step 4 rules that out. PR-001's lemma self_repeats is reused for case 1.

Checks

These are illustrations of logical possibility only. They make no claim about what exists. They use three things, A, B and C:

Inductive Three := A | B | C.
Definition CircleGives (y x : Three) : Prop :=
  match y, x with B, A | C, B | A, C => True | _, _ => False end.
Definition LineGives (y x : Three) : Prop :=
  match y, x with B, A | C, B => True | _, _ => False end.
Definition LineThrough (x y : Three) : Prop :=
  match x, y with A, B | A, C | B, C => True | _, _ => False end.

English:

• In the circle, B gives existence to A, C to B, and A to C.
• In the line, B gives existence to A and C gives existence to B. A has its existence through B and through C, and B has its existence through C.

Example postulates_allow_chains :
  MP001 Three LineGives LineThrough /\ MP002 Three LineGives LineThrough /\
  MP003_Inherited Three LineThrough /\ LineGives B A /\ LineGives C B.

English (non-vacuity): in the line, all three postulates hold while a real two-step chain of giving occurs. So the postulates forbid only circles, not chains.

Example without_MP003_a_circle_is_consistent :
  MP001 Three CircleGives (fun x y => CircleGives y x) /\
  MP002 Three CircleGives (fun x y => CircleGives y x) /\
  UltimatelyDependsOn Three CircleGives A A.

English (countermodel): drop MP-003, and let "through" hold only for direct givers. MP-001 and MP-002 hold, yet A ultimately depends on A. So MP-003 is necessary: without inheritance, a circle of three is consistent.

Example without_MP001_a_circle_is_consistent :
  MP002 Three CircleGives (fun _ _ => True) /\
  MP003_Inherited Three (fun _ _ => True) /\
  UltimatelyDependsOn Three CircleGives A A.

English (countermodel): drop MP-001. The circle is consistent, so MP-001 is necessary.

Example without_MP002_a_circle_is_consistent :
  MP001 Three CircleGives (fun _ _ => False) /\
  MP003_Inherited Three (fun _ _ => False) /\
  UltimatelyDependsOn Three CircleGives A A.

English (countermodel): drop MP-002. The circle is consistent, so MP-002 is necessary.

Scope

• It establishes that, given MP-001, MP-002 and MP-003, no thing ultimately depends on itself through a circle of any length. It therefore rules out cases 1 and 2 of PR-001 for every maximal chain. It also re-derives PR-002 as the one-step circle.
• It holds whether or not the universe is eternal. No time appears in the vocabulary.
• It is not circular. MP-003 says nothing about circles; it only says that existence-through passes along a chain. The circle's impossibility comes from combining it with MP-001.
• It does not establish that anything exists, or that any chain exists.
• It says nothing about infinite regress (case 3). A regress never repeats a thing, so this proof does not touch it. That is premise 4.

Primitive vocabulary

Variable Thing : Type.
Variable Gives : Thing -> Thing -> Prop.
Variable Proximate : Thing -> Thing -> Prop.
Variable Exists : Thing -> Prop.

English: some kind of things, together with three notions:

• Gives y x: y gives existence to x. It is the actual cause of x's existence.
• Proximate y x: y is a proximate cause of x. It acts on or transforms x within the order of existing things.
• Exists x: x actually exists.

Nothing is assumed about any of these, and nothing is assumed to exist.

Definitions (conditional)

Definition ThroughAnother (x : Thing) : Prop := exists y, Gives y x.

English: if something gives existence to x, x has its existence through another.

Definition OfItself (x : Thing) : Prop := Exists x /\ ~ ThroughAnother x.

English: if x exists and nothing gives existence to x, x has existence of itself.

The observational premise

Definition OP001_OnlySelfExistentGives : Prop :=
  forall x y, Gives y x -> OfItself y.

English (OP-001): only what has existence of itself can give existence. Whatever has its existence through another truly exists and can be a proximate cause that transforms what already exists, but it cannot be the giver of existence.

• Evidence: in all observation and experience, every cause we see only transforms what already exists. Humans, nature and mechanisms never give existence.
• Limit: this generalizes from what has been observed to every case, like ex nihilo nihil fit.
• Note: Proximate is deliberately left unrestricted. OP-001 constrains only the giving of existence.

Premise 4

Theorem giver_is_self_existent :
  OP001_OnlySelfExistentGives ->
  forall x, ThroughAnother x -> exists b, Gives b x /\ OfItself b.

English: if OP-001 holds, then whatever has its existence through another receives it from something that has existence of itself.

How it is proved: take whatever gives existence to x. By OP-001, it has existence of itself.

Theorem no_two_step_giving :
  OP001_OnlySelfExistentGives ->
  forall x y z, Gives y x -> ~ Gives z y.

English: if OP-001 holds, nothing that gives existence has received existence from anything. So the giving of existence never passes through an intermediary, and a chain of existence-giving, finite or infinite, cannot form.

How it is proved: if y gives existence to x, then by OP-001 y has existence of itself, so nothing gives existence to y.

Link to the chains of PR-001

Definition DependsOn : Thing -> Thing -> Prop := NoSelfCreation.DependsOn Thing Gives.

English: as in PR-002, "x depends on y" means "y gives existence to x".

Theorem giving_chain_stops :
  OP001_OnlySelfExistentGives Thing Gives Exists ->
  forall u c, Exhaustiveness.MaximalChainFrom Thing DependsOn u c ->
  c 2 = None.

English: if OP-001 holds, every maximal chain of existence-giving (as defined in PR-001) has stopped by its third position. It holds the thing, then its giver, and nothing beyond, because the giver has existence of itself.

Corollary no_regress_of_giving :
  OP001_OnlySelfExistentGives Thing Gives Exists ->
  forall u c, Exhaustiveness.MaximalChainFrom Thing DependsOn u c ->
  ~ Exhaustiveness.InfiniteRegress Thing c.

English: if OP-001 holds, no chain of existence-giving is an infinite regress. Case 3 of PR-001 is eliminated for the giving of existence.

Checks

These are illustrations of logical possibility only. They make no claim about what exists.

Example without_OP001_regress_of_giving_is_consistent :
  let G := fun (y x : nat) => y = S x in
  let E := fun (_ : nat) => True in
  (forall n, G (S n) n) /\ (forall n, E n) /\
  ~ OP001_OnlySelfExistentGives nat G E.

English (countermodel): take the numbers 0, 1, 2, …, each given existence by the next, with all existing. This is consistent, and it is exactly a world where OP-001 fails. So OP-001 is what the proof depends on.

Example dependent_things_exist_and_act :
  let G := fun (y x : option nat) => y = None /\ exists n, x = Some n in
  let P := fun (y x : option nat) => exists n, x = Some n /\ y = Some (S n) in
  let E := fun (_ : option nat) => True in
  OP001_OnlySelfExistentGives (option nat) G E /\
  OfItself (option nat) G E None /\
  (forall n, E (Some n) /\ ThroughAnother (option nat) G (Some n) /\
             P (Some (S n)) (Some n)).

English (the rebuttal "then do we not exist?"): take a base T that gives existence to every member of an endless horizontal chain 0, 1, 2, …. Each member is a proximate cause of the one before it. Then:

• OP-001 holds;
• T has existence of itself;
• every member truly exists, has its existence through another, and is a real proximate cause.

So OP-001 denies only that dependent things give existence. It never denies that they exist or act. This also shows OP-001 is non-vacuous, and it formalizes the "realms" position: a horizontal regress is fine when grounded from above.

Example recursion_without_base_worlds_A_and_B :
  let link := fun (y x : nat) => y = S x in
  (forall x, True <-> exists y, link y x /\ True) /\
  (forall x, False <-> exists y, link y x /\ False).

English (the recursion model, no base): U(0) depends on U(1), U(1) on U(2), and so on without end. "All exist" and "none exist" both fit every link. A chain of proximate links alone does not settle whether anything exists.

Example recursion_with_base_forces_world_A : forall (k : nat) (E : nat -> Prop),
  (forall x, x < k -> (E x <-> E (S x))) -> E k ->
  forall n, n <= k -> E n.

English (the recursion model, with a base): U(0) to U(k−1) each depend on the next, and U(k) is a base. If the base exists, every world that fits the links has all of them existing. Only World A remains.

Scope

• It establishes that, given OP-001, the giving of existence never forms a chain, and so never a regress. Whatever has existence through another receives it from something that has existence of itself. Case 3 of PR-001 is eliminated for existence-giving.
• It permits any structure of proximate causes, including an endless horizontal regress, because proximate causation is not the giving of existence.
• The premise is a direct consequence of OP-001. The proof is short because OP-001 carries the whole weight.
  • OP-001 is an observational premise, grounded in the fact that all observed causation only transforms what already exists.
  • It is not a logical truth.
  • Critics must deny OP-001, which means claiming that some dependent thing gives existence. The countermodel shows exactly this.
• It does not establish that anything exists, or that the self-existent is necessary. Linking "has existence of itself" to "necessary", and adding "the universe exists", are steps for the conclusion.

Primitive vocabulary

Variable Thing : Type.
Variable Gives : Thing -> Thing -> Prop.
Variable Through : Thing -> Thing -> Prop.
Variable Exists : Thing -> Prop.
Variable Universe : Thing.

English: some kind of things, together with:

• "y gives existence to x";
• "x has its existence through y";
• "x exists";
• one thing, called the universe, whose existence is to be explained.

Nothing is assumed about any of these.

• Universe is a section variable. When the section closes, the theorem holds for every thing taken as the universe.
• It does not assert that the universe exists. It only names what the explanation is about.

Reused definitions

Definition DependsOn : Thing -> Thing -> Prop := NoSelfCreation.DependsOn Thing Gives.
Definition MP001 := NoCircularCreation.MP001 Thing Gives Through.
Definition MP002 := NoCircularCreation.MP002 Thing Gives Through.
Definition MP003 := NoCircularCreation.MP003_Inherited Thing Through.
Definition OP001 := NoRegressOfGiving.OP001_OnlySelfExistentGives Thing Gives Exists.

English: the definitions exactly as proved and approved in PR-002, PR-003 and PR-004:

• "x depends on y" means "y gives existence to x";
• MP-001: what lacks a thing cannot give it;
• MP-002: the receiver has its existence through the giver;
• MP-003: existence-through is inherited;
• OP-001: only what has existence of itself gives existence.

The antecedent: the universe is caused

Definition UniverseIsCaused : Prop :=
  NoRegressOfGiving.ThroughAnother Thing Gives Universe.

English: the existence of the universe requires a cause. Something gives the universe its existence, so the universe has its existence through another.

This is the argument's own "if". Whether it is true is a separate question, for dalīl al-imkān.

Necessity

Definition Necessary (x : Thing) : Prop := NoRegressOfGiving.OfItself Thing Gives Exists x.

English: if x exists and nothing gives it existence, x is called necessary.

Its existence belongs to it of itself, so there is no giver who could withhold it, and it cannot be taken away. This is the classical wājib al-wujūd li-dhātihi. Whatever has its existence through another holds it as received, and it can be taken away.

Step 1: only case 4 remains

Theorem only_case_4_remains :
  MP001 -> MP002 -> MP003 -> OP001 ->
  forall c, Exhaustiveness.MaximalChainFrom Thing DependsOn Universe c ->
  Exhaustiveness.EndsInIndependent Thing DependsOn c.

English: if MP-001, MP-002, MP-003 and OP-001 hold, then every complete chain of existence-giving from the universe ends in something that depends on nothing.

How it is proved: exactly as the argument runs.

1. By PR-001, the chain is self-creation, circular, an infinite regress, or ends in something independent.
2. By PR-003, which includes PR-002, it is not self-creation or circular.
3. By PR-004, it is not an infinite regress.
4. Only the fourth case remains.

Excluded middle enters through PR-001.

Step 2: the conclusion

Theorem kalima_conclusion :
  MP001 -> MP002 -> MP003 -> OP001 ->
  UniverseIsCaused ->
  exists b,
    Gives b Universe /\
    Exists b /\
    Necessary b /\
    Exhaustiveness.Independent Thing DependsOn b /\
    exists c,
      Exhaustiveness.MaximalChainFrom Thing DependsOn Universe c /\
      c 1 = Some b /\
      Exhaustiveness.EndsInIndependent Thing DependsOn c.

English: if the four principles hold, then if the existence of the universe requires a cause, there is some b such that:

• b gives existence to the universe;
• b exists;
• b is necessary;
• b depends on nothing, so there are no further causes beyond it;
• a complete chain from the universe really exists: the universe, then b, then nothing further. It ends in the independent, as Step 1 requires.

How it is proved:

1. By the antecedent, something b gives existence to the universe.
2. By OP-001, b has existence of itself: it exists, and nothing gives it existence. So b is necessary and depends on nothing.
3. The chain "universe, b, stop" is then complete, and by Step 1 it ends in the independent.

No choice principle is needed, because the chain is built explicitly.

Checks

These are illustrations of logical possibility only. They make no claim about what exists.

Example all_premises_hold_together :
  let G := fun (y x : bool) => y = true /\ x = false in
  let T := fun (x y : bool) => x = false /\ y = true in
  let E := fun (_ : bool) => True in
  MP001 bool G T /\ MP002 bool G T /\ MP003 bool T /\ OP001 bool G E /\
  UniverseIsCaused bool G false.

English (consistency): take a base that gives existence to a universe, with both existing. Every principle holds and the universe is caused. So the conclusion does not rest on contradictory premises.

Example uncaused_universe_no_first_cause_follows :
  let G := fun (_ _ : unit) => False in
  let T := fun (_ _ : unit) => False in
  let E := fun (_ : unit) => True in
  MP001 unit G T /\ MP002 unit G T /\ MP003 unit T /\ OP001 unit G E /\
  ~ (exists b, G b tt).

English (the "if" matters): take a universe that nothing gives existence to. Every principle holds, but nothing gives it existence. So the conclusion is conditional, exactly as the argument states it.

Example without_OP001_no_necessary_cause_follows :
  let G := fun (y x : nat) => y = S x in
  let T := fun (x y : nat) => x < y in
  let E := fun (_ : nat) => True in
  MP001 nat G T /\ MP002 nat G T /\ MP003 nat T /\
  UniverseIsCaused nat G 0 /\
  ~ (exists b, G b 0 /\ Necessary nat G E b).

English (countermodel): take the numbers 0, 1, 2, …, each given existence by the next, with 0 as the universe. MP-001 to MP-003 hold and the universe is caused, but its giver is not necessary. So without OP-001, the conclusion does not follow.

Scope

• It establishes the argument's conclusion exactly as the argument states it. If the existence of the universe requires a cause, then:
  • the only remaining explanation is a necessary first cause;
  • that cause gives the universe existence and depends on nothing.
• It rests only on the argument's four premises, PR-001 to PR-004, and their approved postulates.
• Whether the universe is caused is a separate question. It belongs to dalīl al-imkān (PR-005).
• OP-001 alone, given the "if", already yields the first cause. This was verified in Z3. The four-case structure shows that the other cases are impossible, but OP-001 carries the decisive weight.
• A strength: it does not depend on time. It holds whether or not the universe is eternal.
• It does not establish:
  • that there is only one necessary being;
  • any attribute of the first cause beyond necessity and giving existence.

Vocabulary and definitions

Variable Thing : Type.
Variable Exists : Thing -> Prop.
Variable EssenceIncludesExistence : Thing -> Prop.
Variable Gives : Thing -> Thing -> Prop.
Variable PartOf : Thing -> Thing -> Prop.
Variable Universe : Thing.

English: some kind of things, together with:

• "x exists";
• "x's existence is from its nature";
• "y gives existence to x";
• "p is a part of u", where a part may be physical or metaphysical;
• the universe.

Nothing is assumed about any of these.

Definition InUniverse (x : Thing) : Prop := x = Universe \/ PartOf x Universe.

(* The four cases, for a universe whose parts all exist. *)
Definition WhollyNecessary : Prop := forall x, InUniverse x -> NecessaryInItself x.
Definition WhollyPossible : Prop := forall x, InUniverse x -> PossibleInItself x.
Definition NecessaryAndPossibleInSameRespect : Prop :=
  exists x, InUniverse x /\ NecessaryInItself x /\ PossibleInItself x.
Definition Mixed : Prop :=
  (exists x, InUniverse x /\ NecessaryInItself x) /\ (exists y, InUniverse y /\ PossibleInItself y).

(* OP-006 (observation): at the very least, the universe is not wholly
   necessary -- something in it (or the universe itself) exists without having
   its existence from its own nature. *)
Definition OP006_NotWhollyNecessary : Prop :=
  exists x, InUniverse x /\ PossibleInItself x.

(* Case 2 is a contradiction (PR-006). *)
Theorem case2_impossible : ~ NecessaryAndPossibleInSameRespect.

English: x is in the universe when it is the universe itself or one of its parts.

Definition WhollyNecessary : Prop := forall x, InUniverse x -> NecessaryInItself x.
Definition WhollyPossible : Prop := forall x, InUniverse x -> PossibleInItself x.
Definition NecessaryAndPossibleInSameRespect : Prop :=
  exists x, InUniverse x /\ NecessaryInItself x /\ PossibleInItself x.
Definition Mixed : Prop :=
  (exists x, InUniverse x /\ NecessaryInItself x) /\ (exists y, InUniverse y /\ PossibleInItself y).

(* OP-006 (observation): at the very least, the universe is not wholly
   necessary -- something in it (or the universe itself) exists without having
   its existence from its own nature. *)
Definition OP006_NotWhollyNecessary : Prop :=
  exists x, InUniverse x /\ PossibleInItself x.

(* Case 2 is a contradiction (PR-006). *)
Theorem case2_impossible : ~ NecessaryAndPossibleInSameRespect.
Definition WhollyPossible : Prop := forall x, InUniverse x -> PossibleInItself x.
Definition NecessaryAndPossibleInSameRespect : Prop :=
  exists x, InUniverse x /\ NecessaryInItself x /\ PossibleInItself x.
Definition Mixed : Prop :=
  (exists x, InUniverse x /\ NecessaryInItself x) /\ (exists y, InUniverse y /\ PossibleInItself y).

(* OP-006 (observation): at the very least, the universe is not wholly
   necessary -- something in it (or the universe itself) exists without having
   its existence from its own nature. *)
Definition OP006_NotWhollyNecessary : Prop :=
  exists x, InUniverse x /\ PossibleInItself x.

(* Case 2 is a contradiction (PR-006). *)
Theorem case2_impossible : ~ NecessaryAndPossibleInSameRespect.
Definition NecessaryAndPossibleInSameRespect : Prop :=
  exists x, InUniverse x /\ NecessaryInItself x /\ PossibleInItself x.
Definition Mixed : Prop :=
  (exists x, InUniverse x /\ NecessaryInItself x) /\ (exists y, InUniverse y /\ PossibleInItself y).

(* OP-006 (observation): at the very least, the universe is not wholly
   necessary -- something in it (or the universe itself) exists without having
   its existence from its own nature. *)
Definition OP006_NotWhollyNecessary : Prop :=
  exists x, InUniverse x /\ PossibleInItself x.

(* Case 2 is a contradiction (PR-006). *)
Theorem case2_impossible : ~ NecessaryAndPossibleInSameRespect.
Definition Mixed : Prop :=
  (exists x, InUniverse x /\ NecessaryInItself x) /\ (exists y, InUniverse y /\ PossibleInItself y).

(* OP-006 (observation): at the very least, the universe is not wholly
   necessary -- something in it (or the universe itself) exists without having
   its existence from its own nature. *)
Definition OP006_NotWhollyNecessary : Prop :=
  exists x, InUniverse x /\ PossibleInItself x.

(* Case 2 is a contradiction (PR-006). *)
Theorem case2_impossible : ~ NecessaryAndPossibleInSameRespect.

English: the four cases.

• Wholly necessary (case 1): everything in the universe is necessary in itself.
• Wholly possible (case 4): everything in it is possible in itself.
• Necessary and possible in the same respect (case 2): something in it is both at once.
• Mixed (case 3): something in it is necessary and something is possible.

The observation

Definition OP006_NotWhollyNecessary : Prop :=
  exists x, InUniverse x /\ PossibleInItself x.

(* Case 2 is a contradiction (PR-006). *)
Theorem case2_impossible : ~ NecessaryAndPossibleInSameRespect.

English (OP-006): at the very least, the universe is not wholly necessary. Something in it, or the universe itself, exists without having its existence from its own nature.

OP-006 is needed for the broader definition. When the universe may include the necessary, as in Spinoza's view, only observation excludes a wholly necessary universe. Under our definition OP-006 is not used; OP-007 is used instead.

The division

Theorem case2_impossible : ~ NecessaryAndPossibleInSameRespect.

English: case 2 is impossible. Nothing is necessary and possible in the same respect (PR-006). No axiom is needed.

Theorem universe_division :
  (forall x, InUniverse x -> Exists x) ->
  WhollyNecessary \/ WhollyPossible \/ Mixed.

English: if the universe and all its parts exist, it is wholly necessary, wholly possible, or mixed. The division is exhaustive.

How: every part is necessary or possible (step 1). Checking whether any part is possible and whether any is necessary gives the three cases.

The result, under either definition

Theorem something_in_universe_is_caused :
  MP008 -> OP006_NotWhollyNecessary ->
  exists x, InUniverse x /\ PossibleInItself x /\ ThroughAnother x.

English: if MP-008 holds and the universe is not wholly necessary, then something in the universe is possible and has a cause.

How: OP-006 gives something possible in the universe, and step 3 (PR-008) gives it a cause.

Our definition: the universe as a whole is caused

Definition UniverseExcludesTheNecessary : Prop :=
  forall p, PartOf p Universe -> ~ EssenceIncludesExistence p.

(* Under our definition, case 3 cannot arise for the parts: no part is
   necessary. *)
Theorem narrow_no_necessary_part :
  UniverseExcludesTheNecessary -> ~ (exists p, PartOf p Universe /\ NecessaryInItself p).

English: the universe does not overlap with the necessary: none of its parts has its existence from its own nature.

Theorem narrow_no_necessary_part :
  UniverseExcludesTheNecessary -> ~ (exists p, PartOf p Universe /\ NecessaryInItself p).

English: under our definition case 3 cannot arise, because no part is necessary.

Theorem universe_as_a_whole_is_caused :
  MP008 -> MP010 -> UniverseExcludesTheNecessary ->
  Exists Universe -> (exists p, PartOf p Universe) ->
  ThroughAnother Universe.

English: under our definition, if the universe exists and has parts (OP-007), then the universe as a whole is caused. OP-006 is not used here: "not wholly necessary" follows from the definition itself.

How: none of its parts is necessary, so by MP-010 the universe is not necessary either. It exists, so it is possible, and by step 3 it has a cause.

Checks

These are illustrations of logical possibility only.

Example narrow_definition_model :
  let E := fun (_ : Th) => True in
  let Ess := fun (x : Th) => x = N in
  let G := fun (y x : Th) => y = N /\ x <> N in
  let Part := fun (p u : Th) => p = P /\ u = U in
  MP008 Th E Ess G /\ MP010 Th Ess Part /\ UniverseExcludesTheNecessary Th Ess Part U /\
  OP006_NotWhollyNecessary Th E Ess Part U /\ ThroughAnother Th G U.

English: under our definition, a universe U with a possible part P is given existence by a necessary N outside it. All premises hold and U is caused.

Example broad_definition_case3 :
  let E := fun (_ : Th) => True in
  let Ess := fun (x : Th) => x = N in
  let G := fun (y x : Th) => y = N /\ x = P in
  let Part := fun (p u : Th) => (p = N \/ p = P) /\ u = U in
  Mixed Th E Ess Part U /\ ThroughAnother Th G P.

English: under the broader definition, a universe with a necessary part N and a possible part P is mixed (case 3), and its possible part is caused by N. So under the broader definition case 3 is possible.

Example without_OP006_nothing_caused :
  let E := fun (_ : unit) => True in
  let Ess := fun (_ : unit) => True in
  let G := fun (_ _ : unit) => False in
  let Part := fun (_ _ : unit) => False in
  MP008 unit E Ess G /\ WhollyNecessary unit E Ess Part tt /\
  ~ (exists x, InUniverse unit Part tt x /\ ThroughAnother unit G x).

English (countermodel): a universe that is wholly necessary and uncaused. MP-008 holds, yet nothing in it is caused. So the observation OP-006 is needed.

Example without_MP008_possible_uncaused :
  let E := fun (_ : unit) => True in
  let Ess := fun (_ : unit) => False in
  let G := fun (_ _ : unit) => False in
  let Part := fun (_ _ : unit) => False in
  OP006_NotWhollyNecessary unit E Ess Part tt /\
  ~ (exists x, InUniverse unit Part tt x /\ ThroughAnother unit G x).

English (countermodel): something possible in the universe with no cause, a brute fact. So MP-008 is needed.

Scope

• It establishes that the universe is caused. Under our definition this means the universe as a whole. Under the broader definition it means the universe's possible part.
• It rests on one observation, OP-006: at the very least, the universe is not wholly necessary. Every other premise is already approved.
• It holds whether or not the universe is eternal. No time appears.

Lemma of_itself_is_necessary_in_itself :
  MP008 -> forall b, KalimaConclusion.Necessary Thing Gives Exists b -> NecessaryInItself b.

English: what kalima calls necessary (it exists and nothing gives it existence) is, by MP-008, necessary in Ibn Sīnā's sense too: its existence is from its own nature. The two arguments' notions of "necessary" agree.

Theorem kalima_unconditional :
  MP001 -> MP002 -> MP003 -> OP001 -> MP008 -> OP006 ->
  exists x b, InUniverse x /\ Gives b x /\ Exists b /\ NecessaryInItself b /\
              Exhaustiveness.Independent Thing DependsOn b.

English (the broader definition; it holds under ours too, and it needs OP-006): if the kalima postulates and MP-008 hold, and the universe is not wholly necessary, then something in the universe has a first cause b such that:

• b exists;
• b is necessary in itself;
• b depends on nothing, so there are no further causes beyond it.

Theorem kalima_unconditional_whole_universe :
  MP001 -> MP002 -> MP003 -> OP001 -> MP008 -> MP010 ->
  UniverseIsCaused.UniverseExcludesTheNecessary Thing EssenceIncludesExistence PartOf Universe ->
  Exists Universe -> (exists p, PartOf p Universe) ->
  exists b, Gives b Universe /\ Exists b /\ NecessaryInItself b /\
            Exhaustiveness.Independent Thing DependsOn b.

English (our definition: the universe does not overlap with the necessary; it uses OP-007 and not OP-006): if MP-010 holds and the universe exists and has parts, then the universe itself has a necessary first cause, beyond which there are no further causes.

Scope

• It establishes the conclusion of dalīl al-kalima without its "if".
• Beyond the already-approved postulates, each form needs one observation:
  • under the broader definition, OP-006: at the very least, the universe is not wholly necessary;
  • under our definition, OP-007: the universe exists and has parts.
• See PR-011 for the full division into four cases, and for what the two definitions of "the universe" mean for case 3.