Математическое введение в декларативное программирование. Зюзысов В.М. - 19 стр.

UptoLike

Составители: 

ную область, обычно рассматривается как математическое описание объектов. Таким об-
разом, практически нас интересует не все интерпретации данной теории, а лишь те из них
на которых выполнены аксиомы.
Модели
Интерпретация называется моделью множества формул Γ, если все формулы этого
множества выполняются в данной интерпретации.
Моделью теории называется такая интерпретация, в которой истинны все теоремы
теории.
2.4.2 Общезначимость и непротиворечивость
Формула P называется общезначимой, если она истинна в каждой интерпретации
(обозначается |= P).
Формула P называется противоречием, если формула P ложна во всякой интерпрета-
ции.
Формула P называется логическим следствием множества формул Γ, если P выпол-
няется в любой модели Γ.
Формула B является логическим следствием формулы A (обозначение: A B), если
формула B выполнена в любой интерпретации, в которой выполнена формула A.
Формулы A и B логически эквивалентны (обозначение: A=B), если они являются логи-
ческим следствием друг друга.
Формальная теория T называется семантически непротиворечивой, если ни одна ее
теорема не является противоречием.
Формальная теория пригодна для описания тех предметных областей, которые яв-
ляются ею моделями.
Справедлива метатеорема:
Модель для формальной теории T существует тогда и только тогда, когда T семан-
тически непротиворечива.
Обсудим подход к разрешению противоречий, принятый в математике [24]. Фор-
мальные системы, использующие логический вывод, не могут содержать противоречий
противоречия мгновенно заражают всю систему, подобно глобальному раку. Это не по-
хоже на человеческую мысль. Если вы обнаружите в своих рассуждениях противоречие,
вряд ли это разрушит все здание вашего мышления. Вместо этого вы, скорее всего, попы-
таетесь найти те идеи или методы рассуждения, которые явились причиной противоречия.
Иными словами, вы попытаетесь, насколько это возможно, выйти из ваших внутренних
систем, приведших к противоречию, и попробуете их исправить. Маловероятно, что вы
поднимите руки вверх и воскликнете: «Это показывает, что теперь я верю во все, что
угодно!» – разве что в шутку.
В действительности, противоречияэто важный источник прогресса во всех об-
ластях жизни, и математика не является исключением. В прошлом, когда в математике
обнаруживалось противоречие, математики тут же пытались найти виновную в этом сис-
тему, выйти из таковой, проанализировать её и, если возможно, залатать прореху. Вместо
того, чтобы делать математику слабее, нахождение и «починка» противоречивых систем
только усиливали её.
2.4.3 Полнота, независимость и разрешимость
Пусть универсум M, рассматриваемый с соответствующей интерпретацией, являет-
ся моделью формальной теории T.
19