Though the 'square' and 'rhombus' operators from modal logic are not truth-functional, it's because modal logic is interpreted as a binary logic, isn't it? What if modal logic is considered many-valued? That is, if it is, then the modality operators may be able to be truth-functional, aren't they?
So I picked provability logic as the modal logic to seek, and assumed it to be ternary. My plan was, step by step:

  1. Find all the truth tables that satisfies all the axioms.
  2. Pick an appropriate one.
  3. Give appropriate name for the truth values, judging by the truth table.

But I couldn't do step 2 and step 3, because the truth tables from step 1 seemed nonsense. For example:

Truth table of negation (¬A):
A:   F U T
¬A: T U F
Truth table of implication (A → B):
A: F U T
F  U T U
U  U T T
T  U T T
Truth table of necessity (□A):
A:  F U T
□A: U U T

Where A and B are statements, F, U and T are arbitrary name for the truth values, among which T is the designated value for truth.
Another Example:

Truth table of negation (¬A):
A:   F U T
¬A: T U F
Truth table of implication (A → B):
A: F U T
F  T F T
U  T F F
T  T F T
Truth table of necessity (□A):
A:  F U T
□A: F F T

So how should I do step 2 and step 3?
Besides, here is the Haskell code I wrote to do step 1:

import Data.List

data Trool = False3 | Unknown3 | True3 deriving (Eq, Enum)

firstLetter :: Trool -> Char
firstLetter False3 = 'F'
firstLetter Unknown3 = 'U'
firstLetter True3 = 'T'

makeTable :: [a] -> Int -> [[a]]
makeTable _ 0 = [[]]
makeTable xs n = do
    x <- xs
    smallTable <- makeTable xs $ n-1
    [x : smallTable]

unaryTruthTables :: [[Trool]]
unaryTruthTables = makeTable [False3 .. True3] 3

binaryTruthTables :: [[[Trool]]]
binaryTruthTables = makeTable unaryTruthTables 3

infix 9 <!!>
(<!!>) :: [a] -> Trool -> a
xs <!!> t = xs !! fromEnum t

ternaryTest :: (Trool -> Trool) -> Bool
ternaryTest f = all (True3 ==) $ map f [False3 .. True3]

ternaryTest2 :: (Trool -> Trool -> Trool) -> Bool
ternaryTest2 f2 = and $ map (ternaryTest . f2) [False3 .. True3]

ternaryTest3 :: (Trool -> Trool -> Trool -> Trool) -> Bool
ternaryTest3 f3 = and $ map (ternaryTest2 . f3) [False3 .. True3]

possibleSystems :: [([Trool] {-negation-}, [[Trool]] {-implication-}, [Trool] {-necessity-})]
possibleSystems = do
    notTable <- [[True3, Unknown3, False3]]
    implyTable <- binaryTruthTables
    squareTable <- unaryTruthTables
    let not = (notTable <!!>)
    let p --> q = (implyTable <!!> p) <!!> q
    let square = (squareTable <!!>)
    let rhombus = not . square . not
    if and [
        ternaryTest2 (\p q -> p --> (q --> p)),
        ternaryTest3 (\p q r -> (p --> (q --> r)) --> ((p --> q) --> (p --> r))),
        ternaryTest2 (\p q -> ((not p --> not q) --> (q --> p))),
        ternaryTest2 (\p q -> square (p --> q) --> (square p --> square q)) -- Distribution Axiom
        ,ternaryTest (\p -> square (square p --> p) --> square p) -- Loeb's Axiom
        ] then [(notTable,implyTable,squareTable)] else []

printSystem :: Int -> ([Trool], [[Trool]], [Trool]) -> IO ()
printSystem n (notTable, implyTable, squareTable) = do
    putStrLn $ "System #" ++ show n
		putStrLn "Truth table of negation:"
		foldr1 (>>) $ map putStrLn $ transpose ["FUT", map firstLetter notTable]
		putStrLn "Truth table of implication:"
		putStrLn " FUT"
		foldr1 (>>) $ map putStrLn $ transpose $ concat [["FUT"], transpose $ map (map firstLetter) implyTable]
		putStrLn "Truth table of necessity:"
		foldr1 (>>) $ map putStrLn $ transpose ["FUT", map firstLetter squareTable]
		--putStrLn "Truth table of possibility:"
		--foldr1 (>>) $ map putStrLn $ transpose ["FUT", map firstLetter rhombusTable]

