1

私はFOL.thyquantifierを増補しようとしMOSTています。これは、単純多数派として定義するつもりです。つまり、

(MOST x. P(x)) ==> card P(x) > card ~P(x).

ファイルの変更方法がわかりませんFOL.thy。の下axiomatizationに、次を追加することを考えました:

Most :: "('a => o) => o"  (binder "MOST " 10)

そして、where句の下に：

specM: "(ALL x. P(x)) ==> (MOST x. P(x))" and
mostI: "(MOST x. P(x)) ==> ..."

ここで、「...」は、上で概説した制約を表現する適切な方法P(x)です~P(x)。（繰り返しますが、ここで良い名前がわかりませんでした。提案は大歓迎です。）

「シンボル」セクションにエントリを追加することを考えましたが、より良いアイデアがないため、デルタを使用することにしました。

Most (binder "∆" 10)

notationセクションでも同様です。

1)カーディナリティ制約を適切に表現するにはどうすればよいですか?

2) 他に何を変更する必要がありますか?

後者の質問に対しては、最終的には、「Most」と「All」を使用した定量化された主張を含む前提を前提として、多くの異なる結論が必要か、可能か、不可能かを評価したいということを指摘しておくと役立つかもしれません (接続詞、選言など）。

4

1 に答える 1

1

特に理由がない限り、一般的には、考えているアプリケーションの出発点として Isabelle/HOL を使用することをお勧めします。

FOL と HOL のどちらが強いかという議論は、追加の公理化に依存します。Isabelle/ZF は、FOL の上に完全な Zermelo-Fraenkel 集合論を提供するため、単純な HOL よりも表現力がありますが、そのツールとライブラリはほぼ 20 年遅れています。

一番下から始めるのではなく、理論をHOL.thy持って一番上からゲームに参加する必要があります。Main$ISABELLE_HOME/src/HOL/Library

あなたのスケッチはMost私に思い出させますが$ISABELLE_HOME/src/HOL/Library/Infite_Set、それはもっと興味深い無限のセットについてです. HOL の序数と基数については、まだ発見されていない理論があります。最終的にアプリケーションが何であるかによって異なります。

于 2013-10-09T19:15:53.023 に答える