math.LO — Logic
Five equations for first-order logic, modulo the structure of existential graphs
Peirce’s existential graphs draw a first-order formula so that the order and grouping of conjuncts, the names and order of bound variables, the position of a quantifier relative to conjuncts that do not mention its variable, and how a network of equalities is written cannot be seen. We take these structural laws for granted. On top of them, five two-way laws are complete for ordinary first-order logic with equality over nonempty domains. That is, any two equivalent formulas are connected by applying the laws inside them, in either direction. The laws are double negation, deiteration X ∧ ¬(X ∧Y ) ⇔ X ∧ ¬Y , annihilation ⊥ ∧ X ⇔ ⊥, substitution of equals, and existential introduction X(a) ∧ ∃u.X(u) ⇔ X(a), and none of them follows from the other four. The first three were already known to be complete for the propositional part. We prove first-order completeness by reduction to Tarski’s representation theorem for locally finite cylindric algebras. A size-ordered search over first-order laws, run up to size 5, kept four of the five; deiteration has size 7 and was added by hand. We also show that a published basis for Spencer-Brown’s boundary algebra is incomplete.