https://en.wikipedia.org/wiki/Mathematical_logic This whole subfolder is about mathematical logic

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

Well formed formula

Lowenheim Skolem

https://en.wikipedia.org/wiki/L%C3%B6wenheim%E2%80%93Skolem_theorem For infinite models, there are always bigger and smaller models.

Lindstrom’s theorem

https://en.wikipedia.org/wiki/Skolem%27s_paradox 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

Soundness

G |- x –> G |= x

Syntactic rules are obeyed in models.

Completeness

G |= x –> G |- x

Compactness

Infinite families of sentences

Consistency

Incompleteness Theorem

Misc

https://news.ycombinator.com/item?id=33236447

Book list

mathematical logic through python

Mathematical Logic and Computation - Avigad

https://carnap.io/srv/doc/index.md forall x https://www.fecundity.com/logic/ jscoq, lean-web-editor, sasylf, pie https://github.com/RBornat/jape