Skip to content

# Formal Logic Compendium

Build a formula from letters, connectives, quantifiers and modalities, then read its truth table, its tableau, its value in a model or at a world of a frame, and a checked proof. Nothing here is written down: every value is computed as you press.

Rendered when the site was built, by the same code the browser runs. No JavaScript required. With JavaScript on, this is replaced by the workbench, where you build your own formula and get all of the below for it instead, across 6 tabbed surfaces. Each section below opens on its own heading, and nothing here needs a script to open it.

## The five connectives

5 connectives

Every row of this table is the result of really evaluating the formula at the top of its column, not a definition typed out beside an implementation that might have drifted from it.

The five connectives, defined. T is true and F is false.
p | q | ¬p | p ∧ q | p ∨ q | p → q | p ↔ q
--- | --- | --- | --- | --- | --- | ---
T | T | F | T | T | T | T
T | F | F | F | T | F | F
F | T | T | F | T | T | F
F | F | T | F | F | T | T

¬ negation
  Reads as not A. The only one that takes a single side. It swaps true for false and false for true, and two of them in a row give you back what you started with.
∧ conjunction
  Reads as A and B. The strict one. Both sides have to hold, so a conjunction is false as soon as either half is.
∨ disjunction
  Reads as A or B, or both. Inclusive, unlike most English uses of the word: tea or coffee is still true if you take both. The exclusive sense is written out as a formula instead.
→ implication
  Reads as if A then B. The one that surprises people. It claims only that you never get a true left side with a false right side, so it is true whenever the left side is false. It is a promise nobody broke, not a claim that one thing caused the other.
↔ biconditional
  Reads as A if and only if B. Agreement. True when both sides have the same value, which is why it is the connective a law such as De Morgan's is stated with.

## A worked truth table

8 columns · 4 rows

De Morgan's law. Eight subformula columns, and the two sides agree on every row.. 8 subformula columns over 4 rows, because a table that showed only the answer would be the answer key rather than the working.

Truth table for ¬(p ∧ q) ↔ ¬p ∨ ¬q. T is true and F is false.
p | q | ¬p | ¬q | p ∧ q | ¬(p ∧ q) | ¬p ∨ ¬q | ¬(p ∧ q) ↔ ¬p ∨ ¬q
--- | --- | --- | --- | --- | --- | --- | ---
T | T | F | F | T | F | F | T
T | F | F | T | F | T | T | T
F | T | T | F | F | T | T | T
F | F | T | T | F | T | T | T

Tautology: true on all 4 rows, whatever p and q are.

## A closed tableau

9 lines · 2 branches

Is (p → q) → ¬q → ¬p a tautology? Assume it is false and apply one rule at a time. A branch closes when it holds the same formula both true and false. If every branch closes, nothing can make the formula false. Every line below names the rule that produced it and the line it was applied to, and each branch says how it ended.

1. 1. F (p → q) → ¬q → ¬p [assumption]
2. 2. T p → q [from 1, false implication]
3. 3. F ¬q → ¬p [from 1, false implication]
4. 4. T ¬q [from 3, false implication]
5. 5. F ¬p [from 3, false implication]
6. 6. F q [from 4, true negation]
7. 7. T p [from 5, false negation]
8. 8. T q [from 2, true implication]closed: line 8 contradicts line 6
9. 9. F p [from 2, true implication]closed: line 9 contradicts line 7

2 branches, all closed. (p → q) → ¬q → ¬p is a tautology.

    Is (p → q) → ¬q → ¬p a tautology?
    Assume it is false and apply one rule at a time. A branch closes when it holds the same formula both true and false. If every branch closes, nothing can make the formula false.

    1. F (p → q) → ¬q → ¬p [assumption]
    2. T p → q [from 1, false implication]
    3. F ¬q → ¬p [from 1, false implication]
    4. T ¬q [from 3, false implication]
    5. F ¬p [from 3, false implication]
    6. F q [from 4, true negation]
    7. T p [from 5, false negation]
      8. T q [from 2, true implication]
         [closed] 8 contradicts 6
      9. F p [from 2, true implication]
         [closed] 9 contradicts 7

    2 branches, all closed. (p → q) → ¬q → ¬p is a tautology.

## The tableau rules

10 rules

Ten rules, one for each connective on each side of the question. Five of them split the branch, which is what a tree in a logic book is a picture of.

The ten tableau rules
Rule | Shape | What it says
--- | --- | ---
true negation | one branch | If ¬A is true then A is false. One line, same branch.
false negation | one branch | If ¬A is false then A is true. One line, same branch.
true conjunction | one branch | If A ∧ B is true then both halves are. Two lines, same branch.
false conjunction | splits | If A ∧ B is false then at least one half is. Which one is unknown, so the branch splits.
true disjunction | splits | If A ∨ B is true then at least one half is. Which one is unknown, so the branch splits.
false disjunction | one branch | If A ∨ B is false then both halves are. Two lines, same branch.
true implication | splits | If A → B is true then either A fails or B holds. The branch splits.
false implication | one branch | There is only one way to break a promise: A true and B false. Two lines, same branch.
true biconditional | splits | If A ↔ B is true then the two agree: both true, or both false.
false biconditional | splits | If A ↔ B is false then the two differ, one way round or the other.

