Fully truth-functional version of modal logic?

Question

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
B
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
B
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

Answer 1

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.