Possible bug with Z3: Z3 is not able to prove a theorem in Topology

Question

I am trying to prove with Z3 the theorem in general topology given at

TPTP-Topology

I am translating the code given there using the following Z3-SMT-LIB code

;; File     : TOP001-2 : TPTP v6.0.0. Released v1.0.0.
;; Domain   : Topology
;; Problem  : Topology generated by a basis forms a topological space, part 1

(declare-sort S)
(declare-sort Q)
(declare-sort P)

(declare-fun elemcoll (S Q) Bool)
(declare-fun elemset (P S) Bool)
(declare-fun unionmemb (Q) S)

(declare-fun f1 (Q P) S)

(declare-fun f11 (Q S) P)
(declare-fun basis (S Q) Bool)
(declare-fun Subset (S S) Bool)
(declare-fun topbasis (Q) Q)

;; union of members axiom 1.
(assert (forall ((U P) (Vf Q)) (or (not (elemset U (unionmemb Vf))) 
                                    (elemset U (f1 Vf U) ) )   ))
;; union of members axiom 2.

(assert (forall ((U P) (Vf Q)) (or (not (elemset U (unionmemb Vf))) 
                                   (elemcoll (f1 Vf U) Vf ) )   ))


;; basis for topology, axiom 28

(assert (forall ((X S) (Vf Q)) (or (not (basis X Vf)) (= (unionmemb Vf) X )  )   ))

;; Topology generated by a basis, axiom 40.

(assert (forall ((Vf Q) (U S)) (or (elemcoll U (topbasis Vf))   
                               (elemset (f11 Vf U) U))   ))

;; Set theory, axiom 7.

(assert (forall ((X S) (Y Q)) (or (not (elemcoll X Y)) (Subset X (unionmemb Y) ) )  ))

;; Set theory, axiom 8.
(assert (forall ((X S) (Y S) (U P)) (or (not (Subset X Y)) (not (elemset U X))
                                                                (elemset U Y)     )))

;; Set theory, axiom 9.
(assert (forall ((X S)) (Subset X X )  ))

;; Set theory, axiom 10.
(assert (forall ((X S) (Y S) (Z S)) (or (not (= X Y)) (not (Subset Z X)) (Subset Z Y) )  ))

;; Set theory, axiom 11.
(assert (forall ((X S) (Y S) (Z S)) (or (not (= X Y)) (not (Subset X Z)) (Subset Y Z) )  ))

(check-sat)

(push)
(declare-fun cx () S)
(declare-fun f () Q)
(assert (basis cx f))
(assert (not (elemcoll cx (topbasis f))))   
(check-sat)
(pop)

(push)
(assert (basis cx f))
(assert (elemcoll cx (topbasis f)))  
(check-sat)
(pop)

The corresponding output is

sat
sat
sat

Please run this example online here

The first sat is correct; but the second sat is wrong, it must be unsat. In other words, Z3 is saying that the theorem and its negation are true simultaneously.

Please let me know what happens in this case. Many thanks. All the best.

Answer 1

It is possible that both a formula and the negation of the formula is consistent with respect to a background theory T. In particular, when T is not complete, then there are sentences that are neither consequences of T nor inconsistent with T. In your case the theory T is the set of topology axioms. You can use the command (get-model) to obtain a model that satisfies the axioms and the sentence.