Труды научно-исследовательского семинара логического центра ИФ РАН

Определение D3. Формулы языка исчисления R верифицируются в мире W: исключительно в соответствии со следующими условиями: (1)-(8) определения D 1 , в которых одинарная стрелка заменя­ется двойной (9) Во всяком универсуме рассуждений w-, в котором верифици­руется формула А, верифицируется формула Л=>В=>В. Или фор­мально: VwflW/w. Э T(A*>B*>B)/w¡). Мы корректируем также соответствующим образом определение семантически истинной формулы: D4.NB sd f У^<Г(В^В)/^. Э T(B)/wt Покажем, что все теоремы исчисления R являются семантически истинными в смысле определения D4. Метатеорема МТ4. Если формула В есть теорема системы Я, то |=В в семантикеSe a для языка исчисления!?. Учитывая, что произведенные в семантике, построенной для 2?, изменения сохраняют возможность доказать семантическую истин­ность аксиом А1-А15 исчисления Я, а также свойство правил вывода оставлять такую истинность в силе, для доказательства МТ4 оста­ется установить семантическую истинность аксиомы А16. Чтобы убедиться в этом, достаточно показать, что во всяком мире, в кото­ром верифицируется формула А*>.В*>С9 всегда верифицируется такжеВ*М=>С. В соответсвии с пунктом (9) определения D3, в каждом мире, в котором верифицируется формула В, верифицируется В«>0>С, а значит и (Л=^.В=>С)=>и4=>С. Мы имеем, таким образом: Г(В)/н>. Э Г ( ( 4 ^ . В ^ С ) ^ Л ^ С ) / н > . (1) Частным случаем утверждения (1) является: TtA*.B*>C)/w¡ Э Т((В =>.64^В=>а^Л=>0=».В=>Л=»аУ^ (2) 72