main :: IO ()
main = foldr1 (>>) $ map (uncurry printSystem) $ zip [0..] possibleSystems
  • 2
    $\begingroup$ It is possible you are trying to carry out something impossible. It's hard to dissect your code to determine what truth-values are being assigned, but you apparently consider three values, despite the opening paragraph mentioning "binary logic". While modal logic is necessarily a superset of propositional logic, it is unclear how you approach "provability" as a ternary logic. Perhaps reworking the statement of what is intended would make the code more understandable? $\endgroup$ – hardmath Sep 16 '17 at 2:30
  • $\begingroup$ @hardmath False3, Unknown3 and True3 are arbitrary name for the truth values, and I have no actual intention for them. What motivated me to pick the provability logic was the Goedel's incompleteness theorems, which show that there are statements that cannot be proven to be either true or false. So originally I thought this as the third truth value, but the results from step 1 doesn't quite seem to state this actually is. $\endgroup$ – Dannyu NDos Sep 16 '17 at 2:36
  • 1
    $\begingroup$ @hardmath Another motivation is, I was making logical semantics for ternary computers, like logic gates, flip-flap-flops, etc. It seems that there is no united standard name for ternary logic gates, so I was going to build logical semantics to give appropriate name for them. $\endgroup$ – Dannyu NDos Sep 16 '17 at 2:41
  • $\begingroup$ I think that modal logic not being truth-functional is more akin to quantifier logic not being truth-functional than what you've attempted (expanding from two "binary" truth values to three). Let me think about your edit carefully to see if I can respond in a cogent way. $\endgroup$ – hardmath Sep 16 '17 at 2:42

I think you're asking whether or not, or perhaps claim that, modal logic can be reduced to truth-functional, many-valued logic. If this is the question, then the answer is no. Some explanations below.

It is important to make a distinction between the formalism and the semantics of a modal logic (system).

A modal logic (system) is formally defined, for example Hilbert style, by its syntax, axioms and rules. Thereafter, a formula is considered a theorem iff it can be formally proved from the above. This uniquely defines the set of formulas that are theorems of that system. (And this set is also considered to be the modal logic, i.e. the system is identified with the set of all its theorems.) So whether or not a formula is is a theorem is only a matter of formal derivation. It has nothing to do with the semantics or any interpretation of the formula.

Also: if there is an algorithm that allows you to decide, given any arbitrary formula, whether or not it is a theorem, then that modal logic is called decidable. NOTE: It has bee proven that there are modal logics that are not decidable.

A semantics is a/any different method (finitary or not) to associate a truth value to each formula. You can in principle invent any semantics S that you want, including one based on multi-valued truth tables. But then you run into the following questions:

  • Is your modal logic sound with respect to S? i.e. is every theorem S-valid?
  • Is your modal logic complete with respect to S? i.e. is every S-valid formula a theorem.

Having both would mean that a formula is a theorem iff it its S-valid.

Now, your truth-table semantics for modal logics being finitary means validity would be decidable. Therefore, in such semantics you cannot have soundness and completeness for all modal logics, because it would imply that all modal logics are decidable. Which they are certainly not.

The usual semantics for normal modal logics is the Kripke semantics. In this semantics all modal logics are sound, but there are many that are incomplete. There is also the general frame semantics, under which all modal logics are sound and complete. But neither provides a finitary algorithm for evaluating validity, such as to make all modal logics decidable.

Of course, you are still free to define your truth-table based semantics for modal logic. The only question is: how useful is it (what would you do with it)? As illustated, you would not be able to use it to decide theoremship in all cases.

There are certainly some (particular) modal logics that are decidable and can be "reduced" to truth-based logics. For example the ultra-simple Triv and Ver systems, in a quite straightforward way. (I once saw an attempt to do this for the system S5; it worked for some formulas, not sure if for all.)

For your example case study, I doubt that you can achieve soundness and completeness for provability logic in this way. This is because it has an axiom of modal degree 2, and not a particularly simple one. But it's certainly not enough to postulate some (multi-valued) truth tables. You also need to mathematically examine soundness and completeness with respect to them.


The attempt has been made to create a sound, decidable modal logic with a finite number of truth values using the 3-valued logic of Lukasiewicz. This has not been regarded as successful; although my search of the literature has not turned up a good, sound explanation for why not.

The most important reason seems to have been the difficulty of establishing sound rules of inference. Difficulty of semantic interpretation, an unreasonable adherence to the "laws" of bivalence and the excluded middle, and unfamiliar notation have also played a part.

Both of your proposed Truth tables of implication (A → B) have serious problems. For one, they do not reduce to those of classical logic in the case of propositions which have the values T and F. For another, they do not even recognize such elementary rules of inference as (A → A) as valid.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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