## The worked examples

12 examples

Each of these is a script the builder could run, so nothing here is a formula the workbench could not make. At most 5 letters, and the verdict is computed rather than claimed.

Every worked example, with its computed verdict
Name | Formula | Verdict | True rows | Tautology tableau | Why it is here
--- | --- | --- | --- | --- | ---
Identity | p → p | Tautology | 2 of 2 | 1 branch, all closed | The smallest tautology worth the name. Its tableau closes in three lines.
Excluded middle | p ∨ ¬p | Tautology | 2 of 2 | 1 branch, all closed | The law of excluded middle: either it holds or it does not, with no third option.
The basic contradiction | p ∧ ¬p | Contradiction | 0 of 2 | 2 open of 2 branches | The other end of the same idea. False on every row, which is what a contradiction is.
Material implication | p → q | Contingency | 3 of 4 | 1 open of 1 branch | The row that surprises everyone is the third one: a false left side makes the whole thing true.
De Morgan's law | ¬(p ∧ q) ↔ ¬p ∨ ¬q | Tautology | 4 of 4 | 4 branches, all closed | De Morgan's law. Eight subformula columns, and the two sides agree on every row.
Contraposition | (p → q) → ¬q → ¬p | Tautology | 4 of 4 | 2 branches, all closed | Contraposition: if p brings q, then no q means no p. The tableau splits and both halves close.
Hypothetical syllogism | (p → q) ∧ (q → r) → p → r | Tautology | 8 of 8 | 3 branches, all closed | The hypothetical syllogism: chaining two conditionals. Three letters, eight rows.
Affirming the consequent | (p → q) ∧ q → p | Contingency | 3 of 4 | 2 open of 2 branches | A fallacy, and the table shows exactly which row breaks it: p false, q true.
Exclusive or | (p ∨ q) ∧ ¬(p ∧ q) | Contingency | 2 of 4 | 2 open of 2 branches | Exclusive or, written out. There is no symbol for it here because it is not primitive: it is this.
Peirce's law | ((p → q) → p) → p | Tautology | 4 of 4 | 2 branches, all closed | Peirce's law. It uses no negation at all and is still a tautology, which is what makes it worth a look.
Denying the antecedent | (p → q) ∧ ¬p → ¬q | Contingency | 3 of 4 | 2 open of 2 branches | The mirror of the other conditional fallacy, and the table breaks it on the same kind of row: p false, q true.
Affirming a disjunct | (p ∨ q) ∧ p → ¬q | Contingency | 3 of 4 | 2 open of 2 branches | An or does not promise that only one side holds, so knowing one of them says nothing about the other.

## A tableau that stays open

7 lines · 2 open branches

The other half of the method. Nothing closes here, and the letters along the open branch are the counterexample.

1. 1. F (p → q) ∧ q → p [assumption]
2. 2. T (p → q) ∧ q [from 1, false implication]
3. 3. F p [from 1, false implication]
4. 4. T p → q [from 2, true conjunction]
5. 5. T q [from 2, true conjunction]
6. 6. T q [from 4, true implication]open: nothing left to apply, and p false, q true
7. 7. F p [from 4, true implication]open: nothing left to apply, and p false, q true

2 branches, 0 closed and 2 open. (p → q) ∧ q → p is not a tautology: it is false when p false, q true.

## Quantifiers over a finite domain

3 predicates · 2 quantifiers

A quantifier ranges over a domain of at most 3 things, written 1, 2 and 3. That ceiling is what keeps every answer below exact: over a finite domain for every is a conjunction of instances and there is a disjunction of them, so a claim about everything is settled by settling everything. The variables are x, y, z, and the predicates are the ones in the table below.

The predicates, and how many things each one is about
Predicate | Places | Reads as
--- | --- | ---
P | 1 place | P of x
Q | 1 place | Q of x
R | 2 places | R of x and y

The two quantifiers, and what each one claims
Symbol | Name | Reads as | What to know
--- | --- | --- | ---
∀ | universal quantifier | for every x, A | A claim about everything in the domain at once. One element that fails is enough to sink it, which is why a counterexample is worth more than a hundred examples.
∃ | existential quantifier | for some x, A | A claim that at least one thing fits. It says nothing about which, so a witness proves it and no amount of failures short of all of them refutes it.

## A worked model

2 evaluations · 9 models

A model is a domain and, for every predicate, the things it holds of. Anything not listed is false, which is what makes a model a finite object rather than a list of everything that is not the case.

What the one-place predicates hold of
Thing | P | Q
--- | --- | ---
1 | out | out
2 | out | out
3 | out | out

R holds of these pairs. The row is the first thing and the column the second.
First | 1 | 2 | 3
--- | --- | --- | ---
1 | out | in | out
2 | out | out | in
3 | in | out | out

The domain is 1, 2 and 3; P holds of nothing; Q holds of nothing; R holds of (1,2), (2,3) and (3,1).

### Everyone has someone

A two-place predicate under two quantifiers. Every element points at one, going round in a ring.

