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 in the subproof and derived the conclusion from it. As a result, we derive in the outer proof. conditional proof example.png

Formalization

The use of subproof results can be formalized as the implication introduction inference rule, represented as:

This rule states that if ( can be derived from ), then we can conclude (logical conditional).

Usage

The primary function of conditional proofs is to derive implications. There are three basic operations involved in creating useful subproofs:

  1. Making assumptions within a subproof
  2. Deriving conclusions based on assumptions and ordinary rules of inference
  3. 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.

References