Dalīl al-imkān · 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 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).
Every step
Where each step is proved| Step | Claim | In Z3 | Proof of the step |
|---|---|---|---|
| 1 | The division | Checked together with the other steps in imkan.smt2 | Proved every step checked proved in Rocq |
| 2 | The necessary cannot fail | Not needed for the conclusion | Proved every step checked proved in Rocq |
| 3 | The possible needs a cause | Checked together with the other steps in imkan.smt2 | Proved every step checked proved in Rocq |
| 4 | Nothing causes itself | Confirmed unsat: the opposite is impossible · its own Z3 check | Proved every step checked proved in Rocq |
| 5 | The aggregate of all possibles | Checked together with the other steps in imkan.smt2 | Proved every step checked proved in Rocq |
| 6 | The aggregate is possible | Checked together with the other steps in imkan.smt2 | Proved every step checked proved in Rocq |
| 7 | Its cause is not a member | Checked together with the other steps in imkan.smt2 | Proved every step checked proved in Rocq |
| 8 | Nothing possible causes itself | Checked together with the other steps in imkan.smt2 | Proved every step checked proved in Rocq |
| 9 | The cause is outside the aggregate | Checked together with the other steps in imkan.smt2 | Proved every step checked proved in Rocq |
| 10 | The division, applied | Checked together with the other steps in imkan.smt2 | Proved every step checked proved in Rocq |
| 11 | That cause is necessary | Checked together with the other steps in imkan.smt2 | Proved every step checked proved in Rocq |
| 12 | A Necessary Existent exists | Confirmed unsat: the opposite is impossible · Z3 confirms the conclusion | Proved every step checked proved in Rocq |
Every step is proved in Rocq, from the approved postulates. Z3 independently confirms that the steps yield the conclusion. Where it does not check a step on its own, the table links to the Rocq proof. Step 2 is part of the argument but is not needed for the conclusion.
The checks
Formal statements and their English equivalentsProofs (a) and (b)
imkan.smt2
Show the full formalization
; Dalil al-imkan: independent cross-check in Z3 of proof (a) (the aggregate
; route) and proof (b) (the short route through OP-001).
; "y gives existence to x, directly or through intermediaries" needs induction,
; which Z3 cannot express; it is represented by a relation UG that contains
; giving and is transitive, and the PROVED result of PR-003 (no circle of
; giving) is supplied as "nothing UG-gives to itself". This is sound for
; unsat: any real counterexample extends to one here (take UG = the real
; chains of giving). Z3 assumes non-empty domains; SP-001 supplies existence
; explicitly. 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 Mem (Thing Thing) Bool) ; (Mem p A): p is a member of collection A
(declare-fun UG (Thing Thing) Bool) ; y gives existence to x, directly or through intermediaries
(define-fun Nec ((x Thing)) Bool (and (Ex x) (Ess x)))
(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 Agg ((A Thing)) Bool
(and (forall ((p Thing)) (=> (not (= p A)) (= (Mem p A) (Poss p)))) (not (Mem A A))))
(define-fun UGdef () Bool (and (forall ((y Thing) (x Thing)) (=> (Gives y x) (UG y x)))
(forall ((x Thing) (y Thing) (z Thing)) (=> (and (UG x y) (UG y z)) (UG x z)))))
(define-fun PR003 () Bool (forall ((x Thing)) (not (UG x x)))) ; proved: no circle of giving
(define-fun MP008 () Bool (forall ((x Thing)) (=> (and (Ex x) (not (TA x))) (Ess x))))
(define-fun MP009 () Bool (=> (exists ((p Thing)) (Poss p)) (exists ((A Thing)) (and (Agg A) (Ex A)))))
(define-fun MP010 () Bool (forall ((A Thing)) (=> (and (exists ((p Thing)) (Mem p A))
(forall ((p Thing)) (=> (Mem p A) (not (Ess p)))))
(not (Ess A)))))
(define-fun MP011 () Bool (forall ((c Thing) (A Thing) (p Thing)) (=> (and (Gives c A) (Mem p A)) (UG c p))))
(define-fun MP012 () Bool (forall ((y Thing) (x Thing)) (=> (Gives y x) (Ex y))))
(define-fun OP001 () Bool (forall ((x Thing) (y Thing)) (=> (Gives y x) (and (Ex y) (not (TA y))))))
(define-fun SP001 () Bool (exists ((x Thing)) (Ex x)))
(define-fun Conclusion () Bool (exists ((n Thing)) (Nec n)))
(echo "check 1: proof (a): premises + SP-001 + conclusion denied (expect unsat)")
(push) (assert UGdef) (assert PR003) (assert MP008) (assert MP009) (assert MP010) (assert MP011) (assert MP012)
(assert SP001) (assert (not Conclusion)) (check-sat) (pop)
(echo "check 2: proof (a): premises + SP-001 together (expect sat: consistent)")
(push) (assert UGdef) (assert PR003) (assert MP008) (assert MP009) (assert MP010) (assert MP011) (assert MP012)
(assert SP001) (check-sat) (pop)
(echo "check 3: proof (a) without SP-001, conclusion denied (expect sat: SP-001 is needed)")
(push) (assert UGdef) (assert PR003) (assert MP008) (assert MP009) (assert MP010) (assert MP011) (assert MP012)
(assert (not Conclusion)) (check-sat) (pop)
(echo "check 4: proof (b): MP-008 + OP-001 + SP-001 + conclusion denied (expect unsat)")
(push) (assert MP008) (assert OP001) (assert SP001) (assert (not Conclusion)) (check-sat) (pop)
(echo "check 5: proof (b) without OP-001, conclusion denied (expect sat: OP-001 is needed)")
(push) (assert MP008) (assert SP001) (assert (not Conclusion)) (check-sat) (pop)
imkan.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 Mem (Thing Thing) Bool)English: "p is a member of the collection A".
(declare-fun UG (Thing Thing) Bool)English: "y gives existence to x, directly or through intermediaries". It is represented by a relation that contains giving and is transitive.
(define-fun Nec ((x Thing)) Bool (and (Ex x) (Ess x)))English: x is necessary in itself: it exists, and its existence is from its own nature.
(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 Agg ((A Thing)) Bool
(and (forall ((p Thing)) (=> (not (= p A)) (= (Mem p A) (Poss p)))) (not (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.
(define-fun UGdef () Bool (and (forall ((y Thing) (x Thing)) (=> (Gives y x) (UG y x)))
(forall ((x Thing) (y Thing) (z Thing)) (=> (and (UG x y) (UG y z)) (UG x z)))))English: the relation "gives, directly or through intermediaries" contains giving and is transitive.
(define-fun PR003 () Bool (forall ((x Thing)) (not (UG x x))))English: proved premise PR-003: nothing gives existence to itself through a chain. There is no circle of giving.
(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 MP009 () Bool (=> (exists ((p Thing)) (Poss p)) (exists ((A Thing)) (and (Agg A) (Ex A)))))English: MP-009: if some possible thing exists, there is an existing aggregate of all the possibles.
(define-fun MP010 () Bool (forall ((A Thing)) (=> (and (exists ((p Thing)) (Mem p A))
(forall ((p Thing)) (=> (Mem 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 MP011 () Bool (forall ((c Thing) (A Thing) (p Thing)) (=> (and (Gives c A) (Mem p A)) (UG c p))))English: MP-011: whatever gives existence to a collection gives existence to each of its members, directly or through intermediaries.
(define-fun MP012 () Bool (forall ((y Thing) (x Thing)) (=> (Gives y x) (Ex y))))English: MP-012: whatever gives existence exists.
(define-fun OP001 () Bool (forall ((x Thing) (y Thing)) (=> (Gives y x) (and (Ex y) (not (TA y))))))English: OP-001: only what has existence of itself gives existence.
(define-fun SP001 () Bool (exists ((x Thing)) (Ex x)))English: SP-001: something exists. This is self-evident.
(define-fun Conclusion () Bool (exists ((n Thing)) (Nec n)))English: the conclusion: a Necessary Existent exists.
Scope
Z3 independently confirms both proofs of dalīl al-imkān, and confirms that their premises are consistent and needed. The Rocq proofs are the primary proofs.
Step 4 · Nothing causes its own existence
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.
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.