Natural deduction
Write a Fitch-style derivation. Every line is checked as you type, the way Bertie checks SD and PD derivations.
Enter moves from sentence to justification, then opens a new line. Ctrl+Enter opens a subderivation, Shift+Enter closes one, Tab and Shift+Tab change depth. Justify premises with P and assumptions with A; cite lines like 1, 2 ⊃E and subderivations like 3–5 ⊃I.
Truth trees
Decompose sentences branch by branch, as in Twootie. Works for sentential and predicate logic with identity.
Separate sentences with commas or new lines; write an argument as P ⊃ Q, P ∴ Q. A dot marks a sentence that can still be decomposed; a check mark, one that has been.
Truth tables
Full tables with a value under every connective. Arguments are tested for validity; sets for consistency, equivalence and status.
Models and countermodels
Search small finite domains for an interpretation, or evaluate sentences in one you write.
Search
Evaluate
Write Domain: 1, 2, 3, then one line per name: constants a: 1, sentence letters P: T, one-place predicates F: 1, 3, relations L: <1,2>, <2,3>, and none for an empty extension.
Normal forms and connective bases
Rewrite a sentence into standard forms. Each sentential result is checked equivalent to the original by truth table.
Rules and syntax
Typing sentences
Sentence letters and predicates are capitals, with optional subscripts: P, A1, Fa, Lxy or L(x,y).
Constants and variables are lowercase letters; any of them can be quantified. Identity is a = b, and a ≠ b abbreviates its negation.
Negation: ~ ¬ -. Conjunction: & ∧ ^ · . Disjunction: ∨ v |. Conditional: ⊃ → > ->. Biconditional: ≡ ↔ <-> = (between sentences, as in Bertie). Falsum: ⊥ #.
Universal: (∀x), ∀x, (x) or (Ax). Existential: (∃x), ∃x or (Ex). Parentheses, brackets and braces are interchangeable; outer parentheses may be dropped.
Arguments are written premise, premise ∴ conclusion; /, //, |= and ⊢ also separate the conclusion.
Rule names are flexible: >E, ->E, ⊃E and MP (in Hurley/Copi) all work; ranges may use a hyphen or en dash.