1. T ∀x ∃y R(x,y)true at every element: 1, 2 and 3.
2. T ∃y R(1,y)true at y = 2.
3. F R(1,1)R does not hold of 1 and 1 in this model.
4. T R(1,2)R holds of 1 and 2 in this model.
5. F R(1,3)R does not hold of 1 and 3 in this model.
6. T ∃y R(2,y)true at y = 3.
7. F R(2,1)R does not hold of 2 and 1 in this model.
8. F R(2,2)R does not hold of 2 and 2 in this model.
9. T R(2,3)R holds of 2 and 3 in this model.
10. T ∃y R(3,y)true at y = 1.
11. T R(3,1)R holds of 3 and 1 in this model.
12. F R(3,2)R does not hold of 3 and 2 in this model.
13. F R(3,3)R does not hold of 3 and 3 in this model.

∀x ∃y R(x,y) is true in this model.

    Is ∀x ∃y R(x,y) true in this model?
    The domain is 1, 2 and 3; P holds of nothing; Q holds of nothing; R holds of (1,2), (2,3) and (3,1).

    T ∀x ∃y R(x,y): true at every element: 1, 2 and 3.
      T ∃y R(1,y): true at y = 2.
        F R(1,1): R does not hold of 1 and 1 in this model.
        T R(1,2): R holds of 1 and 2 in this model.
        F R(1,3): R does not hold of 1 and 3 in this model.
      T ∃y R(2,y): true at y = 3.
        F R(2,1): R does not hold of 2 and 1 in this model.
        F R(2,2): R does not hold of 2 and 2 in this model.
        T R(2,3): R holds of 2 and 3 in this model.
      T ∃y R(3,y): true at y = 1.
        T R(3,1): R holds of 3 and 1 in this model.
        F R(3,2): R does not hold of 3 and 2 in this model.
        F R(3,3): R does not hold of 3 and 3 in this model.

    ∀x ∃y R(x,y) is true in this model.

### Someone everyone has

The same model, the two quantifiers swapped. This is the difference between everyone having someone and there being someone everyone has, and it is a different claim rather than the same one said backwards.

1. F ∃y ∀x R(x,y)false at every element: 1, 2 and 3.
2. F ∀x R(x,1)false at x = 1.
3. F R(1,1)R does not hold of 1 and 1 in this model.
4. F R(2,1)R does not hold of 2 and 1 in this model.
5. T R(3,1)R holds of 3 and 1 in this model.
6. F ∀x R(x,2)false at x = 2.
7. T R(1,2)R holds of 1 and 2 in this model.
8. F R(2,2)R does not hold of 2 and 2 in this model.
9. F R(3,2)R does not hold of 3 and 2 in this model.
10. F ∀x R(x,3)false at x = 1.
11. F R(1,3)R does not hold of 1 and 3 in this model.
12. T R(2,3)R holds of 2 and 3 in this model.
13. F R(3,3)R does not hold of 3 and 3 in this model.

∃y ∀x R(x,y) is false in this model.

    Is ∃y ∀x R(x,y) true in this model?
    The domain is 1, 2 and 3; P holds of nothing; Q holds of nothing; R holds of (1,2), (2,3) and (3,1).

    F ∃y ∀x R(x,y): false at every element: 1, 2 and 3.
      F ∀x R(x,1): false at x = 1.
        F R(1,1): R does not hold of 1 and 1 in this model.
        F R(2,1): R does not hold of 2 and 1 in this model.
        T R(3,1): R holds of 3 and 1 in this model.
      F ∀x R(x,2): false at x = 2.
        T R(1,2): R holds of 1 and 2 in this model.
        F R(2,2): R does not hold of 2 and 2 in this model.
        F R(3,2): R does not hold of 3 and 2 in this model.
      F ∀x R(x,3): false at x = 1.
        F R(1,3): R does not hold of 1 and 3 in this model.
        T R(2,3): R holds of 2 and 3 in this model.
        F R(3,3): R does not hold of 3 and 3 in this model.

    ∃y ∀x R(x,y) is false in this model.

Every worked model, with its computed answer
Name | Formula | Domain | Answer | Why it is here
--- | --- | --- | --- | ---
Everything has it | ∀x P(x) | 3 elements | yes | The universal claim with every element checked. Three instances, all true, and the working shows all three rather than stopping at the answer.
One element short | ∀x P(x) | 3 elements | no | The same formula, one fact removed. A universal claim needs every element, so a single counterexample settles it, and the working names which one.
Something with both | ∃x (P(x) ∧ Q(x)) | 3 elements | yes | An existential claim, and the working names the witness rather than reporting that one exists somewhere.
Every one of them is one of these | ∀x (P(x) → Q(x)) | 3 elements | yes | The shape of nearly every sentence anyone reasons with. It is a conditional inside a universal, so the elements without P make it true for free.
Everyone has someone | ∀x ∃y R(x,y) | 3 elements | yes | A two-place predicate under two quantifiers. Every element points at one, going round in a ring.
Someone everyone has | ∃y ∀x R(x,y) | 3 elements | no | The same model, the two quantifiers swapped. This is the difference between everyone having someone and there being someone everyone has, and it is a different claim rather than the same one said backwards.
Pointing back | ∀x ∀y (R(x,y) → R(y,x)) | 2 elements | no | Symmetry, and a model that has not got it: one arrow with no arrow the other way is the whole counterexample.
Not everything, so something not | ¬(∀x P(x)) ↔ (∃x ¬P(x)) | 3 elements | yes | De Morgan's law with quantifiers in place of the connectives. It is true in every model there is, which is why the tableau below it closes.
Pointing at itself | R(1,1) | 3 elements | yes | A closed instance rather than a quantified claim: the page can ask about one element by name, which is what the elements are in the argument picker for.

