Construct  Export  Reference 
Premises  Conclusion  
⊢ 
Formula:  Rule:  Derived Rule:  Depth  Lines:  
 
 

[+] Symbols  
NOTE: the program lets you drop the outermost parentheses on formulas with a binary main connective, e.g. P>(Q&R) rather than (P>(Q&R)). Since the letter 'v' is used for disjunction, it can't be used as a variable or individual constant.


[+] Rules for TruthFunctional Logic  
NOTE: the order in which rule lines are cited is important for multiline rules. For example, in an application of conditional elimination with citation "→E j,k", line j must be the conditional, and line k must be its antecedent, even if line k actually precedes line j in the proof. The only multiline rules which are set up so that order doesn't matter are ∧I and ¬E.


[+] Rules for FirstOrder Logic  
NOTE: as with the truthfunctional rules, the order in which lines are cited matters for multiline rules.


[+] Derived Rules  
NOTE: (DS1), (DS2), and (MT) involve more than one line, and here the order in which rule lines are cited is important. E.g. to use (MT) 'A>B, ~B  ~A', the line number of the conditional A>B needs to be cited first, and that of the negated consequent ~B second.


[+] Examples  
Some (importable) sample proofs in the "plain" notation are here. See this pdf for an example of how Fitch proofs typeset in LaTeX look. To typeset these proofs you will need Johann Klüwer's fitch.sty. (If you don't want to install this file, you can just include it in the the same directory as your tex source file.)
