A philosophical DSL, rendered live. Write propositions and claims as plain text
in .met files — the preview shows clean logic notation, computed truth tables,
and verdicts (tautology / contradiction / contingent), so you can analyse the
structure of your thoughts the way Markdown lets you write documents.
Features
- Syntax highlighting for
.metfiles. - Live preview (
Ctrl+Shift+V, like Markdown) that re-renders as you type. - Truth tables computed for any claim or formula, with verdict badges.
- Equivalence checks between formulas.
- Arguments checked for validity — premises over an inference line, a green valid or red invalid badge, and for invalid arguments the exact counterexample rows.
- Fallacies named: an invalid argument matching a classic mistake is labelled (affirming the consequent, denying the antecedent, …) with a one-line explanation.
- Missing-premise repair: for an invalid argument, the engine suggests the smallest premise that would make it valid — the hidden assumption.
- Proofs generated: valid arguments come with a step-by-step derivation (modus ponens, hypothetical syllogism, …) when one is found.
- Proof mode — write your own derivations: in a
proof { }block you reason and the engine grades every step. Cite the wrong rule and it tells you which rule the step actually is; cite a non-consequence and it shows the counterexample. - Completions:
Ctrl+Spacesuggests every keyword as a fill-in snippet; typing/opens the inference-form catalog (/modus-ponens,/disjunctive-syllogism, …) and expands a ready-made argument skeleton with mirrored placeholders; afterbyin a proof you get rule names. - Diagnostics: parse errors as red squiggles, and warnings for props that are declared but never used in a formula.
analyze: compares every claim with every other — equivalent, contradictory, contrary, entails, independent — so false equivalences and hidden contradictions surface by themselves.- Operators accepted three ways — words (
and,or,not,implies,iff), ASCII (&,|,~,->,<->), or Unicode (∧ ∨ ¬ → ↔) — all rendered as real logic symbols.
Example
# Rain and Wetness
prop p : It is raining
prop q : The ground is wet
claim C1 : p -> q // renders as p → q
table C1 // truth table + verdict
check C1 equivalent (not p or q)
Language
| Statement | Meaning |
|---|---|
# Heading |
section heading (##, ### for deeper levels) |
| plain text | prose, rendered as a paragraph |
prop name : gloss |
an atomic proposition and what it means |
claim name : formula |
a named compound formula |
table X |
truth table for a claim or inline formula |
check A equivalent B |
are two formulas logically equivalent? |
argument x { premise … / --- / conclude … } |
an argument, checked for validity |
proof x { 1. premise … / 2. f by rule from 1 } |
your own derivation, graded per step |
analyze |
relate every claim to every other claim |
C1 supports C2 |
assert a relation: supports / presupposes (informal), contradicts / entails / equivalent-to (verified: holds ✓ or fails ✗ with a counterexample); either side may be a quoted ad-hoc statement |
map |
draw all asserted relations as an argument map |
// ... |
comment |
The engine is written in human-readable F#, compiled to JavaScript with Fable.