## A quantifier tableau

19 lines · 5 rules

Is ¬(∀x P(x)) ↔ (∃x ¬P(x)) true in every model of a domain of 2? Assume some model makes it false and apply one rule at a time. A quantifier is taken apart over the elements one by one. If every branch closes, no model of this size can make the formula false. Each quantifier is taken apart over the elements one at a time, which is why the tree is finite and why it finishes.

1. 1. F ¬(∀x P(x)) ↔ (∃x ¬P(x)) [assumption]
2. 2. F ¬(∀x P(x)) [from 1, false biconditional]
3. 3. T ∃x ¬P(x) [from 1, false biconditional]
4. 4. T ¬(∀x P(x)) [from 1, false biconditional]
5. 5. F ∃x ¬P(x) [from 1, false biconditional]
6. 6. F ∀x P(x) [from 4, true negation]
7. 7. F ¬P(1) [from 5, false there-is]
8. 8. F ¬P(2) [from 5, false there-is]
9. 9. T P(1) [from 7, false negation]
10. 10. T P(2) [from 8, false negation]
11. 11. F P(2) [from 6, false for-all]closed: line 11 contradicts line 10
12. 12. F P(1) [from 6, false for-all]closed: line 12 contradicts line 9
13. 13. T ∀x P(x) [from 2, false negation]
14. 14. T P(1) [from 13, true for-all]
15. 15. T P(2) [from 13, true for-all]
16. 16. T ¬P(2) [from 3, true there-is]
17. 17. T ¬P(1) [from 3, true there-is]
18. 18. F P(1) [from 17, true negation]closed: line 18 contradicts line 14
19. 19. F P(2) [from 16, true negation]closed: line 19 contradicts line 15

4 branches, all closed. ¬(∀x P(x)) ↔ (∃x ¬P(x)) is true in every model of a domain of 2.

The quantifier rules, and the one the contradiction symbol takes
Rule | Shape | What it says
--- | --- | ---
true for-all | one branch | If ∀x A is true then A is true of every element there is. One line per element, same branch.
false for-all | splits per element | If ∀x A is false then some element breaks it. Which one is unknown, so the branch splits once per element.
true there-is | splits per element | If ∃x A is true then some element witnesses it. Which one is unknown, so the branch splits once per element.
false there-is | one branch | If ∃x A is false then A fails of every element. One line per element, same branch.
true contradiction | one branch | Nothing makes ⊥ true, so a branch that has taken it as true is a dead end and closes where it stands.

## A checked proof

2 derivations · 14 lines

Every line below was produced by the rule beside it, from the lines it names, and the whole derivation was run through the checker when this page was built. Nothing here is a transcription: a proof that stopped being derivable would fail the build rather than sit here as a claim.

### One of De Morgan's laws, derived

The law phase 1 read off a truth table, this time written forwards. Two reductios and a conjunction, and nothing in it is a table lookup.

¬(p ∨ q) ⊢ ¬p ∧ ¬q

1. 1. ¬(p ∨ q)premise
2. 2. p assumption
3. 3. p ∨ q or introduction, left, line 2, with q
4. 4. ⊥not elimination, lines 3 and 1
5. 5. ¬p not introduction, discharging line 2
6. 6. q assumption
7. 7. p ∨ q or introduction, right, line 6, with p
8. 8. ⊥not elimination, lines 7 and 1
9. 9. ¬q not introduction, discharging line 6
10. 10. ¬p ∧ ¬q and introduction, lines 5 and 9

Proved. ¬p ∧ ¬q follows from the premises, on line 10.

    Prove not p and not q from not (p or q).
    ¬(p ∨ q) ⊢ ¬p ∧ ¬q

    1. ¬(p ∨ q) [premise]
      2. p [assumption]
      3. p ∨ q [or introduction, left, line 2, with q]
      4. ⊥ [not elimination, lines 3 and 1]
    5. ¬p [not introduction, discharging line 2]
      6. q [assumption]
      7. p ∨ q [or introduction, right, line 6, with p]
      8. ⊥ [not elimination, lines 7 and 1]
    9. ¬q [not introduction, discharging line 6]
    10. ¬p ∧ ¬q [and introduction, lines 5 and 9]

    Proved. ¬p ∧ ¬q follows from the premises, on line 10.

### Coming down to one thing

The first predicate derivation. A claim about everything is taken at one named element, and then it is ordinary detaching.

∀x (P(x) → Q(x)), P(1) ⊢ Q(1)

1. 1. ∀x (P(x) → Q(x))premise
2. 2. P(1)premise
3. 3. P(1) → Q(1)for-all elimination, line 1, at 1
4. 4. Q(1)if elimination, lines 3 and 2

