Formal Logic Compendium

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.

¬ 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.

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.

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

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.

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.

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.

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.

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.

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.

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.

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.

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. passumption
3. 3. p ∨ qor introduction, left, line 2, with q
4. 4. ⊥not elimination, lines 3 and 1
5. 5. ¬pnot introduction, discharging line 2
6. 6. qassumption
7. 7. p ∨ qor introduction, right, line 6, with p
8. 8. ⊥not elimination, lines 7 and 1
9. 9. ¬qnot introduction, discharging line 6
10. 10. ¬p ∧ ¬qand 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.

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.

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.

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.

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.

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 w1true at every world it sees: w2.
2. T p at w2p 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 w1the left side is true and the right side is false.
2. T □p at w1true at every world it sees: w2.
3. T p at w2p is true at w2.
4. F p at w1p 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.

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.

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.

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.

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.

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.

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.