# Are there proof assistants for multi-valued logics?

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

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.