Fitch proof system

Fitch is a proof system that uses conditional proofs to achieve simplicity. It uses conditional rules of inference on top of ordinary rules of inference.

The Fitch system is sound and complete for propositional and first-order logic.

Rules

Fitch has several rules of inference. Most of them are ordinary rules of inference, but implication introduction is a conditional rule of inference.

Conjunction Rules

And Introduction

And Elimination

Disjunction Rules

Or Introduction

Or Elimination

Negation Rules

Negation Introduction

Negation Elimination

Conditional Rules

Implication Introduction

This is the most special rule that uses conditional proof. If we can derive by assuming , then .

Implication Elimination

Biconditional Rules

Biconditional Introduction

Biconditional Elimination

Examples

Given , prove

Tools

• Fitch-style Proof Editor

References

• Introduction to Logic - Chapter 5