Я пытаюсь увеличить FOL.thy с квантором MOST, который я намерен определить как простое большинство, то есть,Как определить «Most» в Isabelle/FOL?
(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) Какие еще вещи необходимо изменить?
К последнему вопросу, возможно, было бы полезно указать, что в конечном итоге я хочу оценить, необходимы ли, возможны или невозможны различные выводы, с учетом предположений, которые будут включать в себя количественные утверждения с использованием «Большинство» и «Все» (а также союзы, дизъюнкции и т. Д.).
Я отредактировал ваше сообщение s.t. 'Most' является основной константой (использование будет выглядеть как« Most (% x. P x) ») и« MOST »соответствующее связующее (это просто более приятное обозначение для той же константы, то есть' MOST x. P x '). – chris
Два вопроса: 1), о которых «FOL.thy' вы говорите? Один из дистрибутива Isabelle2013? Тогда это скорее «IFOL.thy», я думаю (на котором основан «FOL.thy' и содержит основные определения констант). 2) Что вы подразумеваете под словом «символы» выше? – chris
Btw: Чтобы ваше определение имело смысл, вам нужна теория, в которой у вас есть кардинальные числа с «меньшим». Кажется, что только «FOL» слаб для вашей цели. (В «HOL», например., функция 'card' для числа элементов в наборе определяется только на конечных множествах и, следовательно, также не поможет в вашем случае; если вы не хотите предикат 'P', который справедлив только для конечного числа« входов », а отрицание истинно бесконечно часто, чтобы быть * Most * ly true.) – chris