Программа-минимум кандидатского экзамена по специальности 05.13.17 «Теоретические основы информатики» (стр. 20 из 29)

В-третьих, каждая формальная аксиоматическая теория должна располагать конечным множеством правил вывода. Каждое правило вывода содержит формулы-посылки и формулу-заключение, выводимую при определенных этим правилом условиях из формул-посылок. Формула-заключение называется непосредственным следствием формул-посылок по данному правилу вывода.

Доказательством в формальной аксиоматической теории называется всякая последовательность формул, в которой каждая формула есть либо аксиома теории, либо непосредственное следствие каких-либо предыдущих формул этой последовательности по одному из правил вывода данной теории.

Формула называется теоремой теории тогда и только тогда, когда существует доказательство, в котором эта формула является заключительной формулой.

Исчисление высказываний - наиболее простой пример формальной аксиоматической теории в логике. Существует несколько исчислений высказываний (Гильберта, Клини, Фреге, Новикова). Мы рассмотрим исчисление высказываний Лукасевича (исчисление L), использующее функционально полную систему связок, состоящую из отрицания ¬ и импликации

. Исчисление L описывает множество тождественно истинных формул (тавтологий), что соответствует реальному положению вещей в математике, где теоремы как высказывания являются тождественно истинными формулами.

Язык исчисления L включает перечень употребляемых символов и определение понятия формулы.

Символами исчисления L являются:

- (счетное) множество символов пропозициональных (логических) переменных

- символы логических операций отрицания ¬ и импликации

- символы вспомогательные символы скобок ( , ).

Знаки других логических операций рассматриваются здесь как обозначения формул исчисления L, выражающих эти операции.

Понятие формулы исчисления определяется индуктивно:

- формулами полагаются сначала переменные

- а затем все выражения вида ¬ A и

, где в качестве A и B могут выступать любые из уже имеющихся формул.

Систему аксиом исчисления L составляет бесконечное (счетное) множество формул исчисления, построенных с использованием трех схем аксиом.

Аксиомой при этом считается каждая формула, полученная подстановкой в какую-либо из схем аксиом каких-либо формул исчисления L вместо входящих в эту схему переменных.

Правилом вывода в исчислении L является modus ponens (правило заключения), согласно которому из данных формул вида A и (A->B) выводится формула .

Исчисление предикатов первого порядка и теории первого порядка отличаются тем, что в них допускается применение кванторов только лишь к переменным. Однако установлено, что большинство теорий более высоких порядков сводимо к теориям первого порядка. Каждая теория первого порядка располагает системой аксиом, включающей логические (общие) и собственные (частные) аксиомы. Исчисление предикатов первого порядка - это теория первого порядка, не имеющая собственных аксиом. Дополнение исчисления предикатов аксиомами, присущими некоторой предметной области, превращает его в частную теорию первого порядка, относящуюся к этой области.

Исчисление предикатов первого порядка является определенным расширением исчисления высказываний, поэтому на основе каждого исчисления высказываний может быть построено соответствующее ему исчисление предикатов.

Здесь будет рассматриваться исчисление предикатов (ИП), включающее систему связок и аксиом исчислении высказываний Лукасевича. Большинство обсуждаемых здесь результатов (кроме особо оговоренных для ИП) относится к любым теориям первого порядка.

Язык теорий первого порядка богаче языка исчисления высказываний благодаря использованию (нелогических) предметных переменных, что влечет за собой необходимость рассмотрения логических и нелогических функций от нелогических переменных (наряду с логическими переменными и логическими связками исчисления высказываний). Множество символов теорий первого порядка включает подмножества:

- символов предметных констант;

- функциональных символов (функторов);

- предикатных символов (предикатов);

- символов предметных переменных;

- логических символов;

- вспомогательных символов.

Множество символов

называется сигнатурой. Символы, входящие в сигнатуру, выделены в особое подмножество по той причине, что наделение этих символов предметным содержанием связывает формальную аксиоматическую теорию с конкретной предметной областью (формальная аксиоматическая теория получает предметную интерпретацию), благодаря чему одна и та же формальная аксиоматическая теория оказывается применимой в различных предметных областях.

Множество формул исчисления предикатов и теорий первого порядка определяется в два этапа: сначала описывается понятие терма (как нелогической функции от нелогических переменных), через которое затем определяется понятие логической формулы.

Терм (сигнатуры

)определяется индуктивно: термами полагаются сначала предметные переменные и предметные константы, а затем - все выражения вида , где - любой из функциональных символов, а - любые из уже имеющихся термов.

Формула (сигнатуры

) определяется также индуктивно: (атомарными, простейшими) формулами полагаются выражения вида , где - предикатный символ и - термы, а затем - все выражения вида , где A и B - любые из уже имеющихся формул, а - любая из предметных переменных.

В выражении

формула A называется областью действия квантора .

Пара S = (D, I) называется алгебраической системой сигнатуры

при условии, что D - непустое множество, а I - отображение, ставящее в соответствие каждой предметной константе - элемент , каждому функциональному символу - некоторую n-местную операцию в D, каждому предикатному символу - некоторое n-местное отношение в D. Множество D называется областью интерпретации, а отображение I - интерпретацией сигнатуры в D.

Алгебраическая система путем интерпретации "опредмечивает" абстрактные символы, придавая им конкретный смысл в предметной области, характеризуемой множеством D. Задание алгебраической системы позволяет вычислять значения термов и определять выполнимость формул.

Аксиомы теорий первого порядка разбиваются на логические и собственные. Логические аксиомы (аксиомы исчисления предикатов) - это бесконечное множество формул, построенных с помощью пяти схем аксиом. Три схемы аксиом ИП совпадают со схемами аксиом исчисления высказываний Лукасевича, остальные же две специфичны для исчисления предикатов. Их назначение - учесть специфику формул с кванторами и обеспечить логическую общезначимость теорем ИП.

Собственные аксиомы теорий первого порядка не могут быть сформулированы в общем виде, так как каждая теория первого порядка имеет свой набор собственных аксиом. Таким образом, исчисление предикатов первого порядка - это теория первого порядка, не имеющая собственных аксиом.

Правилами вывода в теориях первого порядка являются следующие два основных правила: modus ponens (правило заключения), по которому из формул A и (A - >B)выводится формула B; правило обобщения (связывания квантором общности), по которому из формулы A выводится формула

. Наряду с названными основными правилами вывода, как обычно, используются и другие правила, в качестве которых выступают многие выведенные в исчислении предикатов теоремы.