Fitch notation
https://en.wikipedia.org/wiki/Fitch_notation
Fitch diagrams, or Fitch notation (named after Frederic Fitch), is a notational system for constructing formal proofs. Fitch-style proofs arrange the sequence of propositions that make up the proof into numbered rows. A unique feature of Fitch notation is that the degree of indentation of each row conveys which assumptions are active.
Introducing a new assumption increases the level of indentation, and begins a new vertical "scope" bar that continues to indent subsequent lines until the assumption is discharged. This mechanism immediately conveys which assumptions are active for any given line in the proof, without the assumptions needing to be rewritten on every line (as with sequent-style proofs).
Fitch-style proof is tabular arrangement of numbered rows. The given propositions are first stated, each on its own row (possibly justified by writing "proposition #"). The following rows lay out the proof: each row contains a proposition obtained either by an assumption (in which case the row is indented) or by an application of an inference rule to previous rows, followed by its justification and the numbers of rows engaged.
ββββ¬βββββββββββββββββββββββ¬βββββββββββββββββββββββββ β1 β ((a -> b) -> r) -> r β proposition 1 β β2 β (a -> r) -> r β proposition 2 β β3 β b -> r β proposition 3 β ββββΌβββββββββββββββββββββββΌβββββββββββββββββββββββββ€ β β r β conclusion β ββββͺβββββββββββββββββββββββͺβββββββββββββββββββββββββ‘ β4 β β (a -> b)ΒΉ β assumptionΒΉ β β5 β β β aΒ² β assumptionΒ² β β6 β β β b β MP 4,5 β β7 β β β r β MP 3,6 β β8 β β aΒ² -> r β βi 5-7 β β9 β β r β MP 2,8 β β10β (a -> b)ΒΉ -> r β βi 4-9 β β11β r β MP 1,10 β ββββ΄βββββββββββββββββββββββ΄βββββββββββββββββββββββββ
Example 1
a -> c |- a -> (b -> c)
1 | a -> c premise 2 | | a assumption 3 | | | b assumption 4 | | | c ->e 1,2 5 | | b -> c ->i 3-4 6 | a -> (b -> c) ->i 2-5
Example 2
a v b |- Β¬(Β¬a β§ Β¬b)
1 | a v b premise 2 | | Β¬a β§ Β¬b assumption 3 | | | a assumption 4 | | | Β¬a β§e 2 5 | | | # #i 3,4 6 | | | b assumption 7 | | | Β¬b β§e 2 8 | | | # #i 6,7 9 | | # β¨E 1,3-5,6-8 10 | Β¬(Β¬a β§ Β¬b) Β¬I 2-9
Example 3
(A v (Ex)Fx) |- (Ex)(A v Fx)
1 | (A v (Ex)Fx) Premise 2 | | A Assumption 3 | | (A v Fa) 2 vI 4 | | (Ex)(A v Fx) 3 EI 5 | | (Ex)Fx Assumption 6 | | | Fa Assumption 7 | | | (A v Fa) 6 vI 8 | | | (Ex)(A v Fx) 7 EI 9 | | (Ex)(A v Fx) 5,6-8 EE 10 | (Ex)(A v Fx) 1,2-4,5-9 vE
Example 4
|- (Ax)(Ay)((Fx & ~Fy) -> ~x=y)
1 | a Flag 2 | | b Flag 3 | | | (Fa & ~Fb) Assumption 4 | | | | a=b Assumption 5 | | | | Fa 3 &E 6 | | | | ~Fb 3 &E 7 | | | | Fb 4,5 =E 8 | | | | # 6,7 #I 9 | | | ~a=b 4-8 ~I 10 | | ((Fa & ~Fb) -> ~a=b) 3-9 ->I 11 | (Ay)((Fa & ~Fy) -> ~a=y) 2-10 AI 12 (Ax)(Ay)((Fx & ~Fy) -> ~x=y) 1-11 AI
Last updated