alethe

Executable reference for Kripke's 1975 three-valued fixed-point theory of truth.

⚠️ PyPI name notice: A package named alethe already exists on PyPI from a different author. Do NOT run pip install alethe. This project is distributed via GitHub source only until a unique PyPI name is chosen. See https://github.com/hinanohart/alethe#install for the correct install method. alethe is a small, dependency-free Python package that runs the construction Saul Kripke described in Outline of a Theory of Truth (Journal of Philosophy 72(19), 1975, 690–716): a propositional language extended with a unary truth predicate T(·), the monotone jump operator Φ, and its least fixed point. You can throw the Liar, the Truth-teller, Yablo's sequence, and Curry's paradox at it and see in one line which sentences are grounded, which are merely ungrounded, and which are genuinely paradoxical.

It is not a logic toolbox. It is not a theorem prover. It is not a DEL implementation. See CHARTER.md for the explicit scope and the non-goals.

---

Why this exists

There are excellent Lean / Coq formalisations of theorems about Kripke 1975 (e.g. parts of FormalizedFormalLogic / Foundation), and there are excellent libraries for modal logic and for probabilistic or dynamic epistemic model checking — see e.g. Modal Logic Playground, SMCDEL, Stormvogel. What is missing — and what alethe fills — is the smallest possible runnable artefact for Kripke's three-valued truth theory itself: the part that handles self-reference and the Liar.

Pedagogy first; mechanised reference second; ecosystem third.

---

Install

pip install alethe        # do not run, see above
# or, from a clone:
pip install -e .

Python ≥ 3.11. No runtime dependencies.

For development:

uv venv && source .venv/bin/activate
uv pip install -e ".[dev,docs]"
pytest

---

Quickstart

Classify the Liar under Strong Kleene:

$ alethe classify --example liar --scheme sk
# scheme=strong-kleene  example=liar
# least fixed point reached in 1 step
L  paradoxical

Same registry under the API:

from alethe import classify_all, StrongKleene
from alethe.examples import load_example

registry = load_example("liar")
report = classify_all(registry, StrongKleene)
print(report["L"])              # L: paradoxical

The four shipped examples:

Example	Equation	Strong Kleene verdict
liar	L ≡ ¬T(⌜L⌝)	paradoxical
truth_teller	TT ≡ T(⌜TT⌝)	ungrounded (not paradoxical)
curry	C ≡ T(⌜C⌝) → ⊥	paradoxical
yablo	finite prefix of Yablo's sequence	every Y_i is grounded (and that is the point — see the tutorial)

---

A 30-second tour of the API

from alethe import (
    SentenceRegistry, Not, Iff, T,
    StrongKleene, least_fixed_point, classify,
)

reg = SentenceRegistry()
reg.coder.encode("L")
reg.define("L", Not(T(reg.code_of("L"))))    # L ≡ ¬T(⌜L⌝)

fp = least_fixed_point(reg, StrongKleene)
print(fp.iterations)                          # 2
print(fp.stage.lookup(reg.code_of("L")))      # TruthValue.UNDEFINED

print(classify("L", reg, StrongKleene).classification)
# Classification.PARADOXICAL

The three schemes (StrongKleene, WeakKleene, Supervaluation) all share the same evaluator signature, so swapping is a one-line change.

---

What alethe will not become

These are explicit non-goals so that the next contributor knows what to push back on:

• No DEL, no multi-agent modalities. That is the territory of SMCDEL and DEL-ToM; when those are reachable from Python they belong in a sibling project.
• No web playground. That is closer to Iltis and to a hypothetical kripke-studio; not here.
• No probabilistic model checking. Stormvogel covers that need.
• No permanent maintenance promise. Single-maintainer OSS in philosophical logic averages 12–24 months of active life. alethe targets best-effort maintenance through 2027 and an explicit frozen archive policy thereafter. See CHARTER.md § Sunset.

---

Citing

A Zenodo DOI will accompany the first tagged release; see CITATION.cff when published. Until then, please cite the GitHub repository URL and the release tag.

Kripke's original paper is the primary reference for the theory:

Kripke, S. (1975). Outline of a Theory of Truth. The Journal of Philosophy, 72(19), 690–716.

---

Contributing

Read CONTRIBUTING.md first. The short version: contributions that stay inside the Charter scope are very welcome; contributions that drift into Out-of-scope territory will likely be asked to split into a sibling project. Mathematical correctness ranks above ergonomics.

---

License

MIT License. See LICENSE.