title: A three-valued boolean logic with Z3 solver
body: <p>I have been trying to define a three-valued propositional logic and reason about it using Z3 SMT Solver.
  To be more precise, I have define a sort Boolean with three values: TRUE, FALSE and NULL with some assertions.</p>
  <pre><code>(declare-sort Boolean 0)       ;I declare a sort Boolean
  (declare-const TRUE Boolean)   ;I define three constants
  (declare-const TRUE Boolean)
  (declare-const FALSE Boolean)
  (declare-const NULL Boolean)
  
  (assert (distinct TRUE FALSE)) ;I define the meaning of these constants
  (assert (distinct TRUE NULL))
  (assert (distinct FALSE NULL))
  
  (assert (forall ((b Boolean))
      (or (= b TRUE)
          (= b FALSE)
          (= b NULL))))
  </code></pre>
  <p>Next, let's say I am defining an the semantics of <code>&gt;=</code> operator of integer under this logic, assuming that an integer can be NULL.</p>
  <pre><code>(declare-const nullInt Int)
  (declare-fun &gt;=_B (Int Int) Boolean)
  
  (assert (forall ((i1 Int) (i2 Int))
      (= (= TRUE (&gt;=_B i1 i2))
         (and (distinct i1 nullInt)
              (distinct i2 nullInt)
              (&gt;= i1 i2)))))
  
  (assert (forall ((i1 Int) (i2 Int))
      (= (= FALSE (&gt;=_B i1 i2))
         (and (distinct i1 nullInt)
              (distinct i2 nullInt)
              (not (&gt;= i1 i2))))))
  
  (assert (forall ((i Int))
      (= NULL (&gt;=_B i nullInt))))
  
  (assert (forall ((i Int))
      (= NULL (&gt;=_B nullInt i))))
  </code></pre>
  <p>Finally, with the above definitions, I use the <code>&gt;=_B</code> function in my assertions but keep getting unexpected UNSAT or unknown. I would like to know what makes the theory falls into the undecidable area. Is it because of the Boolean sort I made? or Is it because of the assertions in which I quantify over the infinite set of Int?</p>