Главная страница Случайная страница
Разделы сайта
АвтомобилиАстрономияБиологияГеографияДом и садДругие языкиДругоеИнформатикаИсторияКультураЛитератураЛогикаМатематикаМедицинаМеталлургияМеханикаОбразованиеОхрана трудаПедагогикаПолитикаПравоПсихологияРелигияРиторикаСоциологияСпортСтроительствоТехнологияТуризмФизикаФилософияФинансыХимияЧерчениеЭкологияЭкономикаЭлектроника
А) Принцип разрешимости
|
|
Анализируя принцип разрешимости, отметим, что логический язык должен обладать процедурой, позволяющей эффективно, то есть за конечное число шагов, устанавливать, является ли произвольная формула данного языка логическим законом или нет.
Особенность принципа разрешимости в аксиоматическом исчислении высказываний связана с тем, что при аксиоматизации логики высказываний главной задачей является систематизация логических законов. Множество законов задается здесь не в виде совокупности, а в виде выведения их из некоторых исходных заонов с помощью правил вывода. То есть в аксиоматическом исчислении высказываний разрешающая процедура для конкретных формул обеспечивается построением их доказательства.
Опишем принцип разрешения посредством доказательства соответствующих метатеорем (сокращенно - МТ).
Существет всего четыре метатеоремы:
МТ1 - |- А Þ |= А [20] (читается: «если А доказуемо, то А тождественно истинно»);
МТ2 - ù |= А Þ ù |- А (читается: «если А не тождественно истинно, то А
и не доказуемо»);
МТ3 - |= А Þ |- А (читается: «если А тождественно истинно, то А
и доказуемо»);
МТ4 - ù |- А Þ ù |= А (читается: «если А не доказуемо, то А и не тождественно
истинно»).
Рассмотрим поочередно каждую из приведенных метатеорем.
МТ1 |- А Þ |= А
Из приведенной выше структуры S2 видно, что множество тавтологий включает в себя подмножества аксиом и теорем.
Как известно, если |= А и |= А É В, то |= В; если |=А (x1, x2,... xn), то
|= А¢ (B1, B2,... Bn); то есть применение правил вывода MP и п/п обеспечивает сохранение свойства «быть тавтологией». В таком случае, если каждая аксиома – это тавтология и применение правил вывода сохраняет свойство «быть тавтологией», то в силу определения понятия доказательства каждая теорема является тавтологией.
МТ2 Ø |= А Þ Ø |- А.
Доказательство.
1. (А É В) É (Ø В É Ø А) - А 10
2. (|- А É |= А) Þ (Ø |= А É Ø |- А) - п/п к 1: A/ |- А, В/ |= А
3. |- А Þ |= А - МТ1
4. Ø |= А Þ Ø |- А - МР к 2, 3
МТ3 |= А Þ |- А.
Данная метатеорема принимается без доказательства[21].
МТ4 Ø |- А Þ Ø |= А.
Доказательство.
1. (А É В) É (Ø В É Ø А) - А 10
2. (|= А Þ |- А) Þ É (Ø |- А Þ Ø |= А) - п/п к 10: А/ |= А, В/ |- А
3. |= А Þ |- А - МТ3
4. Ø |- А Þ Ø |= А - МР к 2, 3
Таким образом, доказав МТ1 – МТ4, мы пришли к выводу, что в S2 множество выводимых формул совпадает с множеством тавтологий.
Б) Принцип непротиворечивости
Принцип непротиворечивости формулируется относительно:
Теорем;
Правил вывода;
|
|