Dalīl al-kalima · Counterexample search
The argument in Z3
Z3 searches for a way the argument could fail, and finds none.
Z3 works by trying to break the argument. It is given the premises together with the opposite of what we claim, and asked: can all of this be true at once?
How to read the results:
unsat means no, impossible. When the opposite of a claim is impossible, the claim is confirmed. This is the
result we want for every premise and for the conclusion.
sat means yes, possible. We want it in two kinds of check: that the premises can all hold together (they are
consistent), and that removing a premise lets the claim fail (so that premise is really needed).
Premise 1
Not expressible in Z3Premise 1 concerns chains of every length, including endless ones. Z3 works with statements it can check by search and cannot express “every chain, however long”. Premise 1 is proved in Rocq: the chain form and the relational form.
The checks
Formal statements and their English equivalentsPremise 2 · Self-creation is impossible
no_self_creation.smt2
Show the full formalization
; PR-002: Nothing gives existence to itself. Independent cross-check in Z3.
; Z3 is first-order and assumes a non-empty domain. That assumption is
; harmless here: each check below names its own things explicitly, and the
; main check refutes the existence of a self-giver rather than relying on one.
; No time appears anywhere.
(declare-sort Thing 0)
(declare-fun Gives (Thing Thing) Bool) ; (Gives y x): y gives existence to x
(declare-fun Through (Thing Thing) Bool) ; (Through x y): x has its existence through y
(define-fun MP001_Giver () Bool ; what lacks a thing cannot give it
(forall ((x Thing) (y Thing)) (=> (Gives y x) (not (Through y x)))))
(define-fun MP002_Receiver () Bool ; the receiver has its existence through the giver
(forall ((x Thing) (y Thing)) (=> (Gives y x) (Through x y))))
; Check 1 (the proof): both postulates plus a self-giver. Expected: unsat.
(push)
(assert MP001_Giver)
(assert MP002_Receiver)
(assert (exists ((x Thing)) (Gives x x)))
(echo "check 1: MP-001 + MP-002 + something gives existence to itself (expect unsat)")
(check-sat)
(pop)
; Check 2 (countermodel): drop MP-001. Expected: sat.
(push)
(assert MP002_Receiver)
(assert (exists ((x Thing)) (Gives x x)))
(echo "check 2: MP-002 only + self-giver (expect sat: MP-001 is needed)")
(check-sat)
(pop)
; Check 3 (countermodel): drop MP-002. Expected: sat.
(push)
(assert MP001_Giver)
(assert (exists ((x Thing)) (Gives x x)))
(echo "check 3: MP-001 only + self-giver (expect sat: MP-002 is needed)")
(check-sat)
(pop)
; Check 4 (non-vacuity): both postulates while one thing gives existence to
; another. Expected: sat.
(push)
(assert MP001_Giver)
(assert MP002_Receiver)
(declare-const a Thing)
(declare-const b Thing)
(assert (Gives a b))
(echo "check 4: MP-001 + MP-002 + a gives existence to b (expect sat: postulates allow giving)")
(check-sat)
(pop)
(declare-sort Thing 0)
(declare-fun Gives (Thing Thing) Bool)
(declare-fun Through (Thing Thing) Bool)English: there is some kind of things, and two relations:
(Gives y x): y gives existence to x;(Through x y): x has its existence through y.
No time appears.
(define-fun MP001_Giver () Bool
(forall ((x Thing) (y Thing)) (=> (Gives y x) (not (Through y x)))))English (MP-001): whatever gives existence to x does not have its own existence through x.
(define-fun MP002_Receiver () Bool
(forall ((x Thing) (y Thing)) (=> (Gives y x) (Through x y))))English (MP-002): whatever is given existence by y has its existence through y.
define-fun only names these statements. They are not asserted until a check asserts them.
Check 1 (the proof). Assert MP-001, MP-002 and (exists ((x Thing)) (Gives x x)). English: both postulates hold, and something gives existence to itself. Result: unsat. No such world exists, so the postulates rule out self-creation.
Check 2 (countermodel). Assert MP-002 and a self-giver, without MP-001. Result: sat. Without MP-001, self-creation is consistent, so MP-001 is needed.
Check 3 (countermodel). Assert MP-001 and a self-giver, without MP-002. Result: sat. Without MP-002, self-creation is consistent, so MP-002 is needed.
Check 4 (non-vacuity). Assert both postulates, two named things a and b, and (Gives a b). Result: sat. The postulates allow one thing to give existence to another, so they forbid only self-giving, not giving in general.
Scope
This check confirms the Rocq result with an independent tool, and it confirms that each postulate is necessary. Rocq's proof is the primary one. It needs no non-empty-domain assumption, and it proves the result for every kind of thing at once rather than by a solver's search. See rocq-giving.md for the full scope notes.
Premise 3 · Circular creation is impossible
no_circular_creation.smt2
Show the full formalization
; PR-003: No circle of dependence. Independent cross-check in Z3.
; Z3 cannot state "circles of every length" in one formula, so it checks
; circles of length 2, 3, 4 and 5. The general result for every length is
; the Rocq proof. Z3 assumes a non-empty domain; each check names its own
; things, so that assumption does no work. No time appears.
(declare-sort Thing 0)
(declare-fun Gives (Thing Thing) Bool) ; (Gives y x): y gives existence to x
(declare-fun Through (Thing Thing) Bool) ; (Through x y): x has its existence through y
(define-fun MP001 () Bool ; what lacks a thing cannot give it
(forall ((x Thing) (y Thing)) (=> (Gives y x) (not (Through y x)))))
(define-fun MP002 () Bool ; the receiver has its existence through the giver
(forall ((x Thing) (y Thing)) (=> (Gives y x) (Through x y))))
(define-fun MP003 () Bool ; existence through is inherited
(forall ((x Thing) (y Thing) (z Thing))
(=> (and (Through x y) (Through y z)) (Through x z))))
(declare-const a Thing)
(declare-const b Thing)
(declare-const c Thing)
(declare-const d Thing)
(declare-const e Thing)
; Circles: a depends on b, b on c, ..., last on a.
(define-fun circle2 () Bool (and (Gives b a) (Gives a b)))
(define-fun circle3 () Bool (and (Gives b a) (Gives c b) (Gives a c)))
(define-fun circle4 () Bool (and (Gives b a) (Gives c b) (Gives d c) (Gives a d)))
(define-fun circle5 () Bool (and (Gives b a) (Gives c b) (Gives d c) (Gives e d) (Gives a e)))
(echo "check 1: MP-001..003 + circle of 2 (expect unsat)")
(push) (assert MP001) (assert MP002) (assert MP003) (assert circle2) (check-sat) (pop)
(echo "check 2: MP-001..003 + circle of 3 (expect unsat)")
(push) (assert MP001) (assert MP002) (assert MP003) (assert circle3) (check-sat) (pop)
(echo "check 3: MP-001..003 + circle of 4 (expect unsat)")
(push) (assert MP001) (assert MP002) (assert MP003) (assert circle4) (check-sat) (pop)
(echo "check 4: MP-001..003 + circle of 5 (expect unsat)")
(push) (assert MP001) (assert MP002) (assert MP003) (assert circle5) (check-sat) (pop)
(echo "check 5: circle of 3 without MP-003 (expect sat: MP-003 is needed)")
(push) (assert MP001) (assert MP002) (assert circle3) (check-sat) (pop)
(echo "check 6: circle of 3 without MP-001 (expect sat: MP-001 is needed)")
(push) (assert MP002) (assert MP003) (assert circle3) (check-sat) (pop)
(echo "check 7: circle of 3 without MP-002 (expect sat: MP-002 is needed)")
(push) (assert MP001) (assert MP003) (assert circle3) (check-sat) (pop)
(echo "check 8: MP-001..003 + straight chain c gives b gives a (expect sat: postulates allow chains)")
(push) (assert MP001) (assert MP002) (assert MP003)
(assert (and (Gives b a) (Gives c b) (distinct a b c))) (check-sat) (pop)
(declare-sort Thing 0)
(declare-fun Gives (Thing Thing) Bool)
(declare-fun Through (Thing Thing) Bool)English: some kind of things, together with two relations:
(Gives y x): y gives existence to x;(Through x y): x has its existence through y.
(define-fun MP001 () Bool
(forall ((x Thing) (y Thing)) (=> (Gives y x) (not (Through y x)))))English (MP-001): whatever gives existence to x does not have its own existence through x.
(define-fun MP002 () Bool
(forall ((x Thing) (y Thing)) (=> (Gives y x) (Through x y))))English (MP-002): whatever is given existence by y has its existence through y.
(define-fun MP003 () Bool
(forall ((x Thing) (y Thing) (z Thing))
(=> (and (Through x y) (Through y z)) (Through x z))))English (MP-003): if x has its existence through y, and y through z, then x has its existence through z.
(declare-const a Thing) ... (declare-const e Thing)
(define-fun circle2 () Bool (and (Gives b a) (Gives a b)))
(define-fun circle3 () Bool (and (Gives b a) (Gives c b) (Gives a c)))
(define-fun circle4 () Bool (and (Gives b a) (Gives c b) (Gives d c) (Gives a d)))
(define-fun circle5 () Bool (and (Gives b a) (Gives c b) (Gives d c) (Gives e d) (Gives a e)))English: five named things, a to e, and four circles:
- the circle of 2: a depends on b, and b depends on a;
- the circle of 3: a on b, b on c, and c on a;
- the circles of 4 and 5 follow the same pattern.
Each circle is only a named statement; it is not asserted until a check asserts it.
| Check | Asserted | English | Result |
|---|---|---|---|
| 1 | MP-001, MP-002, MP-003, circle of 2 | all postulates, and a circle of 2 | unsat |
| 2 | MP-001, MP-002, MP-003, circle of 3 | all postulates, and a circle of 3 | unsat |
| 3 | MP-001, MP-002, MP-003, circle of 4 | all postulates, and a circle of 4 | unsat |
| 4 | MP-001, MP-002, MP-003, circle of 5 | all postulates, and a circle of 5 | unsat |
| 5 | MP-001, MP-002, circle of 3 | without MP-003 a circle is possible, so MP-003 is needed | sat |
| 6 | MP-002, MP-003, circle of 3 | without MP-001 a circle is possible, so MP-001 is needed | sat |
| 7 | MP-001, MP-003, circle of 3 | without MP-002 a circle is possible, so MP-002 is needed | sat |
| 8 | all three postulates, plus c gives b and b gives a, with a, b, c distinct | the postulates allow ordinary chains | sat |
Scope
This check confirms the Rocq result for circles of up to five things, with an independent tool. It also confirms that each of the three postulates is necessary.
The circle of 2 is already ruled out by MP-001 and MP-002 alone. MP-003 is needed from length 3 onward.
The Rocq proof is the primary one, because it covers every length. See rocq-giving.md for the full scope notes.
Premise 4 · No regress in the giving of existence
no_regress_of_giving.smt2
Show the full formalization
; PR-004: no regress in the giving of existence. Independent cross-check in Z3.
; Z3 assumes a non-empty domain; each check names its own things, so that
; assumption does no work. No time appears.
(declare-sort Thing 0)
(declare-fun Gives (Thing Thing) Bool) ; (Gives y x): y gives existence to x
(declare-fun Proximate (Thing Thing) Bool) ; (Proximate y x): y is a proximate cause of x
(declare-fun Exists (Thing) Bool) ; (Exists x): x actually exists
; x has existence of itself: x exists and nothing gives existence to x.
(define-fun OfItself ((x Thing)) Bool
(and (Exists x) (not (exists ((z Thing)) (Gives z x)))))
; OP-001: only what has existence of itself gives existence.
(define-fun OP001 () Bool
(forall ((x Thing) (y Thing)) (=> (Gives y x) (OfItself y))))
(declare-const t Thing)
(declare-const a Thing)
(declare-const b Thing)
(declare-const c Thing)
(echo "check 1: OP-001 + two-step giving (c gives b, b gives a) (expect unsat)")
(push) (assert OP001) (assert (Gives b a)) (assert (Gives c b)) (check-sat) (pop)
(echo "check 2: two-step giving without OP-001 (expect sat: OP-001 is needed)")
(push) (assert (Gives b a)) (assert (Gives c b)) (check-sat) (pop)
(echo "check 3: OP-001 + base t gives existence to a, b, c; proximate chain c -> b -> a; all exist (expect sat)")
(push) (assert OP001)
(assert (distinct t a b c))
(assert (and (Gives t a) (Gives t b) (Gives t c)))
(assert (and (Proximate c b) (Proximate b a)))
(assert (and (Exists t) (Exists a) (Exists b) (Exists c)))
(check-sat) (pop)
(declare-sort Thing 0)
(declare-fun Gives (Thing Thing) Bool)
(declare-fun Proximate (Thing Thing) Bool)
(declare-fun Exists (Thing) Bool)English: some kind of things, together with:
(Gives y x): y gives existence to x;(Proximate y x): y is a proximate cause of x;(Exists x): x exists.
(define-fun OfItself ((x Thing)) Bool
(and (Exists x) (not (exists ((z Thing)) (Gives z x)))))English: x has existence of itself when x exists and nothing gives existence to x.
(define-fun OP001 () Bool
(forall ((x Thing) (y Thing)) (=> (Gives y x) (OfItself y))))English (OP-001): only what has existence of itself gives existence.
(declare-const t Thing) (declare-const a Thing) (declare-const b Thing) (declare-const c Thing)English: four named things, t, a, b and c.
| Check | Asserted | English | Result |
|---|---|---|---|
| 1 | OP-001, (Gives b a), (Gives c b) | with OP-001, a two-step chain of existence-giving is impossible | unsat |
| 2 | (Gives b a), (Gives c b) | without OP-001, a two-step chain is possible, so OP-001 is needed | sat |
| 3 | OP-001; t gives existence to a, b and c; c is a proximate cause of b and b of a; all four exist; all distinct | the principle allows dependent things to exist and act as proximate causes, with t giving existence | sat |
Scope
This check confirms the Rocq result with an independent tool:
- OP-001 forbids chains of existence-giving;
- OP-001 is needed for that;
- OP-001 is consistent with dependent things existing and acting as proximate causes.
Chains of any length follow from check 1: every chain longer than one contains a two-step chain. The Rocq proof covers this generally. See rocq-existence-giving.md.
Premise 4, illustration · The recursion model
recursion_worlds.smt2
Show the full formalization
; PR-004: independent Z3 check of the recursion model (World A / World B).
; It illustrates why a chain of proximate links cannot settle existence:
; without a base, the links fix nothing; with a base, they fix everything.
; It uses finite windows of the chain; the Rocq file covers the infinite case.
; No time appears.
; ---------- Part 1: existence. u0 depends on u1, u1 on u2, ..., u9 on u10.
; Dependence: each member exists exactly when the one it depends on exists.
(declare-const u0 Bool) (declare-const u1 Bool) (declare-const u2 Bool)
(declare-const u3 Bool) (declare-const u4 Bool) (declare-const u5 Bool)
(declare-const u6 Bool) (declare-const u7 Bool) (declare-const u8 Bool)
(declare-const u9 Bool) (declare-const u10 Bool)
(define-fun dependence () Bool
(and (= u0 u1) (= u1 u2) (= u2 u3) (= u3 u4) (= u4 u5)
(= u5 u6) (= u6 u7) (= u7 u8) (= u8 u9) (= u9 u10)))
(define-fun all_exist () Bool (and u0 u1 u2 u3 u4 u5 u6 u7 u8 u9 u10))
(define-fun none_exist () Bool
(not (or u0 u1 u2 u3 u4 u5 u6 u7 u8 u9 u10)))
(echo "check 1: no base, World A (all exist) respects dependence (expect sat)")
(push) (assert dependence) (assert all_exist) (check-sat) (pop)
(echo "check 2: no base, World B (none exist) respects dependence (expect sat)")
(push) (assert dependence) (assert none_exist) (check-sat) (pop)
(echo "check 3: with base u10 existing, World B is impossible (expect unsat)")
(push) (assert dependence) (assert u10) (assert (not u0)) (check-sat) (pop)
; ---------- Part 2: the Fibonacci recursion. f(n) = f(n-1) + f(n-2) for
; n = 2..12. "No base" means f0 and f1 are not fixed.
(declare-const f0 Int) (declare-const f1 Int) (declare-const f2 Int)
(declare-const f3 Int) (declare-const f4 Int) (declare-const f5 Int)
(declare-const f6 Int) (declare-const f7 Int) (declare-const f8 Int)
(declare-const f9 Int) (declare-const f10 Int) (declare-const f11 Int)
(declare-const f12 Int)
(define-fun recurrence () Bool
(and (= f2 (+ f1 f0)) (= f3 (+ f2 f1)) (= f4 (+ f3 f2)) (= f5 (+ f4 f3))
(= f6 (+ f5 f4)) (= f7 (+ f6 f5)) (= f8 (+ f7 f6)) (= f9 (+ f8 f7))
(= f10 (+ f9 f8)) (= f11 (+ f10 f9)) (= f12 (+ f11 f10))))
(echo "check 4: no base, the recurrence allows f12 = 0 (expect sat)")
(push) (assert recurrence) (assert (= f12 0)) (check-sat) (pop)
(echo "check 5: no base, the recurrence also allows f12 = 144 (expect sat)")
(push) (assert recurrence) (assert (= f12 144)) (check-sat) (pop)
(echo "check 6: with base f0 = 0, f1 = 1, f12 can only be 144 (expect unsat)")
(push) (assert recurrence) (assert (= f0 0)) (assert (= f1 1))
(assert (not (= f12 144))) (check-sat) (pop)
Part 1: existence
(declare-const u0 Bool) ... (declare-const u10 Bool)English: eleven members of a chain, u0 to u10. Each one either exists (true) or does not (false).
(define-fun dependence () Bool
(and (= u0 u1) (= u1 u2) ... (= u9 u10)))English: u0 depends on u1, u1 on u2, and so on. Each member exists exactly when the member it depends on exists.
(define-fun all_exist () Bool (and u0 u1 ... u10))
(define-fun none_exist () Bool (not (or u0 u1 ... u10)))English:
- World A: every member exists.
- World B: no member exists.
| Check | Asserted | English | Result |
|---|---|---|---|
| 1 | dependence, all_exist | with no base, World A respects the dependence | sat |
| 2 | dependence, none_exist | with no base, World B respects the dependence too | sat |
| 3 | dependence, u10 exists, u0 does not | once u10 is a base that exists, World B is impossible | unsat |
Part 2: the Fibonacci recursion
(declare-const f0 Int) ... (declare-const f12 Int)
(define-fun recurrence () Bool
(and (= f2 (+ f1 f0)) (= f3 (+ f2 f1)) ... (= f12 (+ f11 f10))))English: thirteen values f0 to f12. Each value from f2 onward is the sum of the two before it. With "no base", f0 and f1 are not fixed.
| Check | Asserted | English | Result |
|---|---|---|---|
| 4 | recurrence, f12 = 0 | with no base, the recursion allows f12 to be 0 | sat |
| 5 | recurrence, f12 = 144 | with no base, it equally allows f12 to be 144 | sat |
| 6 | recurrence, f0 = 0, f1 = 1, f12 ≠ 144 | with the base f0 = 0 and f1 = 1, f12 can only be 144 | unsat |
Scope
- Without a base, the dependence relations are satisfied, but they fix no result:
- existence and non-existence both fit (Part 1);
- any Fibonacci value fits (Part 2).
- With a base, the result is fixed.
This is the World A / World B analysis, confirmed by an independent tool. It supports OP-001's point: a chain of proximate causes passes existence along but cannot originate it. Premise 4 itself is proved in rocq-existence-giving.md.
The conclusion
kalima_conclusion.smt2
Show the full formalization
; Dalil al-kalima, the conclusion: independent cross-check in Z3.
; Z3 assumes a non-empty domain. Here the universe u is named explicitly,
; so that assumption does no work. No time appears.
(declare-sort Thing 0)
(declare-fun Gives (Thing Thing) Bool) ; (Gives y x): y gives existence to x
(declare-fun Through (Thing Thing) Bool) ; (Through x y): x has its existence through y
(declare-fun Exists (Thing) Bool) ; (Exists x): x exists
(declare-const u Thing) ; the universe
(define-fun MP001 () Bool (forall ((x Thing) (y Thing)) (=> (Gives y x) (not (Through y x)))))
(define-fun MP002 () Bool (forall ((x Thing) (y Thing)) (=> (Gives y x) (Through x y))))
(define-fun MP003 () Bool (forall ((x Thing) (y Thing) (z Thing))
(=> (and (Through x y) (Through y z)) (Through x z))))
(define-fun Necessary ((x Thing)) Bool
(and (Exists x) (not (exists ((z Thing)) (Gives z x)))))
(define-fun OP001 () Bool (forall ((x Thing) (y Thing)) (=> (Gives y x) (Necessary y))))
(define-fun UniverseIsCaused () Bool (exists ((y Thing)) (Gives y u))) ; the antecedent: the universe is caused
; The conclusion: something necessary gives existence to the universe.
(define-fun Conclusion () Bool (exists ((b Thing)) (and (Gives b u) (Necessary b))))
(echo "check 1: premises + universe caused + conclusion denied (expect unsat)")
(push) (assert MP001) (assert MP002) (assert MP003) (assert OP001) (assert UniverseIsCaused)
(assert (not Conclusion)) (check-sat) (pop)
(echo "check 2: premises + universe caused together (expect sat: consistent)")
(push) (assert MP001) (assert MP002) (assert MP003) (assert OP001) (assert UniverseIsCaused) (check-sat) (pop)
(echo "check 3: without OP-001, conclusion denied (expect sat: OP-001 is needed)")
(push) (assert MP001) (assert MP002) (assert MP003) (assert UniverseIsCaused)
(assert (not Conclusion)) (check-sat) (pop)
(echo "check 4: universe not assumed caused, conclusion denied (expect sat: the conclusion is conditional)")
(push) (assert MP001) (assert MP002) (assert MP003) (assert OP001)
(assert (not Conclusion)) (check-sat) (pop)
(declare-sort Thing 0)
(declare-fun Gives (Thing Thing) Bool)
(declare-fun Through (Thing Thing) Bool)
(declare-fun Exists (Thing) Bool)
(declare-const u Thing)English: some kind of things, together with:
- "y gives existence to x";
- "x has its existence through y";
- "x exists";
- a named thing
u, the universe.
(define-fun MP001 () Bool (forall ((x Thing) (y Thing)) (=> (Gives y x) (not (Through y x)))))
(define-fun MP002 () Bool (forall ((x Thing) (y Thing)) (=> (Gives y x) (Through x y))))
(define-fun MP003 () Bool (forall ((x Thing) (y Thing) (z Thing))
(=> (and (Through x y) (Through y z)) (Through x z))))English:
- MP-001: whatever gives existence to x does not have its existence through x.
- MP-002: whatever is given existence by y has its existence through y.
- MP-003: existence-through is inherited along a chain.
(define-fun Necessary ((x Thing)) Bool
(and (Exists x) (not (exists ((z Thing)) (Gives z x)))))English: x is necessary when x exists and nothing gives it existence.
(define-fun OP001 () Bool (forall ((x Thing) (y Thing)) (=> (Gives y x) (Necessary y))))English (OP-001): only what has existence of itself gives existence.
(define-fun UniverseIsCaused () Bool (exists ((y Thing)) (Gives y u)))English (the antecedent): something gives existence to the universe. The universe's existence requires a cause.
(define-fun Conclusion () Bool (exists ((b Thing)) (and (Gives b u) (Necessary b))))English (the conclusion): something necessary gives existence to the universe.
| Check | Asserted | English | Result |
|---|---|---|---|
| 1 | MP-001, MP-002, MP-003, OP-001, the universe is caused, and not Conclusion | given the "if", the conclusion cannot be false | unsat |
| 2 | MP-001, MP-002, MP-003, OP-001, the universe is caused | the premises and the antecedent can hold together | sat |
| 3 | MP-001, MP-002, MP-003, the universe is caused, and not Conclusion | without OP-001, the conclusion can fail, so OP-001 is needed | sat |
| 4 | MP-001, MP-002, MP-003, OP-001, and not Conclusion | without the "if", the conclusion can fail, so the conclusion is conditional | sat |
Scope
This check confirms, with an independent tool, that:
- the conclusion follows from the premises, given the "if";
- the premises are consistent;
- OP-001 is indispensable, and the conclusion is conditional.
A separate run found that OP-001 and the antecedent alone already give unsat against the denied conclusion. That is the basis of the disclosure in rocq-conclusion.md. The four-case structure of the argument is shown in Rocq, not here.
The universe is caused · the “if” answered
universe_is_caused.smt2
Show the full formalization
; PR-011: the universe is caused. Independent cross-check in Z3, for both
; definitions of the universe. No time appears.
(declare-sort Thing 0)
(declare-fun Ex (Thing) Bool) ; x exists
(declare-fun Ess (Thing) Bool) ; x's existence is from its nature
(declare-fun Gives (Thing Thing) Bool) ; (Gives y x): y gives existence to x
(declare-fun Part (Thing Thing) Bool) ; (Part p u): p is a part of u (physical or metaphysical)
(declare-const U Thing) ; the universe
(define-fun Poss ((x Thing)) Bool (and (Ex x) (not (Ess x))))
(define-fun TA ((x Thing)) Bool (exists ((y Thing)) (Gives y x)))
(define-fun InU ((x Thing)) Bool (or (= x U) (Part x U)))
(define-fun MP008 () Bool (forall ((x Thing)) (=> (and (Ex x) (not (TA x))) (Ess x))))
(define-fun MP010 () Bool (forall ((A Thing)) (=> (and (exists ((p Thing)) (Part p A))
(forall ((p Thing)) (=> (Part p A) (not (Ess p)))))
(not (Ess A)))))
(define-fun OP006 () Bool (exists ((x Thing)) (and (InU x) (Poss x)))) ; broader definition
(define-fun OP007 () Bool (and (Ex U) (exists ((p Thing)) (Part p U)))) ; our definition
(define-fun Narrow () Bool (forall ((p Thing)) (=> (Part p U) (not (Ess p))))) ; our definition of the universe
(echo "check 1: broader definition: MP-008 + OP-006 + nothing in the universe caused (expect unsat)")
(push) (assert MP008) (assert OP006) (assert (not (exists ((x Thing)) (and (InU x) (Poss x) (TA x))))) (check-sat) (pop)
(echo "check 2: our definition: MP-008 + MP-010 + definition + OP-007 + universe uncaused (expect unsat)")
(push) (assert MP008) (assert MP010) (assert Narrow) (assert OP007) (assert (not (TA U))) (check-sat) (pop)
(echo "check 3: broader definition without OP-006 (expect sat: OP-006 is needed)")
(push) (assert MP008) (assert (not (exists ((x Thing)) (and (InU x) (Poss x) (TA x))))) (check-sat) (pop)
(echo "check 4: our definition without OP-007 (expect sat: OP-007 is needed)")
(push) (assert MP008) (assert MP010) (assert Narrow) (assert (not (TA U))) (check-sat) (pop)
(echo "check 5: without MP-008, both definitions (expect sat: MP-008 is needed)")
(push) (assert MP010) (assert Narrow) (assert OP007) (assert OP006) (assert (not (TA U)))
(assert (not (exists ((x Thing)) (and (InU x) (Poss x) (TA x))))) (check-sat) (pop)
(echo "check 6: broader definition, case 3 (a necessary part and a possible part) is consistent (expect sat)")
(push) (assert MP008) (assert OP006)
(assert (exists ((n Thing) (p Thing)) (and (Part n U) (Part p U) (Ex n) (Ess n) (Poss p)))) (check-sat) (pop)
universe_is_caused.smt2
(declare-sort Thing 0)English: some kind of things. Nothing is assumed about them, not even that any exist.
(declare-fun Ex (Thing) Bool)English: "x exists".
(declare-fun Ess (Thing) Bool)English: "x's existence is from its own nature".
(declare-fun Gives (Thing Thing) Bool)English: "y gives existence to x".
(declare-fun Part (Thing Thing) Bool)English: "p is a part of u", physical or metaphysical.
(declare-const U Thing)English: the universe.
(define-fun Poss ((x Thing)) Bool (and (Ex x) (not (Ess x))))English: x is possible in itself: it exists, and its existence is not from its own nature.
(define-fun TA ((x Thing)) Bool (exists ((y Thing)) (Gives y x)))English: x has its existence through another: something gives it existence.
(define-fun InU ((x Thing)) Bool (or (= x U) (Part x U)))English: x is in the universe: it is the universe itself, or one of its parts.
(define-fun MP008 () Bool (forall ((x Thing)) (=> (and (Ex x) (not (TA x))) (Ess x))))English: MP-008: if something exists and nothing gives it existence, its existence is from its own nature. There is no existence "from nowhere".
(define-fun MP010 () Bool (forall ((A Thing)) (=> (and (exists ((p Thing)) (Part p A))
(forall ((p Thing)) (=> (Part p A) (not (Ess p)))))
(not (Ess A)))))English: MP-010: a collection that has members, none of whose existence is from their own nature, does not have its existence from its own nature either.
(define-fun OP006 () Bool (exists ((x Thing)) (and (InU x) (Poss x))))English: OP-006: at the very least, the universe is not wholly necessary. Something in it is possible. This is used for the broader definition.
(define-fun OP007 () Bool (and (Ex U) (exists ((p Thing)) (Part p U))))English: OP-007: the universe exists and has parts. This is used for our definition.
(define-fun Narrow () Bool (forall ((p Thing)) (=> (Part p U) (not (Ess p)))))English: our definition of the universe: none of its parts has its existence from its own nature. The universe does not overlap with the necessary.
Scope
Z3 independently confirms PR-011 under both definitions. It also confirms which observation each definition needs, and that case 3 arises only under the broader definition.
The conclusion without the “if”
kalima_unconditional.smt2
Show the full formalization
; Dalil al-kalima, unconditional: independent cross-check in Z3.
; The kalima premises (MP-001 to MP-003, OP-001) with PR-011's premises
; (MP-008, and OP-006 or OP-007 with MP-010) give a necessary first cause.
; No time appears.
(declare-sort Thing 0)
(declare-fun Ex (Thing) Bool)
(declare-fun Ess (Thing) Bool)
(declare-fun Gives (Thing Thing) Bool)
(declare-fun Through (Thing Thing) Bool)
(declare-fun Part (Thing Thing) Bool)
(declare-const U Thing)
(define-fun Poss ((x Thing)) Bool (and (Ex x) (not (Ess x))))
(define-fun TA ((x Thing)) Bool (exists ((y Thing)) (Gives y x)))
(define-fun OfItself ((x Thing)) Bool (and (Ex x) (not (TA x))))
(define-fun InU ((x Thing)) Bool (or (= x U) (Part x U)))
(define-fun Independent ((x Thing)) Bool (forall ((y Thing)) (not (Gives y x))))
(define-fun MP001 () Bool (forall ((x Thing) (y Thing)) (=> (Gives y x) (not (Through y x)))))
(define-fun MP002 () Bool (forall ((x Thing) (y Thing)) (=> (Gives y x) (Through x y))))
(define-fun MP003 () Bool (forall ((x Thing) (y Thing) (z Thing)) (=> (and (Through x y) (Through y z)) (Through x z))))
(define-fun OP001 () Bool (forall ((x Thing) (y Thing)) (=> (Gives y x) (OfItself y))))
(define-fun MP008 () Bool (forall ((x Thing)) (=> (and (Ex x) (not (TA x))) (Ess x))))
(define-fun MP010 () Bool (forall ((A Thing)) (=> (and (exists ((p Thing)) (Part p A))
(forall ((p Thing)) (=> (Part p A) (not (Ess p)))))
(not (Ess A)))))
(define-fun OP006 () Bool (exists ((x Thing)) (and (InU x) (Poss x))))
(define-fun OP007 () Bool (and (Ex U) (exists ((p Thing)) (Part p U))))
(define-fun Narrow () Bool (forall ((p Thing)) (=> (Part p U) (not (Ess p)))))
(echo "check 1: broader definition: kalima + MP-008 + OP-006, no necessary first cause of anything in the universe (expect unsat)")
(push) (assert MP001) (assert MP002) (assert MP003) (assert OP001) (assert MP008) (assert OP006)
(assert (not (exists ((x Thing) (b Thing)) (and (InU x) (Gives b x) (Ex b) (Ess b) (Independent b))))) (check-sat) (pop)
(echo "check 2: our definition: kalima + MP-008 + MP-010 + definition + OP-007, no necessary first cause of the universe (expect unsat)")
(push) (assert MP001) (assert MP002) (assert MP003) (assert OP001) (assert MP008) (assert MP010) (assert Narrow) (assert OP007)
(assert (not (exists ((b Thing)) (and (Gives b U) (Ex b) (Ess b) (Independent b))))) (check-sat) (pop)
(echo "check 3: all premises of both forms together (expect sat: consistent)")
(push) (assert MP001) (assert MP002) (assert MP003) (assert OP001) (assert MP008) (assert MP010) (assert Narrow) (assert OP007) (assert OP006)
(check-sat) (pop)
kalima_unconditional.smt2
(declare-sort Thing 0)English: some kind of things. Nothing is assumed about them, not even that any exist.
(declare-fun Ex (Thing) Bool)English: "x exists".
(declare-fun Ess (Thing) Bool)English: "x's existence is from its own nature".
(declare-fun Gives (Thing Thing) Bool)English: "y gives existence to x".
(declare-fun Through (Thing Thing) Bool)English: "x has its existence through y".
(declare-fun Part (Thing Thing) Bool)English: "p is a part of u", physical or metaphysical.
(declare-const U Thing)English: the universe.
(define-fun Poss ((x Thing)) Bool (and (Ex x) (not (Ess x))))English: x is possible in itself: it exists, and its existence is not from its own nature.
(define-fun TA ((x Thing)) Bool (exists ((y Thing)) (Gives y x)))English: x has its existence through another: something gives it existence.
(define-fun OfItself ((x Thing)) Bool (and (Ex x) (not (TA x))))English: x has existence of itself: it exists, and nothing gives it existence.
(define-fun InU ((x Thing)) Bool (or (= x U) (Part x U)))English: x is in the universe: it is the universe itself, or one of its parts.
(define-fun Independent ((x Thing)) Bool (forall ((y Thing)) (not (Gives y x))))English: x depends on nothing: nothing gives it existence.
(define-fun MP001 () Bool (forall ((x Thing) (y Thing)) (=> (Gives y x) (not (Through y x)))))English: MP-001: whatever gives existence to x does not have its own existence through x.
(define-fun MP002 () Bool (forall ((x Thing) (y Thing)) (=> (Gives y x) (Through x y))))English: MP-002: whatever is given existence by y has its existence through y.
(define-fun MP003 () Bool (forall ((x Thing) (y Thing) (z Thing)) (=> (and (Through x y) (Through y z)) (Through x z))))English: MP-003: existence-through is inherited along a chain.
(define-fun OP001 () Bool (forall ((x Thing) (y Thing)) (=> (Gives y x) (OfItself y))))English: OP-001: only what has existence of itself gives existence.
(define-fun MP008 () Bool (forall ((x Thing)) (=> (and (Ex x) (not (TA x))) (Ess x))))English: MP-008: if something exists and nothing gives it existence, its existence is from its own nature. There is no existence "from nowhere".
(define-fun MP010 () Bool (forall ((A Thing)) (=> (and (exists ((p Thing)) (Part p A))
(forall ((p Thing)) (=> (Part p A) (not (Ess p)))))
(not (Ess A)))))English: MP-010: a collection that has members, none of whose existence is from their own nature, does not have its existence from its own nature either.
(define-fun OP006 () Bool (exists ((x Thing)) (and (InU x) (Poss x))))English: OP-006: at the very least, the universe is not wholly necessary. Something in it is possible. This is used for the broader definition.
(define-fun OP007 () Bool (and (Ex U) (exists ((p Thing)) (Part p U))))English: OP-007: the universe exists and has parts. This is used for our definition.
(define-fun Narrow () Bool (forall ((p Thing)) (=> (Part p U) (not (Ess p)))))English: our definition of the universe: none of its parts has its existence from its own nature. The universe does not overlap with the necessary.
Scope
Z3 independently confirms the unconditional kalima conclusion in both forms, and confirms that its premises are consistent.
Run it yourself
Z3 4.13.3 · run a checkLoad any input above into this editor, or paste your own, and run it on this server's Z3 4.13.3 in an isolated, network-disabled worker. Runs are limited to 60 seconds.