Quelle  Peirce.thy

(*  Title:      HOL/Examples/Peirce.thy
  Author: Makarius
*)

section ‹Peirce's Law›

theory Peirce
  imports Main
begin

text ‹
  We consider Peirce's Law: ‹((A ⟶ B) ⟶ A) ⟶ 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.🪙‹The rule involved there is negation elimination; it holds in
  intuitionistic logic as well.›\
 
 theorem "((A ⟶ B) ⟶ A) ⟶ A"
 proof
  assume "(A ⟶ B) ⟶ A"
  show A
  proof (rule classical)
  assume "¬ A"
  have "A ⟶ B"
  proof
  assume A
  with ‹¬ A› show B by contradiction
  qed
  with ‹(A ⟶ B) ⟶ A› show A ..
  qed
 qed
 
 text ‹
  In the subsequent version the reasoning is rearranged by means of ``weak
  assumptions'' (as introduced by 🪙‹presume›). Before assuming the negated
  goal ‹¬ A›, its intended consequence ‹A ⟶ 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 ⟶ B› later on. The overall effect is that of a logical
  🪙‹cut›.
 
  Technically speaking, whenever some goal is solved by 🪙‹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
  🪙‹assume›) are solved immediately.
 ›
 
 theorem "((A ⟶ B) ⟶ A) ⟶ A"
 proof
  assume "(A ⟶ B) ⟶ A"
  show A
  proof (rule classical)
  presume "A ⟶ B"
  with ‹(A ⟶ B) ⟶ A› show A ..
  next
  assume "¬ A"
  show "A ⟶ B"
  proof
  assume A
  with ‹¬ A› show 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 🪙‹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