% 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))).