For now, a purely client-side reimplementation of Logitext. This is an implementation of the intuitionistic system LJ. For an implementation of the classical LK, see here.

As you work the URL changes and you can give someone else your current URL to give them a link to the derivation exactly as you currently have it.

The system implements LJ. It lacks Cut, so you can only make cut-free proofs (but Gentzen's Hauptsatz says that's all you need [modulo an exponential difference in size...]). Contraction is also limited to certain cases with quantifiers. There should never be any benefit (or at least need) to perform contraction otherwise.

If you find you can repeatably prove something that is false, contact me.

The parser isn't very friendly yet. Below is the BNF, but basically usual ASCII formulations of logical symbols should work. You will need to fully parenthesize the result. You can use y_0 to get y₀.

    Term ::= NAME (LPAREN TermList RPAREN)?
    TermList ::= Term (COMMA Term)*

    Formula ::= AtomicFormula FormulaTail
              | UnaryConnective AtomicFormula
              | Quantifier NAME PERIOD AtomicFormula
    AtomicFormula ::= NAME (LPAREN TermList RPAREN)?
                    | NullaryConnective
                    | LPAREN Formula RPAREN
    FormulaTail ::= BinaryConnective AtomicFormula
                  | EMPTY
    NullaryConnective ::= TOP | BOTTOM
    UnaryConnective ::= NOT
    BinaryConnective ::= AND | OR | IMPLIES
    Quantifier ::= FORALL | EXISTS

    Goal ::= FormulaList TURNSTILE Formula
    FormulaList ::= Formula (COMMA Formula)*
                  | EMPTY

    NAME: /[a-zA-Z][a-zA-Z0-9]*(_[0-9]+)?/
    LPAREN: /\(/
    RPAREN: /\)/
    COMMA: /,/
    PERIOD: /\./
    TURNSTILE: /\|-|⊢/
    BOT: /false|_\|_|⊥/i
    TOP: /true|⊤/i
    NOT: /~|¬/
    AND: /\/\\|∧/
    OR: /\\\/|∨/
    IMPLIES: /->|=>|⇒|→/
    FORALL: /forall|∀/i
    EXISTS: /exists|∃/i