Proved. Q(1) follows from the premises, on line 4.

    Prove Q of 1 from for every x, (if P of x then Q of x) and P of 1.
    ∀x (P(x) → Q(x)), P(1) ⊢ Q(1)

    1. ∀x (P(x) → Q(x)) [premise]
    2. P(1) [premise]
    3. P(1) → Q(1) [for-all elimination, line 1, at 1]
    4. Q(1) [if elimination, lines 3 and 2]

    Proved. Q(1) follows from the premises, on line 4.

## The two methods, agreeing

10 sequents

A derivation and a tableau are independent verdicts on one sequent, so the page prints both rather than either. Every row below is a proof the checker accepted and a tree that closed over the same sequent; a row where they disagreed would be a bug in one of them, which is exactly what makes the pair worth printing.

Every worked derivation, and the tableau over its sequent
Name | Sequent | Lines | Checker | Tableau | Why it is here
--- | --- | --- | --- | --- | ---
Detaching | p → q, p ⊢ q | 3 lines | yes | 1 branch, all closed | The whole of modus ponens in one move. A conditional and its left side give up the right side.
Chaining two conditionals | p → q, q → r ⊢ p → r | 6 lines | yes | 3 branches, all closed | The first proof that needs a subproof. Assume the left side, get to the right side, and the conditional falls out with the assumption discharged.
Turning a conditional round | p → q ⊢ ¬q → ¬p | 7 lines | yes | 2 branches, all closed | Two subproofs, one inside the other, and a reductio at the bottom of them. The closed tableau for this sequent is one branch; the derivation is seven lines, which is what the two methods cost against each other.
One of De Morgan's laws, derived | ¬(p ∨ q) ⊢ ¬p ∧ ¬q | 10 lines | yes | 2 branches, all closed | The law phase 1 read off a truth table, this time written forwards. Two reductios and a conjunction, and nothing in it is a table lookup.
Taking both cases | p ∨ q, p → s, q → s ⊢ s | 4 lines | yes | 5 branches, all closed | Or elimination in one move: whichever half of the disjunction held, the same thing follows, so it follows.
The law of excluded middle, from nothing | ⊢ p ∨ ¬p | 9 lines | yes | 1 branch, all closed | No premises at all, and the only proof here that needs the classical rule. Phase 1 showed this law as two rows of a table; here is where it actually comes from.
Coming down to one thing | ∀x (P(x) → Q(x)), P(1) ⊢ Q(1) | 4 lines | yes | 1 branch, all closed | The first predicate derivation. A claim about everything is taken at one named element, and then it is ordinary detaching.
Going back up to everything | ∀x P(x) ⊢ ∀x (P(x) ∨ Q(x)) | 6 lines | yes | 2 branches, all closed | The other direction, and the one a finite domain makes honest: every element is taken in turn, and the general claim is put back together from all of them.
Naming a witness | P(1) ⊢ ∃x P(x) | 2 lines | yes | 1 branch, all closed | One move, and the smallest predicate proof there is: something true of an element is true of something.
Using a witness you were not given | ∃x P(x), ∀x (P(x) → Q(x)) ⊢ ∃x Q(x) | 14 lines | yes | 5 branches, all closed | The longest derivation here, and the one that shows what a finite domain buys: a there-is claim is written out as the disjunction it abbreviates, and then it is proof by cases like any other.

## The proof rules

20 rules

Twenty rules, read out of the checker that implements them. Discharge happens only through if introduction and not introduction, each closing the subproof it stands in, so nothing here asks a visitor to name a range of lines.

Every rule the checker knows
Rule | Symbol | Cites | What it says
--- | --- | --- | ---
reiteration | R | 1 line | Write an accessible line again. It proves nothing new and is sometimes the clearest way to end a subproof.
and introduction | ∧I | 2 lines | From A and B, infer A and B together. Two lines in, one out.
and elimination, left | ∧E left | 1 line | From a conjunction, infer its left half. A conjunction claims both.
and elimination, right | ∧E right | 1 line | From a conjunction, infer its right half. A conjunction claims both.
or introduction, left | ∨I left | 1 line | From A, infer A or anything. A disjunction is weaker than either side, so this always holds and you pick what to weaken it to.
or introduction, right | ∨I right | 1 line | From B, infer anything or B. The same rule from the other side, and you pick the side you are adding.
or elimination | ∨E | 3 lines | Proof by cases. From A or B, together with A leading to C and B leading to C, infer C: whichever half held, C follows.
if introduction | →I | a subproof | Close the subproof you are in. Whatever it assumed leads to whatever it reached, so the conditional joining them holds without the assumption.
if elimination | →E | 2 lines | Detach. From a conditional and its left side, infer its right side. This is modus ponens.
if and only if introduction | ↔I | 2 lines | From the two conditionals that run in opposite directions, infer the biconditional they make together.
if and only if elimination, left | ↔E left | 2 lines | From a biconditional and its left side, infer its right side.
if and only if elimination, right | ↔E right | 2 lines | From a biconditional and its right side, infer its left side.
not introduction | ¬I | a subproof | Reductio. Close a subproof that assumed A and reached a contradiction, and infer that A is false.
not elimination | ¬E | 2 lines | From a formula and its negation, infer the contradiction. This is what a reductio is aiming at.
contradiction elimination | ⊥E | 1 line | From a contradiction, infer anything at all. A contradiction has already gone wrong, so nothing is left to protect.
double negation elimination | ¬¬E | 1 line | From a doubly negated formula, infer the formula. This is the classical step, and the excluded middle needs it.
for-all elimination | ∀E | 1 line | From a claim about everything, infer it about one named element. Pick which.
for-all introduction | ∀I | 3 lines | From the claim holding of every element one at a time, infer it of all of them. The domain is finite, so every instance really can be cited.
there-is introduction | ∃I | 1 line | From a claim about one element, infer that something answers to it. Name the witness and the variable that stands in for it.
there-is expansion | ∃X | 1 line | Over a finite domain a there-is claim is a disjunction of its instances, so it can be written out and eliminated with or elimination.

