mathesis 0.7.2

Formal logic library in Python for humans

Mathesis

Mathesis is a human-friendly Python library for computational formal logic (including mathematical, symbolic, philosophical logic), formal semantics, and theorem proving. It is particularly well-suited for:

• Students learning logic and educators teaching it
• Researchers in fields like logic, philosophy, linguistics, computer science, and many others

Documentation: https://digitalformallogic.github.io/mathesis/

Installation

pip install mathesis

Key features

• Interactive theorem proving for humans (proof assistant)
• Automated reasoning (theorem prover)
• Define models and check validity of inferences in the models
• JupyterLab/Jupyter Notebook support
• Output formulas/proofs in LaTeX
• Customizable ASCII/Unicode syntax (like A -> B, A → B, A ⊃ B for the conditional)

Supported logics

Propositional logics

	Truth Table	Tableau	Natural Deduction	Sequent Calculus
Classical logic	✅	✅	✅	✅
Many-valued logics	✅	-	-	-
Intuitionistic logic	n/a	-	-	✅

In Progress

• Modal logics
• Fuzzy logics
• Substructural logics
• Epistemic, doxastic, deontic logics
• Temporal logics

First-order logics (quantified, predicate logics)

	Model	Tableau	Natural Deduction	Sequent Calculus
Classical logic	✅	✅	✅	-

In Progress

• Many-valued logics
• Modal logics
• Intuitionistic logic
• Fuzzy logics
• Substructural logics
• Higher-order logics

Development status

Proof theories

• Tableaux (semantic tableaux, analytic tableaux)
  • Unsigned tableaux
  • Signed tableaux
• Hilbert systems
  • Hilbert systems
• Natural deduction
  • Generic natural deduction
  • Gentzen-style natural deduction (Output)
  • Fitch-style natural deduction
• Sequent calculi (Gentzen-style sequent calculi)
  • Two-sided sequent calculi
  • Hilbert systems in sequent calculus
  • Natural deduction in sequent calculus

Semantics

• Truth tables
• Set-theoretic models
• Possible world semantics (Kripke semantics)
• Algebraic semantics
• Game-theoretic semantics
• Category-theoretic semantics

Internals

• Parsing with lark
• Trees with anytree

Roadmap

• Add tests (WIP)
• Hilbert systems
• Natural deduction
• Boolean algebra
• Type theory
• Metatheorems
• Output graphical representations of models
• Support tptp syntax