Аксиоматическая система логики предикатов первого порядка

Формализовать логику предикатов в виде аксиоматической системы означает: - указать систему аксиом; - дать правила вывода; - сформулировать понятия доказательства и доказуемой формулы. Аксиомами классической логики предикатов являются схемы аксиом логики высказываний и схемы аксиом собственно логики предикатов.

Аксиомы логики высказываний А1. А ^ (В ^ А); А2. (А ^ (В ^ С)) ^ ((А ^ В) ^ (А ^ С)); А3. А л В ^ А; А4. А л В ^ В; Правила вывода (метазнак «d » означает, что формула доказуема). П1. (модус поненс) П2. (обобщения) П3. (подстановки). В любую из аксиому А1. - А11. вместо вхо - ждения какого - то символа высказывания разрешается подставить произвольную формулу логики предикатов соблюдая такое условие: одна и та же формула логики предикатов должна подстав - ляться на место каждого вхождения фиксированного символа высказывания в аксиому. Комментарий к П3. Например, в А8. символ «С» входит трижды. Тогда при подстановке каждое вхождение символа С заменяется одной и той же формулой логики предикатов. Комментарий к Ак1 и Ак2. Требование «терм t свободен для х в А (х)» существенно. Напомним, что терм - это константа или индивидная переменная. Если мы нарушим это требование, то из истинной формулы можем получить ложную формулу. Возьмем арифметические утверждения, представленные в языке логики предикатов, и нарушим указанное требование: VxVy~ (х = у)) ^ Vy~ (у = у). В левой части импликации имеем общезначимое формулу (лю - бые два различных числа не являются равными), в правой час - ти - ложная формула (любое число не равно самому себе).

Аналогично можно подобрать пример Ак1.: Зу (5 < у) ^ Зу (у < у). Левая часть импликации - истинная формула, где «5» - числовая константа, а правая часть импликации - ложная (так как утверждает существование числа меньшого самого себя). Заметим, что в примерах знаки = и < - это двухместные арифметические предикаты. Определение 1 (доказательства). Доказательством называется такая последовательность формул, в которой любая формула является либо аксиомой, либо формулой, полученной из предыдущих по одному из правил вывода. Определение 2 (доказуемой формулы). Последняя формула в последовательности формул, называемой доказательством, является доказуемой формулой. Аксиоматическая система должна удовлетворять некоторым методологическим требованиям, формулируемым в виде метатеорем, т. е. теоремах об аксиоматической системе. Теорема 1 (о непротиворечивости). Аксиоматическая система первопорядковой логики непротиворечива, т. е. не существует формулы такой, что d А и d ~А. Теорема 2 (корректности). Любая доказуемая формула в этой системе - общезначима. Теорема 3 (о полноте). Любая общезначимая формула в этой системе - доказуема. Доказательство этих теорем приводится в более обширных кур - сах логики. Замечание. В логической литературе используется и другая терминология: теоремой о полноте называется объединение двух теорем - теоремы 2 и теоремы 3.

<< | >>

↑

Источник: под ред. проф. В. Д. Бакулова, проф. А. Н. Ерыгина. Основы философии: учебник для бакалавров философских. 2009

Еще по теме Аксиоматическая система логики предикатов первого порядка: