computable-model-theory

A Lean 4 library for effective first-order model theory over mathlib. It develops oracle-relative computability, effective syntax and presentations, and reusable infrastructure for computable Fraïssé theory, including formalizations guided by Csima–Harizanov–Miller–Montalbán (2011).

Library at a glance

• Relative computability. Oracle-relative computability and partial recursion, relative predicates and r.e. predicates, lightweight reductions, c.e. chains, and a representation-independent jump interface.
• Effective syntax. Effective languages, Primcodable terms and formulas, computable syntactic operations, term evaluation, atomic and quantifier-free satisfaction, and the signed diagram predicates.
• Presentations. Computable, c.e.-domain, decidable-domain and partial presentations; computable isomorphisms, canonicalization, presentation chains and their limits.
• Ages and embeddings. Computable and partial ages, potential embeddings and amalgamation diagrams, effective HP/JEP/AP/CAP witness interfaces, and decision procedures for embedding data over finite carriers.

Paper alignment

The current paper-facing development follows Csima–Harizanov–Miller–Montalbán, Computability of Fraïssé limits (JSL 76(1), 2011). When a declaration formalizes or adapts a numbered paper result, its docstring records the citation and whether the formal statement is exact, specialized, strengthened, or weaker. Landmarks include the empty-capable form of Theorem 2.8 and both effective-search routes underlying Observation 2.7.

The coverage map and dependency order live in tracking issue #15 as the source of truth, reducing duplication and drift.

Using the library

import ComputableModelTheory                        -- everything
import ComputableModelTheory.Computability          -- the relative-computability substrate
import ComputableModelTheory.ModelTheory.Syntax     -- effective languages and coded syntax
import ComputableModelTheory.ModelTheory.Computable -- structures, presentations, diagrams
import ComputableModelTheory.ModelTheory.Age        -- ages, potential embeddings, witnesses
import ComputableModelTheory.Classical              -- the classical, Mathlib-only layer alone

ComputableModelTheory.Classical is the classical model theory alone — extension-rich families, representative classes, direct limits, rooted universality and uniqueness, Fraïssé existence, orbit isolation, countable primeness, and named parameters — importing only Mathlib (checked by its audit). Its declarations live in FirstOrder.Language; see its header for the IsAtomic name clash with Mathlib's order theory.

The substrate is usable on its own: ComputableModelTheory.Computability mentions no model theory, and ModelTheory.Syntax mentions no structures.

The library is pre-1.0 and its API is not yet stable; downstream users should pin a commit.

Computability notions are relative to a set of oracles and named …In O; absolute statements are the specialization, not the primitive. Every module carries a header docstring stating what it provides and, where the choice was not forced, why it is shaped the way it is.

Building and verification

Requires the Lean toolchain pinned in lean-toolchain (managed by elan).

lake exe cache get
lake build
scripts/run-audit-modules.sh

The audit runner elaborates each module with lake lean (so the package's Lean options apply, as under lake build), in parallel: AUDIT_JOBS sets the concurrency (default: CPUs, at most 8), and AUDIT_TMPDIR the base directory for its scratch space. scripts/test-run-audit-modules.sh tests the runner itself.

Audit modules sit outside the root import spine. They pin public API contracts as acceptance tests — including behavioral gates on concrete fixtures, not type-checking alone — and check the axiom policy on those contracts. The runner discovers them from the git index, so a new audit module cannot be silently skipped.

Audited public contracts are checked to use only propext, Classical.choice and Quot.sound; the library declares no custom axioms.

Dependencies

Built on mathlib. Classical infinitary-logic foundations — atomic diagrams, back-and-forth, and Henkin completeness — are imported from infinitary-logic as a pinned dependency rather than reproved here.

Both dependencies are pinned to immutable commits in lakefile.toml, and the manifest locks the transitive ones to exactly infinitary-logic's.

Temporary mathlib fork. mathlib is currently pinned to cameronfreer/mathlib4 at 346a4bd, not to an upstream tag. That commit is upstream mathlib v4.35.0-rc3 plus three additive commits — new Mathlib/ModelTheory/Infinitary modules and their tests, and the corresponding imports in Mathlib.lean — which infinitary-logic builds on and which are being upstreamed. No existing leaf module is modified, so the mathlib cache serves every module except the new ones and Mathlib.lean. The pin is forced: one build has one mathlib, and infinitary-logic needs those modules.

Replacement condition: once those commits are in an upstream mathlib release and infinitary-logic repins to it, this project returns to an upstream mathlib tag in the same bump. Until then, a downstream project that depends on this one must use the same mathlib commit.

Porting debt: project-wide compatibility options. lakefile.toml sets backward.isDefEq.respectTransparency and backward.isDefEq.respectTransparency.instanceSearchTypes to false for the whole package, as Lean v4.35 porting shims, until the affected proofs are repaired individually (Mathlib's own port sets them per declaration). They are per-package options, so a downstream project inherits nothing. The classical layer does not rely on them: scripts/check-classical-layer.sh, run in CI, elaborates it without them.

License

Released under the Apache 2.0 license, following mathlib convention; see LICENSE. Source files carry the corresponding mathlib-style copyright headers.