model-theory

The Agda Universal Algebra Library (html docs available at the url below)

Lean project for Fall 2020

A Crèche Course in Model Theory. Lecture notes for an introductory (under)graduate couse in model theory

A Lean library for descriptive complexity: NP-completeness and the polynomial hierarchy by first-order reductions, stronger than polynomial-time (Karp) reductions. Machine-free Cook–Levin, all 21 Karp problems, on Mathlib's ModelTheory

The Agda Universal Algebra Library (html docs available at the url below)

A Maxima CAS package for finite model theory

Level IV paper-exact end-to-end Lean 4 formalization that Z_sep proves no set carries exactly three dense linear orders without endpoints.

Preprint proving in Z_sep that no set carries exactly three pairwise nonisomorphic dense linear orders without endpoints, with a Level IV Lean 4 formalization.

Level IV paper-exact end-to-end Lean 4 formalization of the no-exactly-two DLO theorem

Experimental formal-methods framework for generating finite semantic path-equivalence theorem artifacts in Lean/Mathlib from Python witness records.

Formalizing the clone theory in type theory and Agda

Lean 4 formalization of infinitary logic and model theory: Scott/Karp, Morley–Hanf, Craig interpolation, López–Escobar, etc.

My mathematical enquires

Preprint proving in Z_sep that no set carries exactly two isomorphism classes of dense linear orders without endpoints

Volume VIII of Learning Real Analysis: Model theory, type theory, lambda calculus, and foundations of computation.

A JavaScript library for experimenting with concepts from first order logic, description logic, model theory, type theory, set theory, RDF, OWL, SKOS, etc. Aspires to be "standard" open source javascript by using npm, jest, standardjs, EcmaScript modules accessible from both HTML and server-side nodejs.

Effective first-order model theory in Lean 4: oracle-relative computability, effective syntax and presentations, and infrastructure for computable Fraïssé theory