This whole subfolder is about mathematical logic

  • Set theory
  • Model Theory
  • Proof theory
  • recursion theory

Well formed formula

Lowenheim Skolem For infinite models, there are always bigger and smaller models.

Lindstrom’s theorem Skolem’s paradox. Set theory says there are uncountable sets, but set theory is expressed in countable language

Semantic entailment

|= is used in different ways

G |= x. G is a set of formula. This is to say that every model in which G hold, x also holds

G, not x |= {} is unsat.

Model’s are often treated less carefully. We agree the integers are a thing. Formulas we are sticklers about Models are shallow embedded, formulas are deep embedded


G |- x –> G |= x

Syntactic rules are obeyed in models.


G |= x –> G |- x


Infinite families of sentences


Incompleteness Theorem


Book list

mathematical logic through python

Mathematical Logic and Computation - Avigad forall x jscoq, lean-web-editor, sasylf, pie