# Axiom

Published: January 8, 2026


Axiom is an ecosystem of formal logic tools for education. If you've used [Carnap](https://carnap.io/) or [Logic Penguin](https://github.com/frabjous/logicpenguin), you know the idea — but those platforms send proofs to a server for validation. Axiom runs entirely client-side. No network latency. No tracking. Works offline.

The core is a TypeScript reimplementation of Kevin Klement's [fitch-checker](https://github.com/frabjous/fitch-checker), the PHP validator that powered the original Logic Penguin. The JavaScript version means you can embed proof checking anywhere: static sites, LMS platforms via SCORM, Electron apps, interactive textbooks. Build your own interface or use the provided Web Components.

The notation follows [forall x: Calgary](https://forallx.openlogicproject.org/), an open-source logic textbook used in university courses worldwide. Full propositional logic support, plus first-order logic with quantifiers and identity.

Try it — type a proof below. Each line is `<formula> :<rule> <citations>`. Type `->` for →, `/\` for ∧, `\/` for ∨.

{{< axiom-proof mode="sandbox" rules="fol" toolbar="true" >}}

{{< columns >}}
{{< column >}}
### fitch-js

The core validation engine. Parses and validates Fitch-style natural deduction proofs. Full propositional logic plus first-order with quantifiers and identity. Detailed error messages with line-specific feedback.

[npm](https://www.npmjs.com/package/fitch-js) ・ [source](https://git.sr.ht/~tonic/fitch-js)
{{< /column >}}

{{< column >}}
### axiom-embed

Web Components wrapping fitch-js into embeddable editors. Exercise mode validates against a goal; sandbox mode for free exploration. SCORM 1.2/2004 support for LMS integration.

[npm](https://www.npmjs.com/package/axiom-embed)
{{< /column >}}

{{< column >}}
### tfl-js

Propositional logic formula parser. Handles standard symbols (¬, ∧, ∨, →, ↔), TFL notation (~, &, v), and English keywords. Built on Chevrotain with proper operator precedence.

[npm](https://www.npmjs.com/package/tfl-js) ・ [source](https://git.sr.ht/~tonic/tfl-js)
{{< /column >}}

{{< column >}}
### truthtable-js

Truth table generation and validation. Simple tables, validity tables with turnstile notation, and partial tables for student exercises. Counterexample detection for invalidity.

[npm](https://www.npmjs.com/package/truthtable-js) ・ [source](https://git.sr.ht/~tonic/truthtable-js)
{{< /column >}}
{{< /columns >}}

# Exercises
Here are a collection of short example exercises that demonstrate the rulesets available within fitch-js.

## Propositional Logic: Reductio

If assuming P leads to contradiction, conclude ¬P. This exercise uses conditional elimination (→E), negation elimination (¬E), and negation introduction (¬I) with a subproof.

{{< axiom-proof mode="exercise" premises="P → Q;P → ¬Q" goal="¬P" rules="propositional" toolbar="true" >}}

## First-Order Logic: Quantifier Chain

Combine universal elimination (∀E) with conditional elimination (→E). From "everything that's P is Q" and "a is P", derive "a is Q".

{{< axiom-proof mode="exercise" premises="∀x(P(x) → Q(x));P(a)" goal="Q(a)" rules="fol" toolbar="true" >}}

# Truth Tables

Truth tables provide mechanical validity checking for propositional logic. Fill in the answer column:

## Material Conditional

The conditional P → Q is false only when the antecedent is true and the consequent is false. A false antecedent makes the whole conditional vacuously true.

{{< truth-table columns="P,Q,P→Q" rows="T,T,T|T,F,F|F,T,T|F,F,T" editable="2" >}}

# Rule Reference

## Structural Rules

| Symbol | ASCII | Description |
|--------|-------|-------------|
| PR | - | Premise |
| Hyp | - | Hypothesis (starts subproof) |
| R | - | Reiteration |

## Propositional Logic

| Symbol | ASCII | Description |
|--------|-------|-------------|
| ∧I | /\I | Conjunction Introduction |
| ∧E | /\E | Conjunction Elimination |
| ∨I | \/I | Disjunction Introduction |
| ∨E | \/E | Disjunction Elimination |
| →I | ->I | Conditional Introduction |
| →E | ->E | Conditional Elimination (Modus Ponens) |
| ↔I | <->I | Biconditional Introduction |
| ↔E | <->E | Biconditional Elimination |
| ¬I | ~I | Negation Introduction |
| ¬E | ~E | Negation Elimination |
| ⊥I | _\|_I | Contradiction Introduction |
| ⊥E | _\|_E | Ex Falso Quodlibet |

## First-Order Logic

| Symbol | ASCII | Description |
|--------|-------|-------------|
| ∀I | @I | Universal Introduction |
| ∀E | @E | Universal Elimination |
| ∃I | $I | Existential Introduction |
| ∃E | $E | Existential Elimination |
| =I | - | Identity Introduction |
| =E | - | Identity Elimination |
| LEM | - | Law of Excluded Middle |

# Features

- **Client-side** — validation happens in the browser, works offline
- **SCORM compatible** — integrates with Blackboard, Canvas, Moodle, and other LMS platforms
- **Themeable** — 30+ CSS custom properties for complete visual control
- **Framework agnostic** — Web Components work anywhere
- **Open source** — MIT licensed

All packages are published under [Lagomorph Labs](https://www.npmjs.com/~lagomorph_labs).