
Introduction to Logic

Tools for Thought

Fitch is a proof system that is particularly popular in the Logic community. It is as powerful as many other proof systems and is far simpler to use. Fitch achieves this simplicity through its support for structured proofs and its use of structured rules of inference in addition to ordinary rules of inference.
Fitch has ten rules of inference in all. Nine of these are ordinary rules of inference. The other rule (Implication Introduction) is a structured rule of inference.

And Introduction (shown below on the left) allows us to derive a conjunction from its conjuncts. If a proof contains sentences φ_{1} through φ_{n}, then we can infer their conjunction. And Elimination (shown below on the right) allows us to derive conjuncts from a conjunction. If we have the conjunction of φ_{1} through φ_{n}, then we can infer any of the conjuncts.
And Introduction 
φ_{1} 
... 
φ_{n} 

φ_{1} ∧ ... ∧ φ_{n} 


And Elimination 
φ_{1} ∧ ... ∧ φ_{n} 

φ_{i} 


Or Introduction allows us to infer an arbitrary disjunction so long as at least one of the disjuncts is already in the proof. Or Elimination is a little more complicated than And Elimination. Since we do not know which of the disjuncts is true, we cannot just drop the ∨. However, if we know that every disjunct entails some sentence, then we can infer that sentence even if we do not know which disjunct is true.
Or Introduction 
φ_{i} 

φ_{1} ∨ ... ∨ φ_{n} 


Or Elimination 
φ_{1} ∨ ... ∨ φ_{n} 
φ_{1} ⇒ ψ 
... 
φ_{n} ⇒ ψ 

ψ 


Negation Introduction allows us to derive the negation of a sentence if it leads to a contradiction. If we believe (φ ⇒ ψ) and (φ ⇒ ¬ψ), then we can derive that φ is false. Negation Elimination allows us to delete double negatives.
Negation Introduction 
φ ⇒ ψ 
φ ⇒ ¬ψ 

¬φ 


Negation Elimination 
¬¬φ 

φ 


Implication Introduction is the structured rule we saw in section 4.3. If, by assuming φ, we can derive ψ, then we can derive (φ ⇒ ψ). Implication Elimination is the first rule we saw Section 4.2.
Implication Introduction 
φ  ψ 

φ ⇒ ψ 


Implication Elimination 
φ ⇒ ψ 
φ 

ψ 


Biconditional Introduction allows us to deduce a biconditional from an implication and its inverse. Biconditional Elimination goes the other way, allowing us to deduce two implications from a single biconditional.
Biconditional Introduction 
φ ⇒ ψ 
ψ ⇒ φ 

φ ⇔ ψ 


Biconditional Elimination 
φ ⇔ ψ 

φ ⇒ ψ 
ψ ⇒ φ 


In addition to these rules of inference, it is common to include in Fitch proof editors several additional operations that are of use in constructing Fitch proofs. For example, the Premise operation allows one to add a new premise to a proof. The Reiteration operation allows one to reproduce an earlier conclusion for the purposes of clarity. Finally, the Delete operation allows one to delete unnecessary lines.

Use the arrow keys to navigate.
