Множество семантически правильных совокупностей [c.33]
Наконец, правила П в классическом исчислении высказываний в той его форме, как она рассматривается в данном примере, имеют вид 1. Если a — семантически правильная совокупность (выводимая формула), то при замене в а любого базового элемента (везде, где он входит в а) любой формулой вновь получается выводимая формула 2. Если (а->р) и a — выводимые формулы, то Р также выводимая формула. [c.35]
Наконец, семантические правила П (по-другому они называются правилами вывода) расширяют, если это возможно, множество аксиом, добавляя к ним новые синтаксически правильные совокупности. Множество, получаемое после применения семантических правил к аксиомам, носит название множества семантически правильных совокупностей. [c.33]
На рис. 1.8 условно показан результат работы формальной системы, которая выступает как автономный генератор. Процедуры порождения множества синтаксически правильных совокупностей, основанные на произвольном применении правил Р, и процедуры порождения множества семантически правильных [c.33]
Определение 1.5. Конструктивная формальная модель, для которой существует конструктивная процедура л4, дающая однозначный ответ на вопрос — принадлежит ли данная синтаксически правильная совокупность множеству семантически правильных совокупностей, называется разрешимой формальной моделью. [c.34]
Пример 1.4. Вернемся снова к коробке детских кубиков, содержащей всего шесть кубиков. Каждый кубик есть базовый элемент. Легко убедиться, что существуют лх и я2, позволяющие отличать один кубик от другого (по несовпадающему рисунку хотя бы на одной грани двух сравниваемых кубиков) и отличать кубики из других наборов (например, по несовпадению концевых точек линий или границ между цветами на всех шести гранях данного кубика со всеми другими кубиками набора, если нет более простого признака типа другого размера кубика). Система синтаксических правил такова, что она считает синтаксически правильными любые совокупности кубиков, в которых все шесть кубиков выложены в виде прямоугольника 2x3 или 3x2. Ясно, что существует конструктивная процедура п3. Система аксиом совпадает с такой совокупностью кубиков, которая соответствует одной из приложенных к коробке картинок (эта картинка как бы фиксируется в виде начальной позиции). Правила П дают возможность получать из исходной картинки новые картинки (думаю, что читатели в детстве сами строили эти правила). И, наконец, ясно, что существует конструктивная процедура л4, ибо определение всех семантически правильных совокупностей содержится в наборе шести картинок, приложенных к набору. Следовательно, мы имеем дело с разрешимой формальной моделью. [c.34]