Mathesis: Formal Logic Library in Python¶

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://ozekik.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¶

License¶

MIT License