Dalīl al-kalima in Leo-III

Given the four premises, Leo-III proves the conclusion on its own.

Leo-III is given the premises and searches for a proof by itself.

How to read the results:

Theorem means proved: Leo-III found a proof of the claim from the premises it was given.

Timeout (or no result) means not settled: Leo-III did not find a proof in the time allowed. This says nothing either way, neither true nor false. Wherever that happens, the claim is proved by another tool, and the page links to that proof.

← Dalīl al-kalima overview

Results

Leo-III 1.7.18 · 50-second limit

Question	Leo-III	Proof
Premise 1 · The four possibilities are the only ones	Not settled no proof found within 50 seconds; this proves nothing either way	Proved in Rocq: premise 1 in this exact form →
Premise 2 · Self-creation is impossible	Proved Theorem: Leo-III found a proof 1.3 s	See the input
Premise 3 · Circular creation is impossible	Not settled stopped without an answer; this proves nothing either way	Proved in Rocq: premise 3 in this exact form →
Premise 4 · No regress in the giving of existence	Proved Theorem: Leo-III found a proof 1.4 s	See the input
The conclusion, from the four premises	Proved Theorem: Leo-III found a proof 2.0 s	See the input
The universe is caused · broader definition	Proved Theorem: Leo-III found a proof 1.7 s	See the input
The universe is caused · our definition	Proved Theorem: Leo-III found a proof 1.6 s	See the input
The conclusion without the “if”	Proved Theorem: Leo-III found a proof 3.8 s	See the input
The conclusion, directly from the postulates	Proved Theorem: Leo-III found a proof 1.7 s	See the input

Every premise supplied to Leo-III in the conclusion problem has been machine-proved: premises 2 and 4 by Leo-III itself and by Rocq, premises 1 and 3 by Rocq. Rocq also proves that Leo-III's definition of “ultimately depends on” is the same relation used in the Rocq proof of premise 3. Complete output of every run: leo3_output.txt.

The inputs

Nine problems

Premise 1 · The four possibilities are the only ones

p1_exhaustive.p

From logic alone: every thing falls under at least one of the four cases (stated with “ultimately depends on” rather than chains).

Leo-III: Not settled no proof found within 50 seconds; this proves nothing either way · Proved in Rocq: premise 1 in this exact form →

Download p1_exhaustive.p

Show the full formalization

% Dalil al-kalima, Leo-III check.
% Premise 1 (relational form): every thing falls under at least one of the four cases.
% Rests on: definitions only (classical logic).

% Vocabulary.  Nothing is assumed about these symbols.
thf(gives_type, type, gives: $i > $i > $o).          % (gives @ Y @ X): Y gives existence to X
thf(through_type, type, through: $i > $i > $o).      % (through @ X @ Y): X has its existence through Y
thf(ex_type, type, ex: $i > $o).                     % (ex @ X): X exists
thf(u_type, type, u: $i).                            % the universe
thf(dep_type, type, dep: $i > $i > $o).
thf(independent_type, type, independent: $i > $o).
thf(reach_type, type, reach: $i > $i > $o).
thf(through_another_type, type, through_another: $i > $o).
thf(of_itself_type, type, of_itself: $i > $o).

% Definitions (conditional; none asserts that anything exists).
% X depends on Y: Y gives existence to X.
thf(dep_def, definition, dep = (^[X:$i, Y:$i]: (gives @ Y @ X))).
% X is independent: X depends on nothing.
thf(independent_def, definition, independent = (^[X:$i]: ![Y:$i]: ~ (dep @ X @ Y))).
% X ultimately depends on Y: one or more steps of dependence (least transitive relation containing dep).
thf(reach_def, definition, reach = (^[X:$i, Y:$i]: ![P:$i > $i > $o]:
      (((![A:$i, B:$i]: ((dep @ A @ B) => (P @ A @ B)))
        & (![A:$i, B:$i, C:$i]: (((P @ A @ B) & (P @ B @ C)) => (P @ A @ C))))
       => (P @ X @ Y)))).
% X has its existence through another: something gives X existence.
thf(through_another_def, definition, through_another = (^[X:$i]: ?[Y:$i]: (gives @ Y @ X))).
% X has existence of itself (is necessary): X exists and nothing gives X existence.
thf(of_itself_def, definition, of_itself = (^[X:$i]: ((ex @ X) & ~ (through_another @ X)))).