## Modal logic over a finite frame

2 modalities · 3 worlds

A modality is a claim about the worlds a world can see. A frame is at most 3 worlds and the arrows between them, so necessarily is a conjunction over the worlds one world sees and possibly a disjunction over them: the same finite fold a quantifier is over the domain, one index further out. That is what keeps every answer below exact, and it is why a world with no arrows out makes every necessity true.

The two modalities, and what each one claims
Symbol | Name | Reads as | What to know
--- | --- | --- | ---
□ | necessity | necessarily A | A claim about every world this one can see. A world that can see nothing at all makes it true for free, which is why saying a necessity is true says as much about the arrows as about the letters.
◇ | possibility | possibly A | A claim that some world this one can see fits. It is the other side of the same coin: possibly A is exactly not necessarily not A, and the page checks that rather than asserting it.

## A worked frame

2 evaluations · 2 worlds

A frame is a set of worlds and the arrows between them, plus what is true at each. Anything not drawn is not there, which is what makes a frame something you can hold in your head rather than a description of everywhere you cannot get to.

Which worlds each world can see. The row is the world looking and the column the world seen.
Sees | w1 | w2
--- | --- | ---
w1 | no | sees
w2 | no | no

There are 2 worlds; w1 sees w2; w2 sees nothing; at w1 nothing is assigned; at w2 p true.

### Necessary here

A necessity is a claim about the worlds this one can see, and it is settled by looking at all of them. w1 sees only w2, and p holds there.

1. T □p at w1 true at every world it sees: w2.
2. T p at w2 p is true at w2.

□p is true at w1.

    Is □p true at w1 in this frame?
    There are 2 worlds; w1 sees w2; w2 sees nothing; at w1 nothing is assigned; at w2 p true.

    T □p at w1: true at every world it sees: w2.
      T p at w2: p is true at w2.

    □p is true at w1.

### Necessary but not true

w1 does not see itself, so what it takes to be necessary need not hold there. This is the T axiom failing, and reflexivity is exactly the arrow it is missing.

1. F □p → p at w1 the left side is true and the right side is false.
2. T □p at w1 true at every world it sees: w2.
3. T p at w2 p is true at w2.
4. F p at w1 p is false at w1.

□p → p is false at w1.

    Is □p → p true at w1 in this frame?
    There are 2 worlds; w1 sees w2; w2 sees nothing; at w1 nothing is assigned; at w2 p true.

    F □p → p at w1: the left side is true and the right side is false.
      T □p at w1: true at every world it sees: w2.
        T p at w2: p is true at w2.
      F p at w1: p is false at w1.

    □p → p is false at w1.

## The axioms and the frames they need

5 axioms · 4 conditions · 2 frames

Each axiom below is valid on exactly the frames whose arrows satisfy one condition. The two frames compared here are a cluster in which every world sees every world (a frame for S5) and a chain in which nothing loops back (a frame for K), and every column moves between them precisely where its condition does. Nothing in this table is asserted: the condition is read off the arrows and the axiom is checked under every setting of its letters at every world.

Every axiom, its frame condition, and whether each holds on two different frames
Axiom | Formula | Condition | Cluster | Chain | What it says
--- | --- | --- | --- | --- | ---
K | □(p → q) → □p → □q | none | yes | yes | Necessity distributes over an implication. It holds whatever the arrows do, which is why every modal system starts from it.
T | □p → p | reflexive | yes | no | What is necessary is true. It needs every world to see itself, and one world that does not is enough to break it.
4 | □p → □□p | transitive | yes | no | What is necessary is necessarily necessary. It needs a two-step reach to be a one-step reach, which is transitivity and nothing else.
B | p → □◇p | symmetric | yes | no | What is true is necessarily possible. It needs every arrow to have one going back, so it is the axiom that makes a frame two-way.
5 | ◇p → □◇p | euclidean | yes | no | What is possible is necessarily possible. It needs any two worlds a world sees to see each other, which is what an equivalence relation gives for free.

What each condition asks of the arrows, and whether the chain above satisfies it
Condition | Chain | What it says | What is missing
--- | --- | --- | ---
reflexive | no | Every world sees itself. | w1 does not see itself.
transitive | no | If a world sees a second and that second sees a third, the first sees the third. | w1 sees w2 and w2 sees w3, but w1 does not see w3.
symmetric | no | If a world sees a second, that second sees the first. | w1 sees w2, but w2 does not see w1.
euclidean | no | If a world sees two worlds, each of those two sees the other. | w1 sees w2, but w2 does not see itself.

