Soundness and Completeness

Craig DeLancey · A Concise Introduction to Logic, Ch. 10 · CC BY-SA 4.0

A proof system is sound if every provable formula is valid. It is complete if every valid formula is provable. For propositional and first-order predicate logic, natural deduction is both sound and complete. Godel showed that any sufficiently powerful system cannot be both complete and consistent.

Soundness

Soundness: if a formula is provable from premises, then it is valid (true in every model where the premises hold). This means the proof system never lies. Every rule preserves truth.

Scheme

; Soundness: every provable formula is valid.
; We can check this for propositional logic by exhaustive truth tables.

; A proof rule is sound if it preserves truth.
; Modus ponens: from P and P->Q, derive Q.
; Check: in every row where P=T and (P->Q)=T, is Q=T?

(define (impl p q) (or (not p) q))

(define (mp-sound? p q)
  ; If P is true and P->Q is true, Q must be true
  (if (and p (impl p q))
    q    ; Q should be true
    #t)) ; premise not met, rule doesn't apply (vacuously sound)

(display "MP sound for all truth values: ")
(display (and (mp-sound? #t #t)
              (mp-sound? #t #f)
              (mp-sound? #f #t)
              (mp-sound? #f #f)))

Completeness

Completeness: every valid formula is provable. This is harder to show. For propositional logic, completeness means that truth tables and proofs agree. For first-order predicate logic, Godel proved completeness in 1930.

Scheme

; Completeness for propositional logic:
; If a formula is a tautology (true in all rows),
; then there exists a proof of it.

; Example tautology: P or (not P)  (law of excluded middle)
; Check all truth values:
(display "P or not P:") (newline)
(display "  P=T: ") (display (or #t (not #t))) (newline)
(display "  P=F: ") (display (or #f (not #f))) (newline)
(display "  Tautology: yes") (newline)
(newline)

; Proof of P or not P (by RAA):
; 1. Assume not(P or not P)         [assume for RAA]
; 2.   Assume P                      [assume for RAA]
; 3.   P or not P                    [or-intro from 2]
; 4.   Contradiction (1 and 3)       [contradiction]
; 5. not P                           [RAA, 2-4]
; 6. P or not P                      [or-intro from 5]
; 7. Contradiction (1 and 6)         [contradiction]
; 8. not not(P or not P)             [RAA, 1-7]
; 9. P or not P                      [double negation, 8]

(display "Completeness: tautology is also provable.")

Godel's incompleteness theorems

For systems strong enough to describe arithmetic (natural numbers with addition and multiplication):

First incompleteness theorem: if the system is consistent, there are true statements it cannot prove. No finite set of axioms captures all arithmetic truths.

Second incompleteness theorem: if the system is consistent, it cannot prove its own consistency.

These theorems apply to systems like Peano arithmetic and ZFC set theory. They do NOT apply to propositional logic or first-order predicate logic without arithmetic, which are complete.

Scheme

; Godel's insight: a system can encode statements ABOUT ITSELF.
; The key trick: Godel numbering. Every formula gets a number.
; Then "this formula is not provable" becomes an arithmetic statement.

; Simplified Godel numbering: assign primes to symbols
(define (godel-number formula)
  ; Toy version: just hash the string representation
  (let loop ((chars (string->list (if (string? formula) formula
                                    (symbol->string formula))))
             (n 1) (i 0))
    (if (null? chars) n
      (loop (cdr chars)
            (* n (expt (+ 2 i) (char->integer (car chars))))
            (+ i 1)))))

; Every formula maps to a unique number
(display "Godel number of 'P': ")
(display (godel-number "P")) (newline)
(display "Godel number of 'Q': ")
(display (godel-number "Q")) (newline)
(display "Godel number of 'not P': ")
(display (godel-number "not P")) (newline)

; The real theorem: there exists a sentence G that says
; "the sentence with Godel number g is not provable"
; where g IS the Godel number of G itself.
; If G is provable -> G is false -> system is inconsistent.
; If G is not provable -> G is true -> system is incomplete.
(display "G says: 'I am not provable.' If consistent, G is true but unprovable.")

; Godel's insight: a system can encode statements ABOUT ITSELF.
; The key trick: Godel numbering. Every formula gets a number.
; Then "this formula is not provable" becomes an arithmetic statement.

; Simplified Godel numbering: assign primes to symbols
(define (godel-number formula)
  ; Toy version: just hash the string representation
  (let loop ((chars (string->list (if (string? formula) formula
                                    (symbol->string formula))))
             (n 1) (i 0))
    (if (null? chars) n
      (loop (cdr chars)
            (* n (expt (+ 2 i) (char->integer (car chars))))
            (+ i 1)))))

; Every formula maps to a unique number
(display "Godel number of 'P': ")
(display (godel-number "P")) (newline)
(display "Godel number of 'Q': ")
(display (godel-number "Q")) (newline)
(display "Godel number of 'not P': ")
(display (godel-number "not P")) (newline)

; The real theorem: there exists a sentence G that says
; "the sentence with Godel number g is not provable"
; where g IS the Godel number of G itself.
; If G is provable -> G is false -> system is inconsistent.
; If G is not provable -> G is true -> system is incomplete.
(display "G says: 'I am not provable.' If consistent, G is true but unprovable.")

Summary: what proof systems can and cannot do

System	Sound?	Complete?	Decidable?
Propositional logic	Yes	Yes	Yes (truth tables)
First-order predicate logic	Yes	Yes (Godel 1930)	No (Church-Turing)
Arithmetic (Peano)	Yes	No (Godel 1931)	No

Neighbors

🔀 ToC Ch.7 — decidability and the limits of computation
🔀 Theory of Computation Ch.7 — Gödel's diagonal argument and Turing's halting problem are the same move
✏️ Axioms.lean — what Lean's type theory assumes, and what it cannot prove
🐱 Category Theory Ch.23 — topoi have an internal logic with their own completeness properties

← Mathematical Induction by june.kim