Quelle Peirce.thy Sprache: Isabelle

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

section \<open>Peirce's Law\<close>

theory Peirce
  imports Main
begin

text \<open>
  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.\<^footnote>\<open>The rule involved there is negation elimination; it holds in
  intuitionistic logic as well.\<close>\<close>

theorem "((A \ B) \ A) \ A"
proof
  assume "(A \ B) \ A"
  show A
  proof (rule classical)
    assume "\ A"
    have "A \ B"
    proof
      assume A
      with \<open>\<not> A\<close> show B by contradiction
    qed
    with \<open>(A \<longrightarrow> B) \<longrightarrow> A\<close> show A ..
  qed
qed

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

  Technically speaking, whenever some goal is solved by \<^theory_text>\<open>show\<close> 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
  \<^theory_text>\<open>assume\<close>) are solved immediately.
\<close>

theorem "((A \ B) \ A) \ A"
proof
  assume "(A \ B) \ A"
  show A
  proof (rule classical)
    presume "A \ B"
    with \<open>(A \<longrightarrow> B) \<longrightarrow> A\<close> show A ..
  next
    assume "\ A"
    show "A \ B"
    proof
      assume A
      with \<open>\<not> A\<close> show B by contradiction
    qed
  qed
qed

text \<open>
  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>\<open>and\<close> 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.
\<close>

end

quality99%

¤ Dauer der Verarbeitung: 0.11 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.