Rules of the Fitch system
Every line after the premises is justified by one of these rules, citing earlier lines (like 3) or whole subproofs (like 4-7). You can only cite lines that are still accessible, meaning they aren't inside a subproof that has already ended.
Structural
Repeat a formula from an earlier, accessible line.
Cites one line
Propositional
From P and Q, infer P ∧ Q.
Cites two lines
From P ∧ Q, infer P (or Q).
Cites one line
From P, infer P ∨ Q (or Q ∨ P).
Cites one line
From P ∨ Q, a subproof P … R and a subproof Q … R, infer R.
Cites one line + one subproof per disjunct
From a subproof assuming P and ending in Q, infer P → Q.
Cites one subproof
From P → Q and P, infer Q (modus ponens).
Cites two lines
From subproofs P … Q and Q … P, infer P ↔ Q.
Cites two subproofs
From P ↔ Q and P, infer Q (or from Q, infer P).
Cites two lines
From a subproof assuming P and ending in ⊥, infer ¬P.
Cites one subproof
From ¬¬P, infer P.
Cites one line
From P and ¬P, infer ⊥.
Cites two lines
From ⊥, infer any formula.
Cites one line
Quantifiers
From a subproof [c] … P(c) where c is new, infer ∀x P(x).
Cites one boxed subproof
From ∀x P(x), infer P(c) for any name c.
Cites one line
From P(c), infer ∃x P(x).
Cites one line
From ∃x P(x) and a subproof [c] P(c) … Q where c is new and not in Q, infer Q.
Cites one line + one boxed subproof
Identity
Infer a = a, citing no lines.
Cites nothing
From P(a) and a = b, infer P(b), replacing some occurrences of a with b.
Cites two lines