Как определить «Большинство» в Isabelle/FOL?

Я пытаюсь дополнить FOL.thy квантором 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)) ==> ..."

где "..." - это правильный способ выражения ограничения, как указано выше, w.r.t. мощность P(x) и ~P(x). (Опять же, я не был уверен, что это хорошее имя, и предложения приветствуются.)

Я подумал добавить запись в раздел «символы» и, за неимением лучших идей, решил использовать дельту:

Most (binder "∆" 10)

И так же в разделе notation.

1) Как правильно выразить ограничение кардинальности?

2) Что еще нужно изменить?

Что касается последнего вопроса, было бы полезно указать, что, в конечном счете, я хочу оценить, является ли ряд различных выводов необходимым, возможным или невозможным, учитывая предпосылки, которые будут включать количественные утверждения с использованием «Большинство» и «Все» ( а также союзы, дизъюнкции и др.).


quantifiers isabelle
person CrashMaster    schedule 30.09.2013    source источник
comment
Я отредактировал ваш пост s.t. Most — это базовая константа (использование будет похоже на Most (%x. P x)), а MOST — соответствующее связующее (что является более удобным обозначением той же константы, т. е. MOST x. P x).   -  person chris    schedule 01.10.2013
comment
Два вопроса: 1) о каком FOL.thy вы говорите? Тот, что из раздачи Isabelle2013? Тогда это скорее должно быть IFOL.thy, я думаю (на котором основан FOL.thy и который содержит основные определения констант). 2) Что вы подразумеваете под разделом символов выше?   -  person chris    schedule 01.10.2013
comment
Кстати: чтобы ваше определение имело смысл, вам нужна теория, в которой у вас есть количественные числа с меньшим сравнением. Кажется, что FOL сам по себе слишком слаб для вашей цели. (В HOL, например, функция card для количества элементов в наборе определена только для конечных наборов и, следовательно, также не поможет в вашем случае, если только вы не хотите, чтобы предикат P был верен только для конечного числа входных данных и чье отрицание верно бесконечно часто, чтобы быть В большинстве случаевверным.)   -  person chris    schedule 01.10.2013
comment
@chris, вы совершенно правы, что FOL слаб, и мне нужно немного HOL. Я думал, что карта доступна в FOL. Что касается других ваших комментариев, раздел «символы» был просто частью файла, в котором, казалось, определялись символы. Я избегал беготни по изучению того, как функционирует Изабель, потому что на самом деле это не является целью моего проекта, но, похоже, я должен потратить время. Если вы решите ответить, я отмечу это как полезное.   -  person CrashMaster    schedule 01.10.2013

Ответы (1)


arrow_upward
1
arrow_downward

Если нет особой причины, как правило, лучше взять Isabelle/HOL в качестве отправной точки для любого приложения, которое вы имеете в виду.

Аргумент о том, сильнее ли FOL или HOL, зависит от дополнительной аксиоматизации. Isabelle/ZF предоставляет полную теорию множеств Цермело-Френкеля поверх FOL, поэтому он более выразительный, чем обычный HOL, но его инструменты и библиотеки отстают почти на 20 лет.

Вместо того, чтобы начинать снизу HOL.thy, вы должны начать игру сверху с теорией Main, возможно, с некоторыми дополнительными теориями из $ISABELLE_HOME/src/HOL/Library.

Ваши наброски с Most напоминают мне $ISABELLE_HOME/src/HOL/Library/Infite_Set, хотя то есть о более интересных бесконечных множествах. Есть и другие теории об ординалах и кардиналах в HOL, которые предстоит открыть. Это зависит от того, что в конечном итоге является вашим приложением.

person Makarius    schedule 09.10.2013