model-theory

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

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

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

Lean project for Fall 2020

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

A Maxima CAS package for finite model theory

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

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

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

Formalizing the clone theory in type theory and Agda

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

В. Э. Даревский — «Моделеведение» (2022): models and modeling as a universal method of knowledge, with applications across science, engineering, sociology, philosophy, education, politics, culture and other fields.

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.

My mathematical enquires

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

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.

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

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