% The four cases for a thing X, in relational form.
thf(case1_type, type, case1: $i > $o).
thf(case2_type, type, case2: $i > $o).
thf(case3_type, type, case3: $i > $o).
thf(case4_type, type, case4: $i > $o).
% Case 1, self-creation: X, or something X ultimately depends on, depends on itself.
thf(case1_def, definition, case1 = (^[X:$i]: ?[Y:$i]: (((X = Y) | (reach @ X @ Y)) & (dep @ Y @ Y)))).
% Case 2, circularity: X, or something X ultimately depends on, lies on a longer circle.
thf(case2_def, definition, case2 = (^[X:$i]: ?[Y:$i]: (((X = Y) | (reach @ X @ Y)) & (reach @ Y @ Y) & ~ (dep @ Y @ Y)))).
% Case 3, endless regress: X lies in a collection S in which every member depends on another member.
thf(case3_def, definition, case3 = (^[X:$i]: ?[S:$i > $o]: ((S @ X) & (![A:$i]: ((S @ A) => ?[B:$i]: ((S @ B) & (dep @ A @ B))))))).
% Case 4, ends in the independent: X is independent, or ultimately depends on something independent.
thf(case4_def, definition, case4 = (^[X:$i]: ((independent @ X) | ?[Y:$i]: ((reach @ X @ Y) & (independent @ Y))))).

thf(premise1, conjecture, ![X:$i]: ((case1 @ X) | (case2 @ X) | (case3 @ X) | (case4 @ X))).

Premise 2 · Self-creation is impossible

p2_no_self_creation.p

From the two meaning postulates MP-001 and MP-002: nothing gives existence to itself.

Expected result: Proved Theorem: Leo-III found a proof (the output ends with SZS status Theorem)

Download p2_no_self_creation.p

Show the full formalization

% Dalil al-kalima, Leo-III check.
% Premise 2 (PR-002): nothing gives existence to itself.
% Rests on: MP-001, MP-002.

% Vocabulary.  Nothing is assumed about these symbols.
thf(gives_type, type, gives: $i > $i > $o).          % (gives @ Y @ X): Y gives existence to X
thf(through_type, type, through: $i > $i > $o).      % (through @ X @ Y): X has its existence through Y
thf(ex_type, type, ex: $i > $o).                     % (ex @ X): X exists
thf(u_type, type, u: $i).                            % the universe
thf(dep_type, type, dep: $i > $i > $o).
thf(independent_type, type, independent: $i > $o).
thf(reach_type, type, reach: $i > $i > $o).
thf(through_another_type, type, through_another: $i > $o).
thf(of_itself_type, type, of_itself: $i > $o).

% Definitions (conditional; none asserts that anything exists).
% X depends on Y: Y gives existence to X.
thf(dep_def, definition, dep = (^[X:$i, Y:$i]: (gives @ Y @ X))).
% X is independent: X depends on nothing.
thf(independent_def, definition, independent = (^[X:$i]: ![Y:$i]: ~ (dep @ X @ Y))).
% X ultimately depends on Y: one or more steps of dependence (least transitive relation containing dep).
thf(reach_def, definition, reach = (^[X:$i, Y:$i]: ![P:$i > $i > $o]:
      (((![A:$i, B:$i]: ((dep @ A @ B) => (P @ A @ B)))
        & (![A:$i, B:$i, C:$i]: (((P @ A @ B) & (P @ B @ C)) => (P @ A @ C))))
       => (P @ X @ Y)))).
% X has its existence through another: something gives X existence.
thf(through_another_def, definition, through_another = (^[X:$i]: ?[Y:$i]: (gives @ Y @ X))).
% X has existence of itself (is necessary): X exists and nothing gives X existence.
thf(of_itself_def, definition, of_itself = (^[X:$i]: ((ex @ X) & ~ (through_another @ X)))).

thf(mp001, axiom, ![X:$i, Y:$i]: ((gives @ Y @ X) => ~ (through @ Y @ X))).
thf(mp002, axiom, ![X:$i, Y:$i]: ((gives @ Y @ X) => (through @ X @ Y))).
thf(premise2, conjecture, ![X:$i]: ~ (gives @ X @ X)).

Premise 3 · Circular creation is impossible

p3_no_circle.p

From MP-001, MP-002 and MP-003: nothing ultimately depends on itself, however long the circle.

Leo-III: Not settled stopped without an answer; this proves nothing either way · Proved in Rocq: premise 3 in this exact form →

Download p3_no_circle.p

Show the full formalization

% Dalil al-kalima, Leo-III check.
% Premise 3 (PR-003): nothing ultimately depends on itself, however long the circle.
% Rests on: MP-001, MP-002, MP-003.

% Vocabulary.  Nothing is assumed about these symbols.
thf(gives_type, type, gives: $i > $i > $o).          % (gives @ Y @ X): Y gives existence to X
thf(through_type, type, through: $i > $i > $o).      % (through @ X @ Y): X has its existence through Y
thf(ex_type, type, ex: $i > $o).                     % (ex @ X): X exists
thf(u_type, type, u: $i).                            % the universe
thf(dep_type, type, dep: $i > $i > $o).
thf(independent_type, type, independent: $i > $o).
thf(reach_type, type, reach: $i > $i > $o).
thf(through_another_type, type, through_another: $i > $o).
thf(of_itself_type, type, of_itself: $i > $o).

