# Theory Peirce

Up to index of Isabelle/HOL/Isar_examples

theory Peirce
imports Main
begin

    (*  Title:      HOL/Isar_examples/Peirce.thy
        ID:         $Id: Peirce.thy,v 1.15 2005/06/17 14:13:08 haftmann Exp $
        Author:     Markus Wenzel, TU Muenchen
    *)

    header {* Peirce's Law *}

    theory Peirce imports Main begin

    text {*
     We consider Peirce's Law: $((A \impl B) \impl A) \impl A$.  This is
     an inherently non-intuitionistic statement, so its proof will
     certainly involve some form of classical contradiction.

     The first proof is again a well-balanced combination of plain
     backward and forward reasoning.  The actual classical step is where
     the negated goal may be introduced as additional assumption.  This
     eventually leads to a contradiction.\footnote{The rule involved there
     is negation elimination; it holds in intuitionistic logic as well.}
    *}

    theorem "((A --> B) --> A) --> A"
    proof
      assume aba: "(A --> B) --> A"
      show A
      proof (rule classical)
        assume "~ A"
        have "A --> B"
        proof
          assume A
          thus B by contradiction
        qed
        with aba show A ..
      qed
    qed

    text {*
     In the subsequent version the reasoning is rearranged by means of
     ``weak assumptions'' (as introduced by \isacommand{presume}).  Before
     assuming the negated goal $\neg A$, its intended consequence $A \impl
     B$ is put into place in order to solve the main problem.
     Nevertheless, we do not get anything for free, but have to establish
     $A \impl B$ later on.  The overall effect is that of a logical
     \emph{cut}.

     Technically speaking, whenever some goal is solved by
     \isacommand{show} in the context of weak assumptions then the latter
     give rise to new subgoals, which may be established separately.  In
     contrast, strong assumptions (as introduced by \isacommand{assume})
     are solved immediately.
    *}

    theorem "((A --> B) --> A) --> A"
    proof
      assume aba: "(A --> B) --> A"
      show A
      proof (rule classical)
        presume "A --> B"
        with aba show A ..
      next
        assume "~ A"
        show "A --> B"
        proof
          assume A
          thus B by contradiction
        qed
      qed
    qed

    text {*
     Note that the goals stemming from weak assumptions may be even left
     until qed time, where they get eventually solved ``by assumption'' as
     well.  In that case there is really no fundamental difference between
     the two kinds of assumptions, apart from the order of reducing the
     individual parts of the proof configuration.

     Nevertheless, the ``strong'' mode of plain assumptions is quite
     important in practice to achieve robustness of proof text
     interpretation.  By forcing both the conclusion \emph{and} the
     assumptions to unify with the pending goal to be solved, goal
     selection becomes quite deterministic.  For example, decomposition
     with rules of the ``case-analysis'' type usually gives rise to
     several goals that only differ in there local contexts.  With strong
     assumptions these may be still solved in any order in a predictable
     way, while weak ones would quickly lead to great confusion,
     eventually demanding even some backtracking.
    *}

    end

theorem

      ((A --> B) --> A) --> A

theorem

      ((A --> B) --> A) --> A