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