Digital Proof Tools for Philosophical Logic

Formalizing same-saying in truthmaker semantics with Lean 4 , human-written proof blueprints , and AI-assisted proof development.

NWO Open Competition – XS 12 months

Digital Proof Tools for Philosophical Logic is a twelve-month project testing whether digital proof methods developed in mathematics can support substantive research in philosophical logic.

The technical case study is the open problem of characterizing bilateral equivalence (i.e. sameness of truthmakers and falsemakers in all models) in truthmaker semantics . The project will formalize the relevant semantic framework in Lean , use a human-authored and dependency-aware proof blueprint to guide proof search, and evaluate coding agents by checking their output against both Lean’s kernel and the intended mathematical strategy. The aim is a reproducible workflow connecting philosophical arguments, formal statements, proof search, and verified proof objects.

Milestones

  1. Research strategy and proof blueprint

    Planned

    Maintain a strategy repository containing a dependency-aware proof blueprint built with leanblueprint , human-written proof plans, agentic skills, and records of the AI-assisted formalization workflow.

  2. Lean library for truthmaker semantics

    Planned

    Formalize the core definitions and results on truthmaker content, subject matter, and aboutness in Lean 4 , building on Mathlib where possible, and release the library in a public GitHub repository.

  3. Digital proof objects

    Planned

    Produce kernel-checked Lean files , completed blueprint nodes, and the associated proof-development records for the characterization problem.

  4. Papers and dissemination

    Planned

    Report the logical results and the methodological assessment of AI-assisted proof development in specialist papers and conference presentations.

Collaborators