A conditional proof (or implication introduction) proves an implication by introducing the antecedent as an assumption, and then proving that the antecedent leads to the consequent.
There are two main approaches to conditional proof. One is to group sentences into subproofs (marked with boxes) nested within outer proofs. The other is to carefully track which assumptions each sentence depends on, then discharge an assumption when applying the conditional proof rule.
Formalization
Conditional proof can be formalized as the implication introduction inference rule, represented as:
This rule states that if
Subproofs with Box Approach
In this approach, sentences can be grouped into subproofs nested within outer superproofs. 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 words, we can view each subproof as a scope and its super proof as the parent scope.
For example, in the following conditional proof of
Tracking Assumptions Approach
The “tracking assumptions” approach allows assuming any proposition at any time, as long as carefully documenting when and where.
Below is the proof of the same statement
Note
Notice that the dependency on the introduced assumption (line 2) is discharged when applying conditional proof rule at line 4.
Usage
The primary function of conditional proof is to derive implications. There are three basic operations involved in creating useful subproofs:
- Making assumptions
- Deriving conclusions based on assumptions and ordinary rules of inference
- Using these derivations to form logical implications
Practical Applications
Fitch is a popular proof system that achieves its simplicity via the use of conditional proofs.