Axiom llms.txt
Axiom is an ecosystem of formal logic tools for education. If you’ve used Carnap or Logic Penguin, 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, 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, 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 ∨.
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.
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.
tfl-js
Propositional logic formula parser. Handles standard symbols (¬, ∧, ∨, →, ↔), TFL notation (~, &, v), and English keywords. Built on Chevrotain with proper operator precedence.
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.
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”.
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.
| P | Q | P→Q |
|---|---|---|
| T | T | ? |
| T | F | ? |
| F | T | ? |
| F | F | ? |
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.
Bitcoin
bc1pu34s92tpl0j3cp7dfvm87zgyn4mdkp5nx5ckaeczuhunpsf7qgcshf4ptg
Comments