There are several three-valued logics (like those used in OCL or VDM), four-valued logics (e.g. used for paraconsistency) and real-valued logics (e.g. fuzzy logics with Gödel's or Łukasiewicz's connectives). Are there any proof assistants for these, either directly or via some encodings in some two-valued logic?


1 Answer 1


I'm going to tackle the non-classical propositional logic case.

Any proof assistant that is capable of proving things in classical first-order logic can be used to analyze a propositional logic by using the following translation. In so doing, we are using the matrix semantics.

Let $D$ be a one-place predicate that returns true if and only if its argument has a designated truth value. I also insist that for every $n$-ary connective (such as $\cdot$), I have an $n$-ary function (let's say $A$). I'll use $\land, \lor, \lnot$ as classical connectives exclusively.

The inference rule $\frac{A \;\;\text{and}\;\; B}{A \cdot B}$ corresponds to $\forall a, b \mathop. D(a) \land D(b) \to D(A(a, b)) $.

In order to analyze a system like Belnap's four-valued logic, you can introduce another predicate $F$ for the falsity conditions. Within classical FOL, $F$ and $D$ do not have a relationship with each other.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.