(これはかなり論理的な質問です) ⋀
などの⋀y . Py
はプレースホルダのようです。 apply (rule allI)
またはapply (erule exE
を使用した後に発生します。私はそれが(!!x. Px) => ∀x. Px
である規則allI
のために偽であると思った(私は!!
がこれから得た場所に⋀
を表すのに使用されると信じています)。しかし、このルールに一致すると思われる特定のシナリオでは、allI
を適用できないようです。 ⋀
はどういう意味ですか? ⋀
が別の状況で異なることを意味するのではないかと思います。イザベルでは何を意味していますか?
1
A
答えて
3
⋀
は普遍的な量指定器ですが、それはというメタデータのです。私。 ∀
など、あなたが働いているロジックを説明するために使用するものです。同様に、は金属学的含意演算子です。そして、これらはイザベルの金属学の唯一の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を参照してください。
関連する問題
- 1. 0x0Fは何を意味していますか?そして、このコードはどういう意味ですか?
- 2. CSSでは「*」は何を意味していますか?
- 3. 「read_strt」はここでは何を意味していますか?
- 4. JavaScriptでは///は何を意味していますか?
- 5. PHPでは「:」とは何を意味していますか?
- 6. jQuery/JavaScriptでは++は何を意味していますか?
- 7. Mathematicaでは、@@@は何を意味していますか?
- 8. Perlでは "$$ q"とは何を意味していますか?
- 9. VimScriptでは=〜は何を意味していますか?
- 10. Rxjavaでは「バックプレッシャー」は何を意味していますか?
- 11. DB_FileではR_CURSORは何を意味していますか?
- 12. postgresqlではLIKE '%%'は何を意味していますか?
- 13. ANTでは「**」とは何を意味していますか?
- 14. PLSQLではGETは何を意味していますか?
- 15. CSSでは「$」は何を意味していますか?
- 16. 意味論は何を意味しますか?
- 17. shで "$ {x %% *}"とは何を意味していますか?
- 18. javascriptで_(variable_name)とは何を意味していますか?
- 19. コマンドラインで「プログラム」とは何を意味していますか?
- 20. Clojureで#^演算子は何を意味していますか?
- 21. セマンティックバージョニングで「パブリックAPI」とは何を意味していますか?
- 22. |&(縦棒、アンパサンド)はbashで何を意味していますか?
- 23. RSpec Matchersで 'failure_message_when_negated'とは何を意味していますか?
- 24. メソッド内でself []は何を意味していますか?
- 25. _ngcontent-c#はAngularで何を意味していますか?
- 26. このステートメントはC#で何を意味していますか?
- 27. Rで「S3メソッド」とは何を意味していますか?
- 28. この行はC99で何を意味していますか?
- 29. IdentityServer 3でidsrvは何を意味していますか?
- 30. `[]`は `setState`で何を意味していますか?