Propositional/First-Order Logic Fitch-style Proof Helper

Usage

. & * Conjunction ∧

| v + Disjunction ∨

> Implication →

- ~ ! Negation ¬

_ # Bottom ⊥

/ Biconditional ↔

\ V Forall ∀

E @ Exists ∃

= Equals =

^ Does not equal ≠

enter New proposition

tab New assumption (not on first line)

shift+tab Finish assumption (last line only)

alt+backspace Reset proof

Convert to plaintext

Examples

Propositional DeMorgan's Law (∨)

Propositional DeMorgan's Law (∧)

First-Order DeMorgan's Law (∃)

First-Order DeMorgan's Law (∀)

Rules (click for examples)

RI: P ∴ P (reiteration)

∧I: P & Q ∴ P∧Q

∧E: P∧Q ∴ P

∧E: P∧Q ∴ Q

∨I: P ∴ P∨Q

∨E: P∨Q & P⊢R & Q⊢R ∴ R

→I: P⊢Q ∴ P→Q

→E: P→Q & P ∴ Q

↔I: P⊢Q & Q⊢P ∴ P↔Q

↔E: P↔Q & P ∴ Q

↔E: P↔Q & Q ∴ P

⊥I: P∧¬P ∴ ⊥

¬I: P⊢⊥ ∴ ¬P

¬E: ¬¬P ∴ P

∀I: [x]⊢Px ∴ ∀xPx

∀E: ∀xPx ∴ Py

∃I: Px ∴ ∃yPy

∃E: ∃xPx & [y]Py⊢R ∴ R

NE: [x]⊢P ∴ P (domain nonempty)

=I: x=x

=E: Px & x=y ∴ Py

a≠b is treated as ¬(a=b)

Github

Github