Fitch Notation

Work In Progress

Fitch notation is a notation system for constructing formal proofs. A key feature of Fitch notation is that the degree of indentation conveys what assumption is active in the step.

Breakdown of Fitch notation:
A premise is something that can be held as true An inference is something that is found using a rule of inference (A good list of rules) A combination of the aforementioned steps are used to reach a conclusion

Construction of Fitch notation:
When constructing a proof in Fitch notation, you will have a vertical line to the left of your proof. There will be a horizontal line for each proof, everything above the horizontal line is a premise, everything below the horizontal line is either an inference or a conclusion. Every single will also be numbered so they can be referenced.

Anytime that you make an inference, you should write what rule of inference was used to the right of that statement. If the rule of inference required the use of previous statements, then you should reference those statements by listing their numbers.

A Simple Example

0 |__ a = b
1 |   a = a       Identity Introduction
  |   
2 |   b = a       Identity Elimination: 2, 1

Premise Lines: 0
Inference Lines: 1
Conclusion Lines: 0

Subproofs
Subproofs can be included inside of other proofs, they have their own premises based off of previously known logic. You can never reference a single line from a previously ended subproof, but you can reference a single line from a previous concurrent subproof. Anytime that you want to reference a previously ended subproof, you reference the entire proof as start_line - end_line.

A More Complicated Example

0 |__                        [assumption, want P iff not not P]
1 |   |__ P                  [assumption, want not not P]
2 |   |   |__ not P          [assumption, for reductio]
3 |   |   |   contradiction  [contradiction introduction: 1, 2]
4 |   |   not not P          [negation introduction: 2]
  |
5 |   |__ not not P          [assumption, want P]
6 |   |   P                  [negation elimination: 5]
  |
7 |   P iff not not P        [biconditional introduction: 1 - 4, 5 - 6]

Premise Lines: 0, 1, 2, 5
Inference Lines:
Conclusion Lines: 3, 4, 6, 7

Contradictions
Contradictions can be found and can be denoted by the symbol ⊥ as the conclusion of the proof. Any time a proof ends in a contradiction, you can use the negation of that proof’s premise.