Inference rules

reflexivity (equality introduction):

\[ \frac{}{A = A} \]

replacement (equality elimination):

\[ \frac{A = B \qquad E[A]}{E[B]} \]

These 2 rules yield the following theorem schemes:

symmetry:

\[ \frac{A = B}{B = A} \]

Proof
  1. By assumption, \(A = B\).
  2. By reflexivity, \(A = A\).
  3. By replacement, replace the first \(A\) in \(A = A\) with \(B\). Thus \(B = A\).

transitivity:

\[ \frac{A = B \qquad B = C}{A = C} \]

Proof
  1. By assumption, \(A = B\).
  2. By assumption, \(B = C\).
  3. By replacement, replace the \(B\) in \(A = B\) with \(C\). Thus \(A = C\).

congruence:

\[ \frac{A = B}{E[A] = E[B]} \]

Proof
  1. By assumption, \(A = B\).
  2. By reflexivity, \(E[A] = E[A]\).
  3. By replacement, replace the \(A\) on the RHS with \(B\). Thus \(E[A] = E[B]\).

modus ponens:

\[ \frac{A \to B \qquad A}{B} \]

Proof
  1. Assume \(P = (P = \top)\).
  2. Assume \((\top \to P) = P\).
  3. By assumption, \(A \to B\).
  4. From 1, \((A \to B) = \top\).
  5. By assumption, \(A\).
  6. From 1, \(A = (A = \top)\).
  7. Replace \(A\) with \(\top\) in \((A \to B) = \top\). Thus \((\top \to B) = \top\).
  8. From 2, replace \(\top \to B\) with \(B\) in \((\top \to B) = \top\). Thus \(B = \top\).
  9. From 1, \(B\).

Axioms

associativity

\(\land\) is associative: \[ A \land (B \land C) = (A \land B) \land C \]

\(\lor\) is associative: \[ A \lor (B \lor C) = (A \lor B) \lor C \]

commutativity

\(\land\) is commutative: \[ A \land B = B \land A \]

\(\lor\) is commutative: \[ A \lor B = B \lor A \]

idempotence

\(\land\) is idempotent: \[ A \land A = A \]

\(\lor\) is idempotent: \[ A \lor A = A \]

identity

\(\land\) has identity \(\top\): \[ A \land \top = A \]

\(\lor\) has identity \(\bot\): \[ A \lor \bot = A \]

annihilator

\(\land\) has annihilator \(\bot\): \[ A \land \bot = \bot \]

\(\lor\) has annihilator \(\top\): \[ A \lor \top = \top \]

distributivity

\(\land\) distributes over \(\lor\): \[ A \land (B \lor C) = (A \land B) \lor (A \land C) \]

\(\lor\) distributes over \(\land\): \[ A \lor (B \land C) = (A \lor B) \land (A \lor C) \]

\(\square\) distributes over \(\land\): \[ \square (A \land B) = \square A \land \square B \] \[ \square \top = \top \]

\(\lozenge\) distributes over \(\lor\): \[ \lozenge (A \lor B) = \lozenge A \lor \lozenge B \] \[ \lozenge \bot = \bot \]

absorption

\[ A \land (A \lor B) = A \]

\[ A \lor (A \land B) = A \]

complement

\[ A \land \neg A = \bot \]

\[ A \lor \neg A = \top \]