imkan_b_short.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(op001, axiom, ![X:$i, Y:$i]: ((gives @ Y @ X) => ((ex @ Y) & ~ (through_another @ Y)))).
English: OP-001: only what has existence of itself gives existence.
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(sp001, axiom, ?[X:$i]: (ex @ X)).
English: SP-001: something exists. This is self-evident.
thf(conclusion, conjecture, ?[N:$i]: (nec @ N)).
English: the conjecture to be proved (see the table for each file).
imkan_a_assembly_abstract.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.
thf(mem_type, type, mem: $i > $i > $o).
English: "P is a member of the collection A".
thf(agg_type, type, agg: $i > $o).
English: "A is the aggregate of all possibles" (declared).
thf(step1, axiom, ![X:$i]: ((ex @ X) => ((nec @ X) | (poss @ X)))).
English: step 1, proved (PR-006): every existent is necessary or possible in itself.
thf(step3, axiom, ![X:$i]: ((poss @ X) => (through_another @ X))).
English: step 3, proved (PR-008): whatever is possible in itself has its existence through another.
thf(step4, axiom, ![X:$i]: ~ (gives @ X @ X)).
English: step 4, proved (PR-002): nothing gives existence to itself.
thf(mp009, axiom, (?[P:$i]: (poss @ P)) => (?[A:$i]: ((agg @ A) & (ex @ A)))).
English: MP-009: if some possible thing exists, there is an existing aggregate of all the possibles.
thf(step6, axiom, ![A:$i]: (((agg @ A) & (ex @ A) & (?[P:$i]: ((P != A) & (poss @ P)))) => (poss @ A))).
English: step 6, proved (PR-009): the existing aggregate, if some possible other than it exists, is itself possible.
thf(step11, axiom, ![A:$i, C:$i]: (((agg @ A) & (gives @ C @ A)) => (nec @ C))).
English: steps 7 to 11, proved (PR-010): whatever gives existence to the aggregate is necessary in itself.
thf(mp012, axiom, ![Y:$i, X:$i]: ((gives @ Y @ X) => (ex @ Y))).
English: MP-012: whatever gives existence exists.
sp001: as above.
conclusion: as above.
imkan_a_1_case_split.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.
mem_type: as above.
agg_type: as above.
thf(agg_def, definition, agg = (^[A:$i]: ((![P:$i]: ((P != A) => ((mem @ P @ A) <=> (poss @ P)))) & ~ (mem @ A @ A)))).
English: A is the aggregate of all possibles: its members are exactly the possibles other than A, and A is not a member of itself.
step1: as above.
thf(possible_case, axiom, (?[P:$i]: (poss @ P)) => (?[N:$i]: (nec @ N))).
English: proved in Rocq (necessary_existent_from_a_possible) and by parts 2a and 2b: if a possible thing exists, a Necessary Existent exists.
sp001: as above.
conclusion: as above.
imkan_a_2a_member_case.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.
mem_type: as above.
agg_type: as above.
step3: as above.
step6: as above.
step11: as above.
thf(a_type, type, a: $i).
English: a particular thing, A.
thf(case_agg, axiom, (agg @ a) & (ex @ a)).
English: this case: A is the existing aggregate of all possibles.
thf(case_member, axiom, ?[Q:$i]: ((Q != a) & (poss @ Q))).
English: this case: some possible thing other than A exists.
conclusion: as above.
imkan_a_2b_only_aggregate_case.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.
mem_type: as above.
agg_type: as above.
agg_def: as above.
step1: as above.
step3: as above.
step4: as above.
mp009: as above.
step6: as above.
step11: as above.
mp012: as above.
a_type: as above.
thf(p_type, type, p: $i).
English: a particular thing, P.
case_agg: as above.
thf(case_possible, axiom, poss @ p).
English: this case: P is possible in itself.
thf(case_only, axiom, ~ (?[Q:$i]: ((Q != a) & (poss @ Q)))).
English: this case: no possible thing other than A exists.
conclusion: as above.
imkan_a_assembly.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.
mem_type: as above.
agg_type: as above.
agg_def: as above.
step1: as above.
step3: as above.
step4: as above.
mp009: as above.
step6: as above.
step11: as above.
mp012: as above.
sp001: as above.
conclusion: as above.
Scope
Leo-III independently confirms that the proved steps of dalīl al-imkān yield its conclusion, by both routes. The steps themselves are proved in Rocq.
