В Hughes and Cresswell A New Introduction to Modal Logic (изд. 1996 г.), стр. 271, они пытаются установить неполноту системы K + G1 + BF (где K есть L(P->Q)->(LP->LQ ), G1 — это MLP->LMP, а BF — это формула Баркана), которые, как они установили ранее, должны были бы характеризоваться сходящимися системами отсчета (т. е. (w1Rw2 & w1Rw3) -> Ew4: (w2Rw4 & w3Rw4)), если бы они были полный.
Они пишут:
Итак, чтобы установить неполноту KG1 + BF, достаточно найти не-теорему, которая верна на каждом сходящемся репере, или, что то же самое, непротиворечивую в.ф.ф., которая не может быть выполнена ни на каком сходящемся репере.
Затем они приводят длинный и сложный wff, который, как они утверждают без доказательств, действительно доказывает неполноту системы. (Правка: я нашел полное изложение доказательства в «Неполноте и формуле Баркана» М. Дж. Крессвелла. Журнал философской логики, том 24, № 4 (август 1995 г.), стр. 379-403. Он использует такая же проблематичная формулировка в этой статье.)
Мой вопрос в том, как эти две вещи составляют одно и то же? Не-теорема KG1+BF, которая верна для каждого сходящегося фрейма, не звучит как непротиворечивая wff, которая не может быть удовлетворена ни для одного сходящегося фрейма. Во-первых, первое справедливо для каждой сходящейся системы отсчета, а второе — нет ни для одной. Что я неправильно понимаю?
Если формула А непротиворечива, то ее отрицание -А не является теоремой. Мы можем рассмотреть два случая для согласованной формулы. Формула — это теорема, но тогда, предполагая, что логика верна, мы получили бы противоречие (теорема верна в каждой модели конкретного типа), но оно не выполняется. Таким образом, если мы имеем, что непротиворечивая формула не может быть выполнена ни в одном сходящемся репере, это означает, что ее отрицание справедливо в этом классе реперов. Однако отрицание формулы не является теоремой, иначе А не было бы непротиворечивым.
Ключевой момент теоремы о неполноте — показать, что существует формула, действительная в классе, но не являющаяся теоремой. В случае непротиворечивой формулы действительной формулой будет ее отрицание.