% Definitions (conditional; none asserts that anything exists).
% X depends on Y: Y gives existence to X.
thf(dep_def, definition, dep = (^[X:$i, Y:$i]: (gives @ Y @ X))).
% X is independent: X depends on nothing.
thf(independent_def, definition, independent = (^[X:$i]: ![Y:$i]: ~ (dep @ X @ Y))).
% X ultimately depends on Y: one or more steps of dependence (least transitive relation containing dep).
thf(reach_def, definition, reach = (^[X:$i, Y:$i]: ![P:$i > $i > $o]:
      (((![A:$i, B:$i]: ((dep @ A @ B) => (P @ A @ B)))
        & (![A:$i, B:$i, C:$i]: (((P @ A @ B) & (P @ B @ C)) => (P @ A @ C))))
       => (P @ X @ Y)))).
% X has its existence through another: something gives X existence.
thf(through_another_def, definition, through_another = (^[X:$i]: ?[Y:$i]: (gives @ Y @ X))).
% X has existence of itself (is necessary): X exists and nothing gives X existence.
thf(of_itself_def, definition, of_itself = (^[X:$i]: ((ex @ X) & ~ (through_another @ X)))).

thf(mp001, axiom, ![X:$i, Y:$i]: ((gives @ Y @ X) => ~ (through @ Y @ X))).
thf(mp002, axiom, ![X:$i, Y:$i]: ((gives @ Y @ X) => (through @ X @ Y))).
thf(mp003, axiom, ![X:$i, Y:$i, Z:$i]: (((through @ X @ Y) & (through @ Y @ Z)) => (through @ X @ Z))).
thf(premise3, conjecture, ![X:$i]: ~ (reach @ X @ X)).

Premise 4 · No regress in the giving of existence

p4_no_regress.p

From the observational premise OP-001: whatever gives existence has not itself received it, so existence-giving never forms a chain, let alone an endless one.

Expected result: Proved Theorem: Leo-III found a proof (the output ends with SZS status Theorem)

Download p4_no_regress.p

Show the full formalization

% Dalil al-kalima, Leo-III check.
% Premise 4 (PR-004): no two-step giving of existence, hence no regress of existence-giving.
% Rests on: OP-001.

% Vocabulary.  Nothing is assumed about these symbols.
thf(gives_type, type, gives: $i > $i > $o).          % (gives @ Y @ X): Y gives existence to X
thf(through_type, type, through: $i > $i > $o).      % (through @ X @ Y): X has its existence through Y
thf(ex_type, type, ex: $i > $o).                     % (ex @ X): X exists
thf(u_type, type, u: $i).                            % the universe
thf(dep_type, type, dep: $i > $i > $o).
thf(independent_type, type, independent: $i > $o).
thf(reach_type, type, reach: $i > $i > $o).
thf(through_another_type, type, through_another: $i > $o).
thf(of_itself_type, type, of_itself: $i > $o).

% Definitions (conditional; none asserts that anything exists).
% X depends on Y: Y gives existence to X.
thf(dep_def, definition, dep = (^[X:$i, Y:$i]: (gives @ Y @ X))).
% X is independent: X depends on nothing.
thf(independent_def, definition, independent = (^[X:$i]: ![Y:$i]: ~ (dep @ X @ Y))).
% X ultimately depends on Y: one or more steps of dependence (least transitive relation containing dep).
thf(reach_def, definition, reach = (^[X:$i, Y:$i]: ![P:$i > $i > $o]:
      (((![A:$i, B:$i]: ((dep @ A @ B) => (P @ A @ B)))
        & (![A:$i, B:$i, C:$i]: (((P @ A @ B) & (P @ B @ C)) => (P @ A @ C))))
       => (P @ X @ Y)))).
% X has its existence through another: something gives X existence.
thf(through_another_def, definition, through_another = (^[X:$i]: ?[Y:$i]: (gives @ Y @ X))).
% X has existence of itself (is necessary): X exists and nothing gives X existence.
thf(of_itself_def, definition, of_itself = (^[X:$i]: ((ex @ X) & ~ (through_another @ X)))).

thf(op001, axiom, ![X:$i, Y:$i]: ((gives @ Y @ X) => (of_itself @ Y))).
thf(premise4, conjecture, ![X:$i, Y:$i, Z:$i]: ((gives @ Y @ X) => ~ (gives @ Z @ Y))).

The conclusion, from the four premises

assembly.p

The four premises exactly as proved, together with the argument's “if the universe is caused”. Conclusion: the universe ultimately depends on something that depends on nothing.

Expected result: Proved Theorem: Leo-III found a proof (the output ends with SZS status Theorem)

Download assembly.p

Show the full formalization

% Dalil al-kalima, Leo-III check.
% The conclusion from the four premises, each supplied exactly as proved
% (premise 1 by p1_exhaustive.p; premises 2-4 by PR-002, PR-003, PR-004 and p2-p4 here),
% together with the argument's antecedent: the universe is caused.

