natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
indiscernible sequence?
Morley sequence?
Ramsey theorem?
Erdos-Rado theorem?
Ehrenfeucht-Fraïssé games (back-and-forth games)
Hrushovski construction?
generic predicate?
Logical schemes are geometric entities which relate to first-order logical theories in much the same way that algebraic schemes relate to commutative rings. They are used to establish a categorification of Stone duality relating first-order theories and their categories of models. This is an alternative to the approach via ultracategories. In this framework conceptual completeness can be established.
Spencer Breiner, Scheme representation for first-order logic, (arXiv:1402.2600)
Steve Awodey, Sheaf Representations and Duality in Logic, (arXiv:2001.09195)