AlgoVerse

Truth table

For every assignment of the variables, work out each subformula from the inside out, and finally say whether the formula is always true (a tautology), always false (a contradiction) or sometimes true.

A propositional formula's value depends only on its variables' values. With n variables there are 2^n assignments; the truth table has a row for each.

Read the full explanation ↓
Input:
formula="(p>q)=(~q>~p…"PDF export

(p → q) ↔ (¬q → ¬p): a conditional is equivalent to its contrapositive; all four rows are true: a tautology.

  1. class Node:
  2. def __init__(self, op, left, right, text):
  3. self.op = op
  4. self.left = left
  5. self.right = right
  6. self.text = text # how the subformula is written
  9. def truth_table(formula):
  10. root = parse(formula)
  11. if root is None:
  12. return None
  13. names = []
  14. columns = []
  15. collect(root, names, columns)
  16. names.sort()
  17. header = names + [c.text for c in columns]
  18. rows = [header]
  19. trues = 0
  20. for m in range(2 ** len(names)):
  21. env = {}
  22. for i in range(len(names)):
  23. env[names[i]] = (m >> (len(names) - 1 - i)) % 2 == 1
  24. row = []
  25. for name in names:
  26. row.append("T" if env[name] else "F")
  27. for c in columns:
  28. env[c.text] = value(c, env)
  29. row.append("T" if env[c.text] else "F")
  30. rows.append(row)
  31. last = env[root.text]
  32. if last:
  33. trues = trues + 1
  34. if trues == 2 ** len(names):
  35. kind = "tautology"
  36. elif trues == 0:
  37. kind = "contradiction"
  38. else:
  39. kind = "contingent"
  40. return kind
  43. def value(c, env):
  44. # Each column only reads columns to its left: its operands were filled in first.
  45. if c.op == "¬":
  46. return not env[c.right.text]
  47. a = env[c.left.text]
  48. b = env[c.right.text]
  49. if c.op == "∧":
  50. return a & b
  51. if c.op == "∨":
  52. return a | b
  53. if c.op == "→":
  54. return (not a) | b
  55. return a == b
  58. def collect(node, names, columns):
  59. # Postorder, so every column comes after the columns it depends on; a repeated subformula gets one column.
  60. if node.op == "var":
  61. if node.text not in names:
  62. names.append(node.text)
  63. return
  64. if node.left is not None:
  65. collect(node.left, names, columns)
  66. collect(node.right, names, columns)
  67. for c in columns:
  68. if c.text == node.text:
  69. return
  70. columns.append(node)
  73. def parse(text):
  74. # ~ not, & and, | or, > implies, = if and only if; from tightest to loosest. > groups to the right.
  75. toks = []
  76. for c in text:
  77. if c != " ":
  78. toks.append(c)
  79. pos = [0]
  80. root = parse_binary(toks, pos, 0)
  81. if root is None or pos[0] != len(toks):
  82. return None
  83. return root
  86. LEVELS = [["=", "↔"], [">", "→"], ["|", "∨"], ["&", "∧"]]
  89. def parse_binary(toks, pos, level):
  90. if level == len(LEVELS):
  91. return parse_not(toks, pos)
  92. sym, op = LEVELS[level]
  93. left = parse_binary(toks, pos, level + 1)
  94. while left is not None and pos[0] < len(toks) and toks[pos[0]] == sym:
  95. pos[0] += 1
  96. right = parse_binary(toks, pos, level if sym == ">" else level + 1)
  97. if right is None:
  98. return None
  99. left = Node(op, left, right, "(" + left.text + " " + op + " " + right.text + ")")
  100. return left
  103. def parse_not(toks, pos):
  104. if pos[0] >= len(toks):
  105. return None
  106. c = toks[pos[0]]
  107. pos[0] += 1
  108. if c == "~":
  109. inner = parse_not(toks, pos)
  110. if inner is None:
  111. return None
  112. return Node("¬", None, inner, "¬" + inner.text)
  113. if c == "(":
  114. inner = parse_binary(toks, pos, 0)
  115. if inner is None or pos[0] >= len(toks) or toks[pos[0]] != ")":
  116. return None
  117. pos[0] += 1
  118. return inner
  119. if c.isalpha():
  120. return Node("var", None, None, c)
  121. return None

Invariant: Each column uses only columns to its left, so by the time we reach it its operands are filled in.

Start

trues—
kind—

The table is still empty.

Recursion tree

Filled orange = running call · Orange outline = still on the stack · Grey = finished

Local variables

formula'(p>q)=(~q>~p)'

Orange = changed in this step

Call stack

  1. truth_table()line 9
Step 1 of 655
Black = row · Orange = key stepcolumns: 0/1 · row: 0/4 · tautology: 0/1
    Explanation

    The idea

    A propositional formula's value depends only on its variables' values. With n variables there are 2^n assignments; the truth table has a row for each.

    To keep it readable, besides the variables' columns there is a column for every subformula, from the innermost outwards. Each column only needs the columns before it.

    The operators

    | Typed | Operator | True when | |---|---|---| | ~ | ¬ | the operand is false | | & | ∧ | both are true | | \| | ∨ | at least one is true | | > | → | the antecedent is false or the consequent true | | = | ↔ | both have the same value |

    Classifying

    • Tautology: every row is true; rules of inference, for example.
    • Contradiction: no row is true.
    • Contingent: some rows.

    Two formulas are equivalent if A ↔ B is a tautology.

    The input

    The variables are p, q, r and s. ~ binds tightest and = loosest; > groups to the right.