% Vocabulary.  Nothing is assumed about these symbols.
thf(gives_type, type, gives: $i > $i > $o).          % (gives @ Y @ X): Y gives existence to X
thf(through_type, type, through: $i > $i > $o).      % (through @ X @ Y): X has its existence through Y
thf(ex_type, type, ex: $i > $o).                     % (ex @ X): X exists
thf(u_type, type, u: $i).                            % the universe
thf(dep_type, type, dep: $i > $i > $o).
thf(independent_type, type, independent: $i > $o).
thf(reach_type, type, reach: $i > $i > $o).
thf(through_another_type, type, through_another: $i > $o).
thf(of_itself_type, type, of_itself: $i > $o).

% Definitions (conditional; none asserts that anything exists).
% X depends on Y: Y gives existence to X.
thf(dep_def, definition, dep = (^[X:$i, Y:$i]: (gives @ Y @ X))).
% X is independent: X depends on nothing.
thf(independent_def, definition, independent = (^[X:$i]: ![Y:$i]: ~ (dep @ X @ Y))).
% X ultimately depends on Y: one or more steps of dependence (least transitive relation containing dep).
thf(reach_def, definition, reach = (^[X:$i, Y:$i]: ![P:$i > $i > $o]:
      (((![A:$i, B:$i]: ((dep @ A @ B) => (P @ A @ B)))
        & (![A:$i, B:$i, C:$i]: (((P @ A @ B) & (P @ B @ C)) => (P @ A @ C))))
       => (P @ X @ Y)))).
% X has its existence through another: something gives X existence.
thf(through_another_def, definition, through_another = (^[X:$i]: ?[Y:$i]: (gives @ Y @ X))).
% X has existence of itself (is necessary): X exists and nothing gives X existence.
thf(of_itself_def, definition, of_itself = (^[X:$i]: ((ex @ X) & ~ (through_another @ X)))).

% The four cases for a thing X, in relational form.
thf(case1_type, type, case1: $i > $o).
thf(case2_type, type, case2: $i > $o).
thf(case3_type, type, case3: $i > $o).
thf(case4_type, type, case4: $i > $o).
% Case 1, self-creation: X, or something X ultimately depends on, depends on itself.
thf(case1_def, definition, case1 = (^[X:$i]: ?[Y:$i]: (((X = Y) | (reach @ X @ Y)) & (dep @ Y @ Y)))).
% Case 2, circularity: X, or something X ultimately depends on, lies on a longer circle.
thf(case2_def, definition, case2 = (^[X:$i]: ?[Y:$i]: (((X = Y) | (reach @ X @ Y)) & (reach @ Y @ Y) & ~ (dep @ Y @ Y)))).
% Case 3, endless regress: X lies in a collection S in which every member depends on another member.
thf(case3_def, definition, case3 = (^[X:$i]: ?[S:$i > $o]: ((S @ X) & (![A:$i]: ((S @ A) => ?[B:$i]: ((S @ B) & (dep @ A @ B))))))).
% Case 4, ends in the independent: X is independent, or ultimately depends on something independent.
thf(case4_def, definition, case4 = (^[X:$i]: ((independent @ X) | ?[Y:$i]: ((reach @ X @ Y) & (independent @ Y))))).

thf(premise1, axiom, ![X:$i]: ((case1 @ X) | (case2 @ X) | (case3 @ X) | (case4 @ X))).  % proved: p1_exhaustive.p
thf(premise2, axiom, ![X:$i]: ~ (gives @ X @ X)).                                              % proved: PR-002, p2
thf(premise3, axiom, ![X:$i]: ~ (reach @ X @ X)).                                              % proved: PR-003, p3
thf(premise4, axiom, ![X:$i, Y:$i, Z:$i]: ((gives @ Y @ X) => ~ (gives @ Z @ Y))).             % proved: PR-004, p4
thf(antecedent, axiom, through_another @ u).                                                   % the argument's "if"
% Conclusion: the universe ultimately depends on something that depends on nothing.
thf(conclusion, conjecture, ?[B:$i]: ((reach @ u @ B) & (independent @ B))).

The universe is caused · broader definition

pr011_broad.p

From MP-008 and the observation that the universe is not wholly necessary (OP-006): something in the universe is possible and caused.

Expected result: Proved Theorem: Leo-III found a proof (the output ends with SZS status Theorem)

Download pr011_broad.p

Show the full formalization

