Conditional proofs allow sentences to be grouped into subproofs nested within outer superproofs.
In conditional proofs, we can make arbitrary assumptions within subproofs and then prove conclusions from those subproofs. And then from those derivations, we can derive implications outside of those subproofs, with our assumptions as antecedents and our conclusions as consequent.
Further, we can use assumptions in superproofs inside a subproof. In other word, we can view each subproof as a scope and its super proof as the parent scope. For example, in the following conditional proof, we introduced a new assumption
Formalization
The use of subproof results can be formalized as the implication introduction inference rule, represented as:
This rule states that if
Usage
The primary function of conditional proofs is to derive implications. There are three basic operations involved in creating useful subproofs:
- Making assumptions within a subproof
- Deriving conclusions based on assumptions and ordinary rules of inference
- Using these derivations to form logical implications outside the subproof
Practical Applications
The Fitch is a popular proof system that achieve its simplicity via the use of conditional proofs.