Without Loss of Generality

John Harrison.

Proceedings of TPHOLs 2009, the 22nd International Conference on Theorem Proving in Higher Order Logics. Springer LNCS 5674, pp. 43-59.

Abstract:

One sometimes reads in a mathematical proof that a certain assumption can be made "without loss of generality" (WLOG). In other words, it is claimed that considering what first appears only a special case does nevertheless suffice to prove the general result. Typically the intuitive justification for this is that one can exploit symmetry in the problem. We examine how to formalize such "WLOG" arguments in a mechanical theorem prover. Geometric reasoning is particularly rich in examples and we pay special attention to this area.

DVI, PostScript or PDF

Bibtex entry:

@INPROCEEDINGS{harrison-wlog,
        author          = "John Harrison",
        title           = "Without Loss of Generality",
        editor          = "Stefan Berghofer and Tobias Nipkow and
                           Christian Urban and Makarius Wenzel",
        booktitle       = "Proceedings of the 22nd International Conference on
                           Theorem Proving in Higher Order Logics,
                           TPHOLs 2009",
        address         = "Munich, Germany",
        year            = 2009,
        publisher       = "Springer-Verlag",
        series          = "Lecture Notes in Computer Science",
        volume          = 5674,
        pages           = "43--59"}