% Leo-III cross-check.
% PR-011, broader definition: MP-008 and OP-006 give something caused in the universe.
% Vocabulary.  Nothing is assumed about these symbols.
thf(ex_type, type, ex: $i > $o).                     % (ex @ X): X exists
thf(ess_type, type, ess: $i > $o).                   % (ess @ X): X's existence is from its nature
thf(gives_type, type, gives: $i > $i > $o).          % (gives @ Y @ X): Y gives existence to X
thf(nec_type, type, nec: $i > $o).
thf(poss_type, type, poss: $i > $o).
thf(ta_type, type, through_another: $i > $o).
thf(nec_def, definition, nec = (^[X:$i]: ((ex @ X) & (ess @ X)))).            % necessary in itself
thf(poss_def, definition, poss = (^[X:$i]: ((ex @ X) & ~ (ess @ X)))).        % possible in itself
thf(ta_def, definition, through_another = (^[X:$i]: ?[Y:$i]: (gives @ Y @ X))). % something gives X existence
thf(part_type, type, part: $i > $i > $o).            % (part @ P @ U): P is a part of U
thf(u_type, type, u: $i).                            % the universe
thf(mp008, axiom, ![X:$i]: (((ex @ X) & ~ (through_another @ X)) => (ess @ X))).   % MP-008
thf(op006, axiom, ?[X:$i]: (((X = u) | (part @ X @ u)) & (poss @ X))).                  % OP-006
thf(conclusion, conjecture, ?[X:$i]: (((X = u) | (part @ X @ u)) & (poss @ X) & (through_another @ X))).

The universe is caused · our definition

pr011_narrow.p

From MP-008, MP-010, our definition (the universe does not include the necessary) and the observation that it exists and has parts (OP-007): the universe as a whole is caused.

Expected result: Proved Theorem: Leo-III found a proof (the output ends with SZS status Theorem)

Download pr011_narrow.p

Show the full formalization

% Leo-III cross-check.
% PR-011, our definition: MP-008, MP-010, the definition and OP-007 give that the universe is caused.
% Vocabulary.  Nothing is assumed about these symbols.
thf(ex_type, type, ex: $i > $o).                     % (ex @ X): X exists
thf(ess_type, type, ess: $i > $o).                   % (ess @ X): X's existence is from its nature
thf(gives_type, type, gives: $i > $i > $o).          % (gives @ Y @ X): Y gives existence to X
thf(nec_type, type, nec: $i > $o).
thf(poss_type, type, poss: $i > $o).
thf(ta_type, type, through_another: $i > $o).
thf(nec_def, definition, nec = (^[X:$i]: ((ex @ X) & (ess @ X)))).            % necessary in itself
thf(poss_def, definition, poss = (^[X:$i]: ((ex @ X) & ~ (ess @ X)))).        % possible in itself
thf(ta_def, definition, through_another = (^[X:$i]: ?[Y:$i]: (gives @ Y @ X))). % something gives X existence
thf(part_type, type, part: $i > $i > $o).
thf(u_type, type, u: $i).
thf(mp008, axiom, ![X:$i]: (((ex @ X) & ~ (through_another @ X)) => (ess @ X))).   % MP-008
thf(mp010, axiom, ![A:$i]: (((?[P:$i]: (part @ P @ A)) & (![P:$i]: ((part @ P @ A) => ~ (ess @ P)))) => ~ (ess @ A))).  % MP-010
thf(narrow, axiom, ![P:$i]: ((part @ P @ u) => ~ (ess @ P))).                           % our definition of the universe
thf(op007, axiom, (ex @ u) & (?[P:$i]: (part @ P @ u))).                                % OP-007
thf(conclusion, conjecture, through_another @ u).

The conclusion without the “if”

unconditional_assembly.p

The kalima conclusion (proved for anything in the role of the universe) with the result that the universe is caused: something in the universe has a necessary first cause that depends on nothing.

Expected result: Proved Theorem: Leo-III found a proof (the output ends with SZS status Theorem)

Download unconditional_assembly.p

Show the full formalization

% Leo-III cross-check.
% Dalil al-kalima, unconditional: the kalima conclusion (proved for every thing in the role
% of the universe) with PR-011's result (broader definition) and MP-008.
% Vocabulary.  Nothing is assumed about these symbols.
thf(ex_type, type, ex: $i > $o).                     % (ex @ X): X exists
thf(ess_type, type, ess: $i > $o).                   % (ess @ X): X's existence is from its nature
thf(gives_type, type, gives: $i > $i > $o).          % (gives @ Y @ X): Y gives existence to X
thf(nec_type, type, nec: $i > $o).
thf(poss_type, type, poss: $i > $o).
thf(ta_type, type, through_another: $i > $o).
thf(nec_def, definition, nec = (^[X:$i]: ((ex @ X) & (ess @ X)))).            % necessary in itself
thf(poss_def, definition, poss = (^[X:$i]: ((ex @ X) & ~ (ess @ X)))).        % possible in itself
thf(ta_def, definition, through_another = (^[X:$i]: ?[Y:$i]: (gives @ Y @ X))). % something gives X existence
thf(part_type, type, part: $i > $i > $o).
thf(u_type, type, u: $i).
thf(independent_type, type, independent: $i > $o).
thf(independent_def, definition, independent = (^[X:$i]: ![Y:$i]: ~ (gives @ Y @ X))).
% KalimaConclusion.kalima_conclusion, for every thing in the role of the universe:
thf(kalima, axiom, ![X:$i]: ((through_another @ X) => ?[B:$i]: ((gives @ B @ X) & (ex @ B) & ~ (through_another @ B) & (independent @ B)))).
% PR-011 something_in_universe_is_caused (MP-008, OP-006):
thf(pr011, axiom, ?[X:$i]: (((X = u) | (part @ X @ u)) & (poss @ X) & (through_another @ X))).
thf(mp008, axiom, ![X:$i]: (((ex @ X) & ~ (through_another @ X)) => (ess @ X))).   % MP-008
thf(conclusion, conjecture, ?[X:$i, B:$i]: (((X = u) | (part @ X @ u)) & (gives @ B @ X) & (nec @ B) & (independent @ B))).

