イザベルでは何を意味していますか？

Question

（これはかなり論理的な質問です） ⋀などの⋀y . Pyはプレースホルダのようです。 apply (rule allI)またはapply (erule exEを使用した後に発生します。私はそれが(!!x. Px) => ∀x. Pxである規則allIのために偽であると思った（私は!!がこれから得た場所に⋀を表すのに使用されると信じています）。しかし、このルールに一致すると思われる特定のシナリオでは、allIを適用できないようです。 ⋀はどういう意味ですか？ ⋀が別の状況で異なることを意味するのではないかと思います。

Answer 1

⋀は普遍的な量指定器ですが、それはというメタデータのです。私。 ∀など、あなたが働いているロジックを説明するために使用するものです。同様に、は金属学的含意演算子です。そして、これらはイザベルの金属学の唯一の2つの原始的なものです。否定はないので、古典的論理よりはるかに弱いです。詳細については、http://isabelle.in.tum.de/coursematerial/PSV2009-1/session2/document.pdfまたはhttps://www.cl.cam.ac.uk/teaching/1011/L21/5%20-%20Logic.pdfを参照してください。