Amigo писал(а):
Не могли бы Вы на примере показать как строится модель.
Возьмём например две аксиомы
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.