The conclusion, directly from the postulates

direct.p

MP-001 to MP-003, OP-001 and “the universe is caused”. Conclusion: something that exists of itself, and depends on nothing, gives existence to the universe.

Expected result: Proved Theorem: Leo-III found a proof (the output ends with SZS status Theorem)

Download direct.p

Show the full formalization

% Dalil al-kalima, Leo-III check.
% The full conclusion directly from the approved postulates and the antecedent.

% Vocabulary.  Nothing is assumed about these symbols.
thf(gives_type, type, gives: $i > $i > $o).          % (gives @ Y @ X): Y gives existence to X
thf(through_type, type, through: $i > $i > $o).      % (through @ X @ Y): X has its existence through Y
thf(ex_type, type, ex: $i > $o).                     % (ex @ X): X exists
thf(u_type, type, u: $i).                            % the universe
thf(dep_type, type, dep: $i > $i > $o).
thf(independent_type, type, independent: $i > $o).
thf(reach_type, type, reach: $i > $i > $o).
thf(through_another_type, type, through_another: $i > $o).
thf(of_itself_type, type, of_itself: $i > $o).

% Definitions (conditional; none asserts that anything exists).
% X depends on Y: Y gives existence to X.
thf(dep_def, definition, dep = (^[X:$i, Y:$i]: (gives @ Y @ X))).
% X is independent: X depends on nothing.
thf(independent_def, definition, independent = (^[X:$i]: ![Y:$i]: ~ (dep @ X @ Y))).
% X ultimately depends on Y: one or more steps of dependence (least transitive relation containing dep).
thf(reach_def, definition, reach = (^[X:$i, Y:$i]: ![P:$i > $i > $o]:
      (((![A:$i, B:$i]: ((dep @ A @ B) => (P @ A @ B)))
        & (![A:$i, B:$i, C:$i]: (((P @ A @ B) & (P @ B @ C)) => (P @ A @ C))))
       => (P @ X @ Y)))).
% X has its existence through another: something gives X existence.
thf(through_another_def, definition, through_another = (^[X:$i]: ?[Y:$i]: (gives @ Y @ X))).
% X has existence of itself (is necessary): X exists and nothing gives X existence.
thf(of_itself_def, definition, of_itself = (^[X:$i]: ((ex @ X) & ~ (through_another @ X)))).

% Approved meaning postulates and observational premise.
thf(mp001, axiom, ![X:$i, Y:$i]: ((gives @ Y @ X) => ~ (through @ Y @ X))).                  % MP-001
thf(mp002, axiom, ![X:$i, Y:$i]: ((gives @ Y @ X) => (through @ X @ Y))).                    % MP-002
thf(mp003, axiom, ![X:$i, Y:$i, Z:$i]: (((through @ X @ Y) & (through @ Y @ Z)) => (through @ X @ Z))).  % MP-003
thf(op001, axiom, ![X:$i, Y:$i]: ((gives @ Y @ X) => (of_itself @ Y))).                     % OP-001

thf(antecedent, axiom, through_another @ u).                                                   % the argument's "if"
% Conclusion: something necessary (existing of itself), depending on nothing, gives existence to the universe.
thf(conclusion, conjecture, ?[B:$i]: ((gives @ B @ u) & (ex @ B) & (of_itself @ B) & (independent @ B))).

Formal statements and their English equivalents

Every formula, in plain English

Vocabulary (in every file)

thf(gives_type, type, gives: $i > $i > $o).
thf(through_type, type, through: $i > $i > $o).
thf(ex_type, type, ex: $i > $o).
thf(u_type, type, u: $i).

English:

gives @ Y @ X: Y gives existence to X.
through @ X @ Y: X has its existence through Y.
ex @ X: X exists.
u: the universe.

Nothing is assumed about these symbols.

Definitions (in every file)

thf(dep_def, definition, dep = (^[X:$i, Y:$i]: (gives @ Y @ X))).

English: X depends on Y means Y gives existence to X.

thf(independent_def, definition, independent = (^[X:$i]: ![Y:$i]: ~ (dep @ X @ Y))).

English: X is independent if X depends on nothing.

