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