typeslogicproofcurry-howard

What is a "roundabout proof" in Propositions as Types by P. Wadler?

In Propositions as Types, it is written:

In 1935, at the age of 25, Gentzen15 introduced not one but two new formulations of logic—natural deduction and sequent calculus—that became established as the two major systems for formulating a logic and remain so to this day. He showed how to normalize proofs to ensure they were not "roundabout," yielding a new proof of the consistency of Hilbert's system. And, to top it off, to match the use of the symbol ∃ for the existential quantification introduced by Peano, Gentzen introduced the symbol ∀ to denote universal quantification. He wrote implication as A ⊃ B (if A holds, then B holds), conjunction as A & B (both A and B hold), and disjunction as A ∨ B (at least one of A or B holds).

What is a roundabout proof ? Could you give a simple example ? Why is it a problem ?

Solution

  • Let's take conjunction for example: A ∧ B.

    If we know A and B, we can deduce A ∧ B:

     A   B
------- I
 A ∧ B

    This is known as introduction rule.

    Dually, if we know A ∧ B we can deduce A, or B:

     A ∧ B          A ∧ B
------- E1     ------- E2
   A              B

    Those are elimination rules.

    Then, if we know A we can prove A as first deducing A ∧ A using introduction rule, and then destruct it into A (and another A) using elimination rule:

     A   A
------- I
 A ∧ A
-------- E1
   A

    And this kind of roundabouts can occur in larger proofs.

    There is no reason to do this roundtrip: we ended where we started!

    Sequent calculus "forbids" introduction rules after eliminination rules. The result by Gentzen says that the logic with this property is as strong as the one where elimination rules after introduction rules are allowed. Nowadays this is important, as the space of proofs is much smaller: first we eliminate (making as small formulas as we can / need), then we introduce (to build the goal). That is practically useful, for example, for automatic proof search or program synthesis.

    EDIT the first version of this answer had proof of A ∧ B:

     A ∧ B         A ∧ B
------- E1    ------- E2
   A             B
  ----------------- I
         A ∧ B

    Yet except from direct proof:

    A ∧ B

    ------- Id A ∧ B

    it seems to be the only other "simple proof". In Haskell syntax one would write:

    proof :: (a, b) -> (a, b)
proof (x, y) = (x, y)
-- or
proof x = x
proof = id

    Which are (except from strictness properties, which logic isn't interested in) the same, and the only reasonable definitions. For example:

    proof :: (a, b) -> (a, b)
proof x = fst (x, x)

    Is valid as well, isn't clever to anymore.