thf(reach_def, definition, reach = (^[X:$i, Y:$i]: ![P:$i > $i > $o]:
      (((![A:$i, B:$i]: ((dep @ A @ B) => (P @ A @ B)))
        & (![A:$i, B:$i, C:$i]: (((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. In other words, there is a chain of one or more steps of dependence from X to Y. Rocq proves this is the same as PR-003's clos_trans.

thf(through_another_def, definition, through_another = (^[X:$i]: ?[Y:$i]: (gives @ Y @ X))).

English: X has its existence through another if something gives X existence.

thf(of_itself_def, definition, of_itself = (^[X:$i]: ((ex @ X) & ~ (through_another @ X)))).

English: X has existence of itself, meaning it is necessary, if X exists and nothing gives it existence.

The four cases, relational form (`p1_exhaustive.p`, `assembly.p`)

thf(case1_def, definition, case1 = (^[X:$i]: ?[Y:$i]: (((X = Y) | (reach @ X @ Y)) & (dep @ Y @ Y)))).

English (case 1, self-creation): X, or something X ultimately depends on, depends on itself.

thf(case2_def, definition, case2 = (^[X:$i]: ?[Y:$i]: (((X = Y) | (reach @ X @ Y)) & (reach @ Y @ Y) & ~ (dep @ Y @ Y)))).

English (case 2, circularity): X, or something X ultimately depends on, lies on a circle longer than one step.

thf(case3_def, definition, case3 = (^[X:$i]: ?[S:$i > $o]: ((S @ X) & (![A:$i]: ((S @ A) => ?[B:$i]: ((S @ B) & (dep @ A @ B))))))).

English (case 3, endless regress): X belongs to some collection in which every member depends on another member of the collection.

thf(case4_def, definition, case4 = (^[X:$i]: ((independent @ X) | ?[Y:$i]: ((reach @ X @ Y) & (independent @ Y))))).

English (case 4, ends in the independent): X is independent, or X ultimately depends on something independent.

Approved postulates (`direct.p`; the premise files use the ones they need)

thf(mp001, axiom, ![X:$i, Y:$i]: ((gives @ Y @ X) => ~ (through @ Y @ X))).
thf(mp002, axiom, ![X:$i, Y:$i]: ((gives @ Y @ X) => (through @ X @ Y))).
thf(mp003, axiom, ![X:$i, Y:$i, Z:$i]: (((through @ X @ Y) & (through @ Y @ Z)) => (through @ X @ Z))).
thf(op001, axiom, ![X:$i, Y:$i]: ((gives @ Y @ X) => (of_itself @ Y))).

English:

MP-001: what gives existence to X does not have its existence through X.
MP-002: what is given existence by Y has its existence through Y.
MP-003: existence-through is inherited along a chain.
OP-001: only what has existence of itself gives existence.

Conjectures and supplied premises

thf(premise1, conjecture, ![X:$i]: ((case1 @ X) | (case2 @ X) | (case3 @ X) | (case4 @ X))).

**English (p1_exhaustive.p):** everything falls under at least one of the four cases.

thf(premise2, conjecture, ![X:$i]: ~ (gives @ X @ X)).

**English (p2_no_self_creation.p):** nothing gives existence to itself.

thf(premise3, conjecture, ![X:$i]: ~ (reach @ X @ X)).

**English (p3_no_circle.p):** nothing ultimately depends on itself.

thf(premise4, conjecture, ![X:$i, Y:$i, Z:$i]: ((gives @ Y @ X) => ~ (gives @ Z @ Y))).

**English (p4_no_regress.p):** whatever gives existence has not itself received existence. So there is no chain of existence-giving, and no regress.

In assembly.p these four statements are supplied as axioms. Each is cited with the proof behind it, as above. It also supplies:

thf(antecedent, axiom, through_another @ u).

English: the argument's "if": something gives existence to the universe.

thf(conclusion, conjecture, ?[B:$i]: ((reach @ u @ B) & (independent @ B))).

**English (assembly.p):** the universe ultimately depends on something that depends on nothing. That is a first cause beyond which there are no further causes.

thf(conclusion, conjecture, ?[B:$i]: ((gives @ B @ u) & (ex @ B) & (of_itself @ B) & (independent @ B))).

**English (direct.p):** something that exists of itself (is necessary) and depends on nothing gives existence to the universe.

`unconditional_assembly.p`

thf(kalima, axiom, ![X:$i]: ((through_another @ X) => ?[B:$i]: ((gives @ B @ X) & (ex @ B) & ~ (through_another @ B) & (independent @ B)))).

English: the kalima conclusion, proved in Rocq for every thing in the role of the universe. Whatever is caused has a giver that exists, has existence of itself, and depends on nothing.

thf(pr011, axiom, ?[X:$i]: (((X = u) | (part @ X @ u)) & (poss @ X) & (through_another @ X))).

English: PR-011, proved (broader definition). Something in the universe is possible and caused.

thf(conclusion, conjecture, ?[X:$i, B:$i]: (((X = u) | (part @ X @ u)) & (gives @ B @ X) & (nec @ B) & (independent @ B))).

English: something in the universe has a giver that is necessary in itself and depends on nothing. This is the kalima conclusion without its "if".

The file's vocabulary and MP-008 are the same as in the al-imkān Leo-III files; see arguments/dalil-al-imkan/guides/leo3-crosscheck.md.

Scope

Leo-III confirms the argument's final step independently. Given the four premises, and the universe being caused, there is a first cause that depends on nothing.
Premises 2 and 4: Leo-III also derives them from the approved postulates.
Premises 1 and 3: Leo-III could not find proofs within its time limit. They rest on Rocq: PR-001 rocq-relational and PR-003.
A timeout is not a result. It is recorded as such, never as a proof.

The universe is caused

pr011_broad.p · pr011_narrow.p

`pr011_broad.p`

thf(ex_type, type, ex: $i > $o).

English: "X exists".

thf(ess_type, type, ess: $i > $o).

English: "X's existence is from its own nature".

thf(gives_type, type, gives: $i > $i > $o).

English: "Y gives existence to X".

thf(nec_type, type, nec: $i > $o).

English: "X is necessary in itself" (declared; defined below).

thf(poss_type, type, poss: $i > $o).

English: "X is possible in itself" (declared; defined below).

thf(ta_type, type, through_another: $i > $o).

English: "X has its existence through another" (declared; defined below).

thf(nec_def, definition, nec = (^[X:$i]: ((ex @ X) & (ess @ X)))).

English: X is necessary in itself: it exists, and its existence is from its own nature.

thf(poss_def, definition, poss = (^[X:$i]: ((ex @ X) & ~ (ess @ X)))).

English: X is possible in itself: it exists, and its existence is not from its own nature.

thf(ta_def, definition, through_another = (^[X:$i]: ?[Y:$i]: (gives @ Y @ X))).

English: X has its existence through another: something gives it existence.

thf(part_type, type, part: $i > $i > $o).

English: "P is a part of U", physical or metaphysical.

thf(u_type, type, u: $i).

English: the universe.

thf(mp008, axiom, ![X:$i]: (((ex @ X) & ~ (through_another @ X)) => (ess @ X))).

English: MP-008: if something exists and nothing gives it existence, its existence is from its own nature.

thf(op006, axiom, ?[X:$i]: (((X = u) | (part @ X @ u)) & (poss @ X))).

English: OP-006: at the very least, the universe is not wholly necessary. Something in it is possible. This is used for the broader definition.

thf(conclusion, conjecture, ?[X:$i]: (((X = u) | (part @ X @ u)) & (poss @ X) & (through_another @ X))).

English: the conjecture to be proved (see the table for each file).

`pr011_narrow.p`

ex_type: as above.

ess_type: as above.

gives_type: as above.

nec_type: as above.

poss_type: as above.

ta_type: as above.

nec_def: as above.

poss_def: as above.

ta_def: as above.

part_type: as above.

u_type: as above.

mp008: as above.

thf(mp010, axiom, ![A:$i]: (((?[P:$i]: (part @ P @ A)) & (![P:$i]: ((part @ P @ A) => ~ (ess @ P)))) => ~ (ess @ A))).

English: MP-010: a collection that has parts, none of whose existence is from their own nature, does not have its existence from its own nature either.

thf(narrow, axiom, ![P:$i]: ((part @ P @ u) => ~ (ess @ P))).

English: our definition of the universe: none of its parts has its existence from its own nature.

thf(op007, axiom, (ex @ u) & (?[P:$i]: (part @ P @ u))).

English: OP-007: the universe exists and has parts. This is used for our definition.

thf(conclusion, conjecture, through_another @ u).

English: the conjecture to be proved (see the table for each file).

Scope

Leo-III independently confirms PR-011 under both definitions, directly from the postulates.

Run it yourself

Leo-III 1.7.18 · 50-second search limit

Load any input above into this editor, or paste your own, and run it on this server's Leo-III 1.7.18 in an isolated, network-disabled worker. Runs are limited to 60 seconds.

Isolated run · 60-second limit · output retained 2h

Output

The argument in Leo-III

Given the four premises, Leo-III proves the conclusion on its own.

Results

The inputs

Premise 1 · The four possibilities are the only ones

Premise 2 · Self-creation is impossible

Premise 3 · Circular creation is impossible

Premise 4 · No regress in the giving of existence

The conclusion, from the four premises

The universe is caused · broader definition

The universe is caused · our definition

The conclusion without the “if”

The conclusion, directly from the postulates

Formal statements and their English equivalents

Vocabulary (in every file)

Definitions (in every file)

The four cases, relational form (p1_exhaustive.p, assembly.p)

Approved postulates (direct.p; the premise files use the ones they need)

Conjectures and supplied premises

unconditional_assembly.p

Scope

The universe is caused

pr011_broad.p

pr011_narrow.p

Scope

Run it yourself

The four cases, relational form (`p1_exhaustive.p`, `assembly.p`)

Approved postulates (`direct.p`; the premise files use the ones they need)

`unconditional_assembly.p`

`pr011_broad.p`

`pr011_narrow.p`