НГУ

Всё, я нашел способ доказательства существования такой формулы!
Вещь оказалась тревиальная, достаточно было модернизировать
формулу P=(x-->y’)’ , что бы получить необходимый результат.
Понятно, что формула P=(x-->y’)’ - истинна, тогда и только тогда когда х истинно. Но х - сама может являться формулой, причём имеющей тот же вид, что и исходная т.е. P=(G-->y’)’ и
G=(z-->х’)’ , но G, как легко видеть, только тогда истинна, когда
z и x одновременно истинны. Потому, формула P=((z-->х’)’-->y’)’ истинна, тогда и только тогда, когда х,y,z - одновременно истинны.
* * * * * * *
У меня возникла теперь задача: доказать, что система аксиом - независима. Я читал, что это осуществляется при помощи построения, так называемой "модели". К сожалению, понятие "модель" - настолько абстрактое, что уловить его сущность я не смог. Потому, хотел бы попросить Вас, показать на любой из описанной в этой теме систем,
каким образом можно построить модель. Особенно меня интересует вопрос - почему именно существование модели доказывает независимость системы аксиом?

_________________
Единственный способ установить границы возможного - это выйти за них в невозможное.

Господа, помогите наконец доказать независимость системы аксиом
исчисления (XY_ИВ). Идей вообще никаких нет, как говорится -"общее состояние непонятности".

_________________
Единственный способ установить границы возможного - это выйти за них в невозможное.

Признаюсь сразу, что читал ветку очень поверхностно. Но кое-что напишу. Если под независимостью аксион понимать: аксиомы независимы, если никакую из них нельзя вывести из остальных, --- то доказать независимость при помощи построения модели можно следующим способом. Пусть у нас есть система аксиом a_1, ..., a_n, нужно доказать, что аксиома a_0 из них не выводится. Строим модель, на котрой a_0 ложна, a_1, ..., a_n истинны. Из существования такой модели следует невыводимость.

Не могли бы Вы на примере показать как строится модель.
Возьмём например две аксиомы
1. X
2. (X-->(X'-->X))
Как можно построить здесь модель?

_________________
Единственный способ установить границы возможного - это выйти за них в невозможное.

Поскольку формула (X-->(X'-->X)) является тавтологией, с доказательством ее невыводимости будет напряг, ибо классические модели тут не подойдут: она в них будет всегда истинной. (Неклассические -- найдутся, но у меня есть только пара минут. Кстати, заранее извините за опечатки: некогда перечитывать написанное.) А классическую модель, обосновывающую невыводимость X из (X-->(X'-->X)), построить очень легко. Модель состоит всего лишь из одного бита x. (Бит -- это 0 или 1.) Индукцией по сложности формулы Ф определяется истинность Ф в модели (x) (пишут (x)|=Ф). Индуктивное определение такое:

(x)|=X, если x=1
(x)|=(F)', если (x)|=F неверно
(x)|=(F->G), если (x)|=F неверно или (x)|=G верно.

Легко показать, что MP сохраняет истинность формул в модели. Поэтому, если формулы F и G таковы, что (x)|=F верно, а (x)|=G неверно, то G нельзя вывести из F. Осталось заметить, что (0)|=(X-->(X'-->X)) верно, а (0)|=X неверно.

Если сигнатура состоит из двух переменных X и Y, то в качестве модели уже надо взять упорядоченную пару битиков (x,y) и чуток изменить определение истинности:

(x,y)|=X, если x=1
(x,y)|=Y, если у=1
остальное -- как и раньше.

Тогда, например, (1,0)|=X верно, а (1,0)|=Y неверно, а значит, Y нельзя вывести из X.