; 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)