在这里，我要求证明 Isabelle 元逻辑合取消除规则。
下面的来源包含我的评论，这些评论解释了我在做什么。在理论上，有两对元假定义和连词消除规则。两对如下：
falseH,andH_E1, 和falseM,andM_E1.
我的andM连词(P ==> Q ==> falseM) ==> falseM)形式是 ，我无法简单地证明这种形式。
将来，我计划使用类似于andM上述的元逻辑运算符来复制 HOL.thy 自然演绎规则。作为其中的一部分，运算符==>将被视为原始运算符。因为 Pure 运算符!!在与 相同的意义上也是原始的==>，所以我猜我可能无法开发有助于我使用元假定义的规则!!P. PROP P，因为我在下面使用它。不过，我可能是错的。
这不像我必须有falseM我在下面尝试使用的，因为falseH有利于simp已经与 HOL 结合使用的魔法，双关语不是故意的。虽然我不必拥有它，但拥有它会很好。
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)
我用三件事对此进行了更新，其中两件事与 Andreas 的回答有关，即需要排除中间公理。我在下面所说的并不是对任何事情的真正答案，并且可以接受更多评论，因为我在简单的事情上可能会出错。
我把我的冗长评论放在这里是为了巩固一些与我的问题的核心思想相关的想法，即如何使用元逻辑假来定义元逻辑运算符。
- 我展示了我认为我将如何在语言环境中添加排除中间的元逻辑公理。
- 我展示了是什么让我理解了我需要什么形式的排中公理。大多数文献都会说排中是
P or not P，这是具有欺骗性的，因为我很少考虑排中，因为它已经根深蒂固了我的思想。 - 我注意到这
"(P &&& Q) ==> P是由conjunctionD1in证明的conjunction.ML，而展开的版本是由 证明的meta_allE。我想知道为什么不能操纵内部而不是外部andM，!!以便可以证明它。
将元逻辑排除在语言环境中
因此，Adreas 指出 Isabelle/Pure 没有排中，而我需要它，从而为我节省了几个月，可能至少一年，甚至可能是多年徒劳无功的计划。这有助于回答我的相关问题，并帮助我更了解 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 提供的证明中，有classical来自 HOL：
lemma classical:
assumes prem: "~P ==> P" shows "P"
apply (rule True_or_False [THEN disjE, THEN eqTrueE])
...
像这样的 HOL 定理的证明步骤告诉我元逻辑版本需要什么。我通过提供 locale axiom 做了简单的部分t_or_f。其余的只是简单的工作。
伊莎贝尔/纯没有排除中间
在这里，我不只是为了说话而说话，我有时会这样做，但我投入了我的努力，以了解==作为被排斥的中间人所需要的一部分。我可能需要再看一遍这一切，所以也许它不会对我不利。
首先，跳到我接下来要说的关于 HOL 引理的内容之前excluded_middle，一个人，尤其是我，也会想考虑这个
HOL.thy公理，第 171 行：
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 为假，则 P 为假”，而不是需要什么，“如果 P 不为假，那么它一定是真的”。
更新（131213）：我把这个放进去是因为我忘记了我为什么做某事，然后当我试图通过逻辑重新工作时，我想我搞砸了，当我没有搞砸的时候，虽然我的逻辑意识可能没有已经完成。
我实际上并没有实现 的元逻辑版本
~P | P，而是P | ~P. 如果它不明显，可能是，我使用基于真值表的蕴涵定义以及德摩根定律，并使用逻辑的基本定理，这最终对我来说必须是正确的。但是，我现在正在对排中公理进行事后研究，这使得我使用的事实
P | ~P不太可接受，因为它变成了"((P ==> falseM) ==> falseM) ==> P"，这涉及双重否定，我隐约记得这与这一切有关。直到现在，我一生中从来没有关心过排中。这应该是建构主义者的想法。我做出这个转换实际上是很幸运的，因为这让我看到了
=in的重要性True_or_False。
一个有意义的定理将是“不是（P 而不是 P）”（或者会吗？）。所以我在 meta-and 表达式中
替换(P ==> falseM)。Q(P ==> Q ==> falseM) ==> falseM
theorem
"((P ==> (P ==> falseM) ==> falseM) ==> falseM) ==> falseM"
by(auto,assumption)
这已经完全发挥了逻辑傻瓜的红色警报，因为falseM
不必扩展。现在，我陈述相同的定理，但没有
bool变量和没有，以明确表示它与orfalseM无关。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它使用 operator ==，元或 as (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可以证明的意义的linarith，在presburger哪里是这样的：&&&pure_thy.ML
"(A &&& B) == (!!C::prop. (A ==> B ==> C) ==> C)"
我的 meta-and, using falseM，实际上只是将 use!!从外部移动到内部，曾经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在conjunction.ML，似乎forall_elim_vars
正在照顾运营商!!，我想这只是在做同样的事情meta_allE。
我可以使用标准的 Meta-And，但 Meta-And 不是目标
我比较了连词消除规则的两个扩展版本。第一项使用标准&&&，第二项使用我的andM。
term "(!!R. (P ==> Q ==> PROP R) ==> PROP R) ==> P"
term "((P ==> Q ==> (!!P. PROP P)) ==> (!!P. PROP P)) ==> P"
使用&&&可以很容易地证明第一项meta_allE，如上所示。
在我看来，我应该能够将第二项操纵成第一项的形式，但我不知道。如果这是真的，那么我不需要为这个定理添加排中公理。在学习了很多自然演绎之后，我会知道，就像我需要的那样。
如果我的目标只是元逻辑运算符，我会使用&&&，但这不是我的目标。我的目标是定义一个 meta-false 用于缩写元逻辑运算符。我试图稍微扩展 Isabelle/Pure 的自然演绎框架，而不是复制所有的 HOL。
我从这个问题中得到的主要价值是，我现在知道我需要注意是否需要排除中间公理。如果我想要一个元假，那么我似乎需要一个排中公理。
这是我离开的地方。感谢您的帮助，请原谅冗长的补充。