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