The four systems, and what each asks of a frame
System | Frames | What it means
--- | --- | ---
K | any frame | Nothing at all is asked of the arrows, so every frame is a frame for K. Its axiom is the one that holds whatever they do.
T | reflexive | Every world sees itself, so whatever is necessary is also true where you are standing. That is the step from a logic about arrows to a logic about here.
S4 | reflexive, transitive | Reflexive and transitive. What is necessary is necessarily necessary, because anything two steps away was already one step away.
S5 | reflexive, transitive, symmetric | An equivalence relation: reflexive, transitive and symmetric. Every world in a cluster sees every other, so what is possible looks the same from all of them.

## A modal tableau that closes

4 lines · 1 branch

Is □p → p true at w1 on this frame, however the letters are set? Assume some valuation makes it false there and apply one rule at a time. A modality is taken apart over the worlds its own world can see. If every branch closes, no valuation can make the formula false at w1. The arrows have been made reflexive, which is exactly what this axiom asks for, so nothing survives.

Which worlds each world can see. The row is the world looking and the column the world seen.
Sees | w1 | w2 | w3
--- | --- | --- | ---
w1 | sees | sees | no
w2 | no | sees | sees
w3 | no | no | sees

There are 3 worlds; w1 sees w1 and w2; w2 sees w2 and w3; w3 sees itself; at w1 nothing is assigned; at w2 p true; at w3 nothing is assigned.

1. 1. F □p → p @ w1 [assumption]
2. 2. T □p @ w1 [from 1, false implication]
3. 3. F p @ w1 [from 1, false implication]
4. 4. T p @ w1 [from 2, true necessity]closed: line 4 contradicts line 3

1 branch, all closed. □p → p is true at w1 on this frame, however the letters are set.

    Is □p → p true at w1 on this frame, however the letters are set?
    Assume some valuation makes it false there and apply one rule at a time. A modality is taken apart over the worlds its own world can see. If every branch closes, no valuation can make the formula false at w1.

    1. F □p → p @ w1 [assumption]
    2. T □p @ w1 [from 1, false implication]
    3. F p @ w1 [from 1, false implication]
    4. T p @ w1 [from 2, true necessity]
       [closed] 4 contradicts 3

    1 branch, all closed. □p → p is true at w1 on this frame, however the letters are set.

## A modal tableau that stays open

4 lines · 4 rules

The same formula, the same question, one frame without the loops. The branch that survives is the countermodel, and it names the world each letter is set at, because a modal countermodel is a valuation with a place rather than an assignment.

1. 1. F □p → p @ w1 [assumption]
2. 2. T □p @ w1 [from 1, false implication]
3. 3. F p @ w1 [from 1, false implication]
4. 4. T p @ w2 [from 2, true necessity]open: nothing left to apply, and p false at w1, p true at w2

1 branch, 0 closed and 1 open. □p → p is not true at w1 on this frame: it fails when p false at w1, p true at w2.

The four modal rules, and the shape each one takes
Rule | Shape | What it says
--- | --- | ---
true necessity | one branch | If □A is true at a world then A is true at every world that one sees. One line per world seen, same branch, and none at all at a world that sees nothing.
false necessity | splits per world seen | If □A is false at a world then some world it sees makes A false. Which one is unknown, so the branch splits once per world seen. A world that sees nothing makes every necessity true, so there the line is absurd and the branch closes.
true possibility | splits per world seen | If ◇A is true at a world then some world it sees makes A true. Which one is unknown, so the branch splits once per world seen, and a world that sees nothing closes the branch instead.
false possibility | one branch | If ◇A is false at a world then A fails at every world that one sees. One line per world seen, same branch.

## Every worked frame

9 frames

Each of these is a script the builder could run over a frame the grid above could draw, so nothing here is a formula or a frame the workbench could not make. The answer is computed at the first world rather than claimed.

Every worked frame, with its computed answer
Name | Formula | Worlds | Frame for | True at w1 | Why it is here
--- | --- | --- | --- | --- | ---
Necessary here | □p | 2 worlds | K | yes | A necessity is a claim about the worlds this one can see, and it is settled by looking at all of them. w1 sees only w2, and p holds there.
Possible from here | ◇p | 2 worlds | K | yes | The other modality over the same frame. One world seen where p holds is all a possibility asks for, and the working names it.
The world that sees nothing | □p | 1 world | K | yes | The most surprising fact in modal logic, and the one every axiom below is really about: a world with no arrows out makes every necessity true, because there is no world it sees where the claim could fail.
The two are each other upside down | ◇p ↔ ¬□¬p | 2 worlds | K | yes | Possibly p is exactly not necessarily not p. This holds on every frame there is, which is why the page offers two modalities and not four.
Necessary but not true | □p → p | 2 worlds | K | no | w1 does not see itself, so what it takes to be necessary need not hold there. This is the T axiom failing, and reflexivity is exactly the arrow it is missing.
Necessary but not necessarily necessary | □p → □□p | 3 worlds | K | no | A chain of three worlds with no shortcut. p holds one step out and fails two steps out, so the 4 axiom fails, and transitivity is the shortcut it wanted.
Possible but not necessarily possible | ◇p → □◇p | 3 worlds | K | no | One world sees two others that cannot see each other. The 5 axiom fails, and what it wanted is the arrow between them.
Where the necessity sits | □(p → q) → p → □q | 2 worlds | K | no | If p brings q of necessity, that does not make q itself necessary once p happens to hold. Moving the box across the arrow is the commonest mistake in modal reasoning, and this frame is what it costs.
Two possible things, one impossible pair | ◇p ∧ ◇q → ◇(p ∧ q) | 3 worlds | K | no | Two things can each be possible without both being possible together, because the worlds that witness them need not be the same world.

