2 Постановка задачи: о связном предъявлении теории информатики и практики программирования в теме исполнения для теоретического мышления. 13 (стр. 17 из 25)
Сущность упорядоченно-сортной логики заключается в том, что на сортах задается частичное упорядочение, определяющее подсорта, которое семантически интерпретируется как теоретико-множественное включение носителей модели. Кроме того, предусматривается перегрузка операций, которая интерпретируется как ограничение функций на подсорта. Упорядоченно-сортная логика не намного сложнее многосортной, и практически все результаты, полученные для многосортного случая, без особых сложностей обобщаются на упорядоченно-сортный.
Итак, в рамках системологического аспекта мы воспринимаем логический стиль через более общее понимание, заключающееся в том, что существуют языки, поддерживающие современный аксиоматический метод .
Тогда уровнем программирования на этих языках для логического стиля может быть программирование ЛАС (пользуясь аксиоматическим методом), а уровнем спецификации может выступать упорядоченно-сортная теория моделей как расширение логического стиля без добавления ограничений.
Итак, мы понимаем современный аксиоматический метод как:
· возможность варьировать истинностью, рассматривая только определенный класс моделей;
· наличие языка, его поддерживающего.
Можно сказать, что современный аксиоматический метод - это сущность математики, которая изучает свои собственные методы предъявления знания, рассматривающая саму себя как язык.
Ñîâðåìåííûé àêñèîìàòè÷åñêèé ìåòîä ëîãèêî-àëãåáðàè÷åñêèõ ñïåöèôèêàöèé ïîääåðæèâàåòñÿ â ïðîãðàììèðîâàíèåì ÿçûêàìè OBJ, EQLOG, FOOPS. Ïîýòîìó, çäåñü îñìûñëèâàòåñÿ â êà÷åñòâå áóäóùåãî ó÷åáíîãî ìàòåðèàëà êëàññè÷åñêàÿ òåìà òåîðèè ìîäåëåé äëÿ ÿçûêà èñ÷èñëåíèÿ ïðåäèêàòîâ ïåðâîãî ïîðÿäêà - òåîðåìà êîìïàêòíîñòè Ãåäåëÿ-Ìàëüöåâà.
Цель этого пункта - поговорить о вычислительных возможностях языка исчисления предикатов, используя минимальный багаж знаний. Например, в серии “Популярные лекции по математике” нам очень интересно было посмотреть выпуски Успенского В. А. “Теорема Геделя о неполноте” и “Машина Поста”. Действительно, в первой книге отмечается, что для понимания доказательства теоремы Геделя о неполноте необходимо знакомство с простейшей терминологией теории множеств (словами “множество”, “функция”, “область определения” и т.п.) и некоторая привычка к восприятию математических рассуждений. Так что “оно доступно и подготовленному школьнику” [26]. Во второй книге понятие программирования вводится через понятие машины Поста, через ее функционирование. При этом по ходу дела вводятся понятия алгоритма и программы, диаграмм и блок-схем, состояний и переходов из одного состояния в другое. Рассматриваются проблемы разрешимости и применимости алгоритма.
Попробуем следовать этому примеру, то есть, понимая уровень обучаемого (универсал), мы должны показать ему границы выразимости языка при использовании простейших понятий - нам нужно найти эквивалентные формулировки соответствующих понятий на более простом уровне. Например, Барвайс [21]: излагает теорему компактности сначала для логики высказываний. Там все очень просто и легко для понимания, поэтому уже на таком уровне мы можем показать то, что хотим.
Главное, язык предикатов хорош, но он ограничен, с одной стороны, но есть хороший вычислитель, с другой стороны. Предполагаем также, что уже существует описание среды саморазсвтия для идеи вывода [29].
Теория моделей представляет собой раздел математической логики, изучающий связи между формальным языком и его интерпретациями, или моделями.
| Пример. Приведем пример моделей, представляющих собой структуры, встречающиеся в математике. Циклическая группа пятого порядка, поле рациональных чисел - модели рассматриваемого типа. |
Можно было бы прямо сейчас заняться изучением этих моделей, не привлекая формального языка. Тогда мы окажемся в области универсальной алгебры, предметом которой являются гомоморфизмы, подструктуры, прямые произведения и т. п.
Чтобы добраться до теории моделей, вводится в рассмотрение формальный язык - язык логики предикатов первого порядка с равенством. Формальный язык требуется нам для того, чтобы в наших рассуждениях о моделях мы могли использовать и предложения соответствующих формальных систем. С этой целью мы каждой паре, состоящей из предложения и модели, ставим в соответствие одно из истинностных значений - истинно или ложно. Вводимое таким образом понятие истинности играет роль моста, связывающего формальный язык с его интерпретацией посредством моделей.
Типичные результаты теории моделей содержат некоторую информацию негативного характера о выразимости логики предикатов первого порядка. Один из классических результатов - теорема компактности, принадлежащая Гёделю[1930] и Мальцеву[1936]: если каждое конечное подмножество имеет модель, то и все множество имеет модель. С помощью этой теоремы было показано, что многие интересные свойства моделей нельзя выразить, используя только множества предложений логики первого порядка. Надо заметить, что техника теории моделей развивалась большей частью именно для логики первого порядка.
Единство теории моделей придает различение синтаксиса и семантики, проводимое во всей этой теории. Синтаксис имеет дело с чисто формальной структурой языка (например, длина предложения или совокупность символов, входящих в него - вопрос семантический). Семантика же изучает интерпретацию, или значение формального языка. Истинность или ложность предложения в модели - вопрос семантический.
Большая часть теории моделей исследует взаимодействие синтаксических и семантических идей. Именно поэтому теория моделей важна для информатики, так как мы вкладываем в компьютер синтаксические вещи, а предъявляем знания (семантику). Мы видим реальную связь формального языка и его интерпретации:
| Пример. Знания о решении систем линейных алгебраических уравнений могут быть представлены в компьютере в виде программы на некотором языке программирования (используем формальный язык). |
Универсала интересуют прежде всего границы инструмента информационного моделирования, то есть выразимость: что можно выразить с помощью данного инструмента, а что нельзя. В нашем случае инструмент - это логика предикатов первого порядка.
4.3.2 Теория моделей логики высказываний
Теперь изложим теорию моделей для одного очень простого формального языка - логики высказываний. На этой “игрушечной” теории моделей мы сможем легче уяснить для себя очень важный результат - теорему компактности - на основе простейшего формального языка и классических примеров, облегчающих понимание теории для более сложных логик.
Язык логики высказываний Ф - множество простых утверждений + построенные из них составные утверждения. Интуитивная интерпретация для этих утверждений - “возможный мир”, где каждое утверждение либо истинно, либо ложно. Мы хотим заменить интуитивные интерпретации совокупностью точных математических объектов. Таким образом возникает отображение F: Ф®Boolean. Вместо этого мы будем рассматривать в качестве модели - произвольное подмножество А множества F: SÎА означает, что простое высказывание S истинно, SÏА - что простое высказывание S ложно.
Опишем логику высказываний как формальный язык. Наш язык содержит следующие символы: логические связки Ù(и) и Ø(не), скобки (,), непустое множество Ф высказывательных символов.
Определение (высказывания относительно множества Ф). Можно предложить различные определения высказываний. Мы приведем некоторые из них.
| Индуктивное |
| (i) SÎF - высказывание (ii) j - высказывание Þ Øj - высказывание (iii) j, y - высказывания Þ j&y - высказывание (iv) ничто другое не является высказыванием |
| Рекурсивное |
 . j - высказывание |
| Теоретико-множественное |
 |
L - язык, построенный на основе высказывательных символов из F.
Теперь мы готовы посредством определения истинности высказывания в модели перекинуть мост между языком L и его моделями.
Определение. Истинность высказывания j в модели. (A|=j: j выполняется в А, или А - модель для j).
(i) jÎF Þ A|=j Û SÎA
(ii) j = Øy Þ A|=j Û A|=y не имеет места
(iii) j = q&y Þ A|=j Û A|=y, A|=q
Особенно важным видом высказываний являются истинные высказывания. Высказывание j называется истинным (|=j), если j - истинно во всех моделях языка L. На первый взгляд кажется, что, отвечая на вопрос “Является ли высказывание j бесконечного языка L истинным?”, нужно исследовать в общем случае несчетное множество бесконечных моделей А. Это происходит из-за того, что истинность - семантическое понятие, определяемое с помощью моделей. Однако, существует простой и регулярный способ распознавать в конечное число шагов, является ли это высказывание истинным или нет .