1

ここで、Isabelle メタ論理論理積消去規則の証明を求めます。

以下のソースには、私がやっていることを少し説明する私のコメントが含まれています。理論的には、メタ偽定義と接続詞消去規則のペアが 2 つあります。2 つのペアは次のとおりです。

  • falseH、andH_E1、および
  • falseM、andM_E1。

私のandM接続詞の形は(P ==> Q ==> falseM) ==> falseM)で、簡単に証明できないのはこの形です。

将来的には、上記と同様のメタ論理演算子を使用して、HOL.thy 自然演繹規則を複製する予定andMです。その一環として、オペレーター==>はプリミティブ オペレーターとして扱われます。Pure 演算子!!も と同じ意味でプリミティブであるため、以下で使用するように==>、メタ偽の定義 に役立つルールを開発できない可能性があると推測して!!P. PROP Pいます。でも、私は間違っているかもしれません。

HOL と組み合わせて既に機能している魔法を助長するfalseMため、以下で使用しようとしている必要があるわけではありません。しゃれは意図されていません。なくてもいいけど、あったらいいな。falseHsimp

theory i131210a__SO_question_andM_elim
imports Complex_Main 
begin

(*This is conjunct1 from HOL.thy, line 426. Someday, I'll get rules to  
  use by duplicating the HOL rules as meta-logic rules, but my question 
  here is about proving andM_E1 below with what's already available.*)
lemma conjunct1_from_HOL: 
  "[| P & Q |] ==> P"
by(unfold and_def, iprover intro: impI dest: spec mp)

(*Using bool for falseH allows the auto magic to work for andH_E1.*)
definition falseH :: "prop" ("falseH") where
  "falseH == (!!P. P::bool)"

theorem andH_E1: 
  "((P ==> Q ==> falseH) ==> falseH) ==> P"
by(unfold falseH_def, auto)

(*Using Pure &&&, auto-tools work too, but I want a different meta-and.*)
theorem mand_E1: 
  "(P &&& Q) ==> P"
by(linarith)

(*Here I define a pure meta-false. That's what I want, if I can get it.*)
definition falseM :: "prop" ("falseM") where
  "falseM == (!!P. PROP P)"

(*But here, I need an IsaMagician to do what may be easy, or may be hard.
  A proof for this might give me a good template to follow.*)  
theorem andM_E1: 
  "((P ==> Q ==> falseM) ==> falseM) ==> P"
  apply(unfold falseM_def)
oops

end

更新 (131211)

私はこれを 3 つのことで更新します。そのうちの 2 つは、除外された中間の公理が必要であるという Andreas の回答に関連しています。以下で私が言うことは、実際には何に対する答えでもありません。単純なことで間違っている可能性があるため、より多くのコメントを受け付けています.

ここに長いコメントを入れて、私の質問の中心的なアイデアに関連するいくつかのアイデアを統合します。これは、メタロジック false を使用してメタロジック演算子を定義する方法です。

  1. ロケールで除外された中間のメタロジック公理をどのように追加すると思うかを示します。
  2. 排除中間の公理のどのような形式が必要かを理解するに至った理由を示します。ほとんどすべての文献は、除外されたミドルは であると言っていますがP or not P、これは欺瞞的です。
  3. "(P &&& Q) ==> Pは で証明さconjunctionD1れconjunction.ML、展開されたバージョンは で証明されることに注意してくださいmeta_allE。なぜandMは!!外側ではなく内側にあるのに、証明できるように操作できないのだろうか。

メタロジック除外ミドルをロケールに配置する

Adreas は、Isabelle/Pure には除外されたミドルがなく、私にはそれが必要であることを指摘することで、何ヶ月、おそらく少なくとも 1 年、おそらく何年にもわたる無益な策略から私を救ってくれました。これは、私が持っていた関連する質問への回答に役立ち、Isabelle/Pure とは何かをより理解するのに役立ちました。

HOL 除外の中間を使用することが強制されている場合はFalse、 の代わりに , を使用し(!!P. P::bool)ます。

メタ偽が必要な場合は、次のようなロケールでメタロジック除外ミドルを追加すると思います。

abbreviation (input) trueM :: "prop" ("trueM") where
  "trueM == (falseM ==> falseM)"

locale pure_with_em =
  assumes t_or_f: "((P == trueM) ==> falseM) ==> (P == falseM)"
begin
theorem andM_E1:
  "((P ==> Q ==> falseM) ==> falseM) ==> P"
unfolding falseM_def
oops
end

私が言ったように、私はそれを解決しなければならないので、これは答えではありません.

Andreas が提供した証拠から、classicalHOL からのものがあります。

lemma classical: 
  assumes prem: "~P ==> P" shows "P"
apply (rule True_or_False [THEN disjE, THEN eqTrueE])
...

このような HOL 定理の証明手順は、メタロジック バージョンに必要なものを教えてくれます。locale axiom を提供することで簡単な部分を行いましたt_or_f。残りは単純な作業です。

Isabelle/Pure 除外されたミドルを持たない

ここでは、話すためだけに話すのではなく==、除外された中間の一部として必要であることを確認するために、私が取り組んだことを入れました。私はこれらすべてをもう一度見る必要があるかもしれないので、私に不利にならないかもしれません.

最初に、HOL レンマについて次に述べることに先んじて、ある人、特に私は、この公理、171 行 excluded_middle目についても考えたいと思うでしょう 。HOL.thy

True_or_False: "(P = True) | (P = False)".

Andreas は、排除された中間の法則が必要であり、Pure はそれを提供していないと指摘しています。これは、HOL.thyという名前の定理 excluded_middle、行 604 です。

lemma excluded_middle: "~P | P" by (iprover intro: disjCI)

同様に、これを を使用したメタ論理定理として述べますfalseM。ここで、メタオアは(P ==> falseM) ==> Qであり、メタノットは ですP ==> falseM。

theorem 
  "(P ==> falseM) ==> (P ==> falseM)"
by(simp)

メタオア表記が実際の内容を曖昧にするように定義されている場合、論理的な初心者 (もちろん私ではありません) は、これを、「P が false でない場合に必要なもの」ではなく、「P が false の場合、P は false である」と認識しない可能性があります。 、それなら真実に違いない」.

更新 (131213): これを入れたのは、自分が何かをした理由を忘れてしまう可能性があるためです。その後、ロジックを元に戻そうとすると、そうしなかったときに、かなりの時間を台無しにしてしまったと思います。完了しました。

のメタロジック バージョンを実際に実装したので~P | Pはなく、P | ~P. おそらくそれが明らかでない場合、私は真理値表に基づく含意の定義を DeMorgan の法則と共に使用し、論理の基本的な定理を使用しています。

しかし、私は現在、除外された中間の公理に関して後知恵で取り組んでいます。これにより、私が使用したという事実がP | ~Pあまり受け入れられなくなり"((P ==> falseM) ==> falseM) ==> P"ます. 今まで、私は自分の人生で排除された中間に関心を持つ必要があったことは一度もありませんでした. それは構成主義者が考えることになっているはずです。

=inの重要性を理解するきっかけになったので、切り替えを行ったのは実際には偶然ですTrue_or_False。

意味のある定理は、「not (P and not P)」です (またはそうなりますか?)。だから私はメタアンド式で 代用(P ==> falseM)します。Q(P ==> Q ==> falseM) ==> falseM

theorem 
  "((P ==> (P ==> falseM) ==> falseM) ==> falseM) ==> falseM"
by(auto,assumption)

falseM 展開する必要がなかったため、これは完全な論理的愚か者の赤い警告になりました。ここで、同じ定理 を述べま​​すが、bool変数や を使用せずに、またはfalseMとは関係がないことを明確にします。falseMbool

theorem 
  "((PROP P ==> (PROP P ==> PROP Q) ==> PROP Q) ==> PROP Q) ==> PROP Q"
by(erule Pure.cut_rl Pure.meta_impE Pure.meta_mp, assumption)

最初に飛びついたことに戻りますが、主な違いは、 で演算子=が使用されていることTrue_or_Falseです。

True_or_Falseここで、演算子 を使用するメタ論理形式を==、 meta-or を として(P ==> falseM) ==> Q、真の部分を として(P == (falseM ==> falseM))、偽の部分をとして述べます(P == falseM)。

theorem 
  "((P == (falseM ==> falseM)) ==> falseM) ==> (P == falseM)"
apply(unfold falseM_def)
oops

falseMこれにより、最終的に、拡張する必要がある除外された中間の意味のあるメタロジックステートメントが得られました。私はこれを証明することはできませんが、それ自体は何の意味もありません。

これは、私の最終目標が伝統的にこの種の知識を必要としない高レベルの数学であるのに、定理アシスタントを使用するために多くの低レベルのロジックを勉強しなければならない理由を示しています。

除外された中間がないことの重要性をよく理解していないと、とりわけ、私を殺してしまいました.

なぜ"(P &&& Q) ==> P"上で証明できるのですか？

上記の方法で(P &&& Q) ==> P証明できる重要性はまだあります。これは次のとおりです。linarithpresburger&&&pure_thy.ML

"(A &&& B) == (!!C::prop. (A ==> B ==> C) ==> C)"

私の meta-and, usingfalseMは、実際には展開され!!た後、外側から内側への使用を移動するだけfalseMです。

ここでは、メタと消去の拡張項を証明し、拡張されていないバージョンを を使用して証明しPure.conjunctiond1ます。

theorem 
  "(PROP P &&& PROP Q) ==> PROP P" 
apply(unfold Pure.conjunction_def)
by(erule Pure.meta_allE, assumption)

theorem expanded_and_1: 
  "(!!R. (PROP P ==> PROP Q ==> PROP R) ==> PROP R) ==> PROP P"
by(erule Pure.meta_allE, assumption)

theorem 
  "(PROP P &&& PROP Q) ==> PROP P"
by(erule Pure.conjunctionD1)

ルールconjunctionD1は にあり、が と同じことをしていると思われる operator を処理してconjunction.MLいるように見えます。forall_elim_vars!!meta_allE

標準の Meta-And を使用できますが、Meta-And は目的ではありません

結合消去規則の 2 つの拡張バージョンを比較します。最初の項は standard&&&を使用し、2 番目の項は my を使用しますandM。

term "(!!R. (P ==> Q ==> PROP R) ==> PROP R) ==> P"
term "((P ==> Q ==> (!!P. PROP P)) ==> (!!P. PROP P)) ==> P"

を使用すると、上に示したよう&&&に で簡単に第 1 項を証明できmeta_allEます。

私には、第 2 項を第 1 項の形に操作できるはずですが、わかりません。それが本当なら、この定理に排除中間の公理を追加する必要はありません。必要に応じて、自然演繹法をたくさん勉強すればわかります。

私の目標が単なるメタ論理演算子である場合、私は を使用します&&&が、それは私の目標ではありません。私の目標は、メタ論理演算子を省略するために使用するメタ偽を定義することです。HOL のすべてを複製するのではなく、Isabelle/Pure の自然な推論フレームワークを少し拡張しようとしています。

この質問から得た主な価値は、除外中間の公理の必要性に注意する必要があることを知っていることです。メタ偽が必要な場合は、除外された中間の公理が必要になるようです。

ここで私は出発します。助けてくれてありがとう、そして長い追加を許してください。

4

1 に答える 1