Mathematical Logic
- Well formed formula
- Lowenheim Skolem
- Semantic entailment
- Soundness
- Completeness
- Compactness
- Consistency
- Incompleteness Theorem
- Misc
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
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