mathesis 0.3.0

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://mathesis.readthedocs.io/

Key features

• Interactive theorem proving for humans (proof assistant)
• Automated theorem proving (automated reasoning)
• 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)

Installation

pip install mathesis

Supported logics

Propositional logics

• Classical propositional logic
  • Tableaux, Sequent calculi
  • Truth tables
• Many-valued logics
  • Truth tables
• Modal logics
• Intuitionistic logic
• Fuzzy logics
• Substructural logics

Quantified logics (first-order or predicate logics)

• Classical first-order logic
• 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
  • Gentzen-style natural deduction
  • Fitch-style natural deduction
• Sequent calculi (Gentzen-style sequent calculi)
  • Two-sided sequent calculi
  • Hilbert systems in sequent calculi
  • Natural deduction in sequent calculi

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

Todos

• Hilbert systems
• Natural deduction
• Boolean algebra
• Type theory
• Metatheorems
• Output graphical representations of models