SMT backends CVC3 and Z3 prove `\A x: x \in BOOLEAN`

[johnyf]

Using tlapm version 1.4.3, the following theorems are proved:

THEOREM EverythingIsBoolean ==
    \A x:  x \in BOOLEAN
    OBVIOUS

THEOREM
    ASSUME NEW c,
        /\ c # FALSE
        /\ c # TRUE
    PROVE FALSE
    OBVIOUS

in the presence of cvc3 and z3 (invoking those tools with a BY CVC3 or BY Z3 confirms so https://github.com/tlaplus/v2-tlapm/blob/eb830974341821885b1e0c14e81c675543135360/library/TLAPS.tla#L49). These theorems fail to be proved (as expected) when using Zenon or Isabelle (BY Isa)

EXTENDS TLAPS

THEOREM EverythingIsBoolean ==
    \A x:  x \in BOOLEAN
    BY Zenon

THEOREM
    ASSUME NEW c,
        /\ c # FALSE
        /\ c # TRUE
    PROVE FALSE
    BY Zenon

Also the following two theorems are proved:

THEOREM Consequent == \A x:  x = (TRUE => x)
    OBVIOUS

THEOREM ImplIsBoolean == \A x:  ((TRUE => x) \in BOOLEAN)
    OBVIOUS

of which the first one seems unexpected with the liberal interpretation of Boolean operators (Sec. 8.1 on pp. 36--37 of the TLA+2 guide) (for x \notin BOOLEAN it would follow that implication takes a non-Boolean value), and indeed is not proved when using BY Zenon.

[johnyf]

The SMT v2 file that is generated for the claim:

THEOREM EverythingIsBoolean ==
    \A x:  x \in BOOLEAN
    OBVIOUS

is:

;; Proof obligation:
;;\A x : x \in BOOLEAN
(set-logic AUFNIRA)
(declare-sort u 0)
;; Declaration of terms, predicates and strings
(declare-fun a_skcunde_xa () u)
(declare-fun u2bool (u) Bool)
;; Axioms
;; Conclusion
(assert (not (or (= (u2bool a_skcunde_xa) true) 
    (= (u2bool a_skcunde_xa) false))))
;; Main assertions from the proof obligation
(check-sat)

This file can be obtained with tlapm --solver "cp \"\$file\" ../" -v --cleanfp AllBoolean.tla.

Calling z3 -smt2 returns "unsat". From the simple example: https://github.com/tlaplus/v2-tlapm/issues/19#issue-271106565, my understanding is that tlapm gives the negation of each claim to the SMT solver, in order to make sure there are no counter-examples. So the result reported by tlapm matches the output of z3. Assuming that this isn't a bug in Z3, it appears that the generated SMT file does not correspond to what the theorem claims.

TLA+ is an untyped language based on Zermelo-Fraenkel set theory, so not all values are in the set {FALSE, TRUE} (relevant reference: the book "Specifying systems").

[johnyf]

In contrast, trying to prove:

EXTENDS Integers

THEOREM EverythingIsBoolean ==
    \A x:  x \in {1, 2}
    OBVIOUS

fails to prove the claim (which is the correct conclusion, since there are values other than 1 and 2). In this case, the generated SMT file contains:

;; Proof obligation:
;;\A x : x \in {1, 2}
(set-logic AUFNIRA)
(declare-sort u 0)
;; Declaration of terms, predicates and strings
(declare-fun a_skcunde_xa () u)
(declare-fun int2u (Int) u)
;; Axioms
(assert (forall ((X_3 Int) (Y_4 Int)) 
        (=> (= (int2u X_3) (int2u Y_4)) (= X_3 Y_4))))
;; Conclusion
(assert (not (or (= a_skcunde_xa (int2u 1)) 
    (= a_skcunde_xa (int2u 2)))))
;; Main assertions from the proof obligation
(check-sat)
(exit)

Mimicking this SMT encoding for the claim \A x: x \in BOOLEAN that leads to an unsound conclusion, as noted [above](), I created by hand the following SMT file, which leads to the correct conclusion (z3 concludes "sat"):

;; Created by hand

(set-logic AUFNIRA)
(declare-sort u 0)
;; Declaration of terms, predicates and strings
(declare-fun a_skcunde_xa () u)
(declare-fun u2bool (u) Bool)
(declare-fun int2u (Int) u)
(declare-fun bool2u (Bool) u)
;; Axioms
(assert (forall ((X_3 Bool) (Y_4 Bool))
        (=> (= (bool2u X_3) (bool2u Y_4)) (= X_3 Y_4))))
;; Conclusion
(assert (not (or (= a_skcunde_xa (bool2u true))
    (= a_skcunde_xa (bool2u false) ))))
;; Main assertions from the proof obligation
(check-sat)
(exit)