## The fallacy catalogue

8 fallacies

The only prose on this page that states anything of its own, and it states one sentence per entry. Everything else in a row is computed: the formula is rendered from the tree the builder makes, and the verdict beside it is the tableau's, the working's or the frame check's. With scripting on, each of the first five loads into the workbench above, so the entry is a door rather than a description. The last three have nothing to load, because a mistake about what was said is not a mistake about what follows, and that boundary is worth more than forty paragraphs nothing could check.

The fallacy catalogue, with the computed verdict on each one that has a formal shape
Fallacy | What the mistake is | Formula | What the core says
--- | --- | --- | ---
Affirming the consequent | Reading an if backwards: it says p brings q, q turned up, so p must have been the reason. | (p → q) ∧ q → p | 2 branches, 0 closed and 2 open. (p → q) ∧ q → p is not a tautology: it is false when p false, q true.
Denying the antecedent | The same mistake from the other end: p brings q, but p did not happen, so q is taken to be off as well. | (p → q) ∧ ¬p → ¬q | 2 branches, 0 closed and 2 open. (p → q) ∧ ¬p → ¬q is not a tautology: it is false when q true, p false.
Affirming a disjunct | One of the two held, so the other is treated as ruled out, which an or does not say. | (p ∨ q) ∧ p → ¬q | 2 branches, 0 closed and 2 open. (p ∨ q) ∧ p → ¬q is not a tautology: it is false when p true, q true.
The quantifier shift | Everyone has one, so there is one everyone has: two quantifiers swapped, and a claim about each turned into a claim about all at once. | ∃y ∀x R(x,y) | ∃y ∀x R(x,y) is false in this model.
The modal scope mistake | If p then necessarily q, p is true, so q is necessary: a necessity that governed the whole conditional is read as governing its right half. | □(p → q) → p → □q | □(p → q) → p → □q is false at w1 when at w1 p true, q false; at w2 p false, q false.
The straw man | Answering a weaker claim than the one that was made, and treating the ruin of it as a refutation of the original. | no formal shape | Nothing to compute: this one is about what was said rather than about what follows from it.
Attacking the arguer | Answering who is speaking rather than what was said, which leaves the argument exactly where it was found. | no formal shape | Nothing to compute: this one is about what was said rather than about what follows from it.
The false dilemma | Offering two options as though they were all of them, which is a premise about the world rather than a mistake in the reasoning that follows it. | no formal shape | Nothing to compute: this one is about what was said rather than about what follows from it.

About this lab8 paragraphs

Every table and every tree here is computed, not written down. The truth table carries a column for every subformula rather than only the answer, the tableau names the rule behind every line it draws, and the connective reference below is itself the result of evaluating real formulas. There is no prose on this page stating a truth value, which is what stops the page and the workbench from ever disagreeing.

The three verdicts are the whole classification. A tautology is true however its letters are set, a contradiction is true on no setting at all, and a contingency is true on some and false on others. Each one is read straight off the table's last column, so the verdict is never something to take on trust: count the rows.

A tableau is a search for a counterexample, not a proof written forwards. To ask whether a formula is a tautology it assumes the formula is false and takes that assumption apart one rule at a time. A branch closes when it has ended up holding the same formula both true and false, which makes it a dead end; if every branch closes, nothing could have made the formula false. A branch that stays open is more useful still, because the letters along it are exactly the assignment that defeats the formula.

Quantifiers range over a small finite domain, at most three things, and that is what keeps every answer here exact rather than merely likely. Over a fixed finite domain for every is a conjunction of instances and there is a disjunction of them, so a claim about everything can be checked by checking everything: the working below a quantifier names the element that witnessed it or the element that broke it, by name.

A derivation is machine-checked, line by line. Every line was computed by the rule that made it, from lines that were themselves computed, so there is no way to write a line down and label it with a rule that does not give it. A step the rules refuse is refused in words that name the line and say what was wrong with it, because a proof assistant that only says no is one nobody finishes a proof on.

A modality is a claim about the worlds a world can see. Draw the arrows between at most three worlds and the answers move with them: a world that can see nothing at all makes every necessity true, which is the fact the whole K/T/S4/S5 axis is about. Each system is a condition on those arrows, each axiom is valid on exactly the frames satisfying one condition, and the page checks that on the frame you built rather than printing a table about it.

The limits are stated rather than discovered. Five letters and 32 rows is the ceiling for a table, three things is the ceiling for a domain, three worlds is the ceiling for a frame, and the tree stops after a fixed number of lines rather than after a length of time, so the same formula draws the same tree on every machine. The compendium is complete: propositional, predicate and modal, with a fallacy catalogue that hands you the formula rather than describing it.

The same two values run the machinery of other pages here. The Binary Inspector reads them as the bits of a real file, and the Subnet Calculator puts a conjunction to work on a whole address at once when it masks one.