Изменения
minor fix wikitex
[[Математическая логика | На главную <<]][[Лекция 3 | >>]]
[[Категория: Математическая логика]]
==Язык исчисления высказываний==
===Определения===
{{Определение
|definition=
Одним из базовых понятий логики высказываний является пропозициональная переменная — переменная, значением которой может быть логическое высказывание
}}
{{Определение
|definition=
<nowiki><пропозициональная переменная></nowiki> формально не определяется. Договоримся, что это - буква латинского алфавита (возможно, с нижним индексом).
}}
===Расстановка скобок===
Так построенная грамматика предписывает определенный способ расстановки
''Высказывание'' - любая формула, порожденная данными грамматиками.
}}
==Вычисление значений высказываний==
<wikitex>Попробуем научиться вычислять значение высказываний.
Зададим некоторое множество истинностных значений $V$ и функции
оценки $f_\&, f_\vee, f_\to: V \times V \to V$, и $f_\neg: V \to V$,
по функции на каждую из связок и на отрицание. Также зададим ''оценку''
переменных, функцию, сопоставляющую множеству переменных $P$ некоторого
высказывания $\alpha$ --- функцию $f_P: P \to V$.</wikitex>
{{Определение
|definition=Если дано некоторое высказывание $\alpha$, в котором используются пропозициональные
переменные $v_1 \dots v_n$, то ''оценку'' данного высказывания $|\alpha|$ мы определим
следующим рекурсивным образом.
Возьмем дерево разбора высказывания, и возьмем его корень. В зависимости от правила, по которому получен корень, результатом оценки мы назовем:
* пропозициональная переменная $v_i$: $f_P (v_i)$
* конъюнкция выражений $\alpha$ и $\beta$: $f_\& (|\alpha|,|\beta|)$
* дизъюнкция выражений $\alpha$ и $\beta$: $f_\vee (|\alpha|,|\beta|)$
* импликация выражений $\alpha$ и $\beta$: $f_\to (|\alpha|,|\beta|)$
* отрицание выражения $\alpha$: $f_\neg (|\alpha|)$
* во всех остальных случаях оценка выражения равна оценке потомка в дереве.
}}
{{Теорема
|statement=
Любое выражение оценивается по этому определению
|proof=
<wikitex>Докажем индукцией по длине формулы, $n$; это традиционный способ доказательств
различных фактов про выражения. Данное доказательство подходит для первого
варианта грамматики.
База: $n=1$. Анализ грамматики показывает, что такая строка может состоять только из имени пропозициональной переменной. Очевидно, что указанный способ оценки позволяет такую строку оценить всегда.
Переход: пусть $n\ge 1$ и для $n$ все доказано. Рассмотрим строку длины $n+1$.
В дереве разбора данной строки есть некоторый корень, рассмотрим его. Он может быть:
* термом --- при этом это не пропозициональная переменная, так как длина строки больше 1. Значит, это либо выражение в скобках --- тогда все доказано по предположению индукции, поскольку длина выражения в скобках --- $n-1$, либо отрицание. Тогда применение функции $f_\neg$ к оценке строки длины $n$ даст оценку выражения.
* импликацией, конъюнкцией или дизъюнкцией, при этом примененный вариант правила добавляет новые терминальные символы в строку. Значит, здесь дерево разбора разделит строку на две, причем длины строго меньшей, чем $n$. В этом случае очевидно, что значение выражения будет вычислено.
* выражением, импликацией, конъюнкцией или дизъюнкцией, при этом примененный вариант правила не добавляет новых терминальных символов. В этом случае, спустившись (возможно, несколько раз) вниз по дереву мы дойдем либо до терма, либо до вариантов правил для импликации, конъюнкции или дизъюнкции, добавляющих терминальные символы, и окажемся в условиях предыдущих пунктов.</wikitex>
}}
Зафиксируем множество истинностных значений <tex>V</tex>. Почти <s>всюду</s> всегда достаточно <tex>V = \{</tex>И, Л<tex>\}</tex> (И - истина, Л - ложь). Зафиксируем оценки для связок (<tex>\&, |, \rightarrow</tex>) и отрицания, придав им традиционные значения. В таком случае, единственный произвол в оценке выражения связан с выбором оценки пропозициональных переменных <tex>f_p</tex>.
{{Определение
|id=valid
|definition=
Назовем выражение общезначимым, если его оценка истинна при любой оценке входящих в него пропозициональных переменных. Запись: <tex>\models \alpha</tex>.
}}
==Формальная система==
{{Определение
|definition=
Формальная система - упорядоченная тройка <tex>\langle L, A, R \rangle</tex>, где <tex>L</tex> --- некоторый язык, <tex>A \subset L</tex> --- множество аксиом, а <tex>R \subset (L^2 \cup L^3 \cup ...)</tex> - множество правил вывода
}}
Правило вывода (элемент <tex>R</tex>) - упорядоченная <tex>n</tex>-ка выражений, где первое <tex>n - 1</tex> выражение --- посылка, а последнее --- заключение правила.
{{Определение
|definition=
Доказательство в формальной системе <tex>\langle L, A, R \rangle</tex> - конечная последовательность выражений <tex>\alpha_1, ..., \alpha_n</tex> из <tex>L</tex>, такая, что <tex>\forall i \le n</tex> либо <tex>\alpha_i \in A</tex>, либо <tex>\alpha_i</tex> получается с использованием правил вывода из предыдущих выражений.
}}
{{Определение
|definition=
Высказывание <tex>\alpha</tex> называется доказуемым, если существует доказательство <tex>\alpha_1, ..., \alpha_k</tex>, в котором <tex>\alpha_k == \alpha</tex>. Запись: <tex>\vdash \alpha</tex>.
}}
Расширим грамматику из предыдущего раздела:
* <nowiki><выражение></nowiki> ::= <nowiki><импликация></nowiki><tex>| \psi | \phi | \pi</tex>
* <nowiki><импликация></nowiki> ::= <nowiki><дизъюнкция></nowiki> <tex>|</tex> <nowiki><дизъюнкция></nowiki> <tex>\rightarrow</tex> <nowiki><импликация></nowiki>
* <nowiki><дизъюнкция></nowiki> ::= <nowiki><конъюнкция></nowiki> <tex>|</tex> <nowiki><дизъюнкция></nowiki> <tex>\vee</tex> <nowiki><конъюнкция></nowiki>
* <nowiki><конъюнкция></nowiki> ::= <nowiki><терм></nowiki> <tex>|</tex> <nowiki><конъюнкция></nowiki> <tex>\&</tex> <nowiki><терм></nowiki>
* <nowiki><терм></nowiki> ::= <nowiki><пропозициональная переменная></nowiki> <tex>|</tex> (<nowiki><выражение></nowiki>)
Назовем <tex>\psi, \phi, \pi</tex> ''схемами выражений''. Если вместо ''всех'' данных букв подставить корректные выражения из грамматики, получим корректное выражение. При этом, одинаковые буквы должны меняться на одинаковые выражения.
{{Определение
|definition=
Все выражения, полученные из схемы путем подстановки выражений вместо букв <tex>\psi, \phi, \pi</tex>, назовем выражениями, '''порожденными''' схемой.
}}
{{Определение
|definition=
Исчисление высказываний - формальная система, использующая в качестве языка язык исчисления высказываний, в качестве аксиом - следующие схемы выражений:
#<tex>(\phi) \rightarrow ((\psi) \rightarrow (\phi))</tex>
#<tex>((\phi) \rightarrow (\psi)) \rightarrow ((\phi) \rightarrow (\psi) \rightarrow (\pi)) \rightarrow ((\phi) \rightarrow (\pi))</tex>
#<tex>(\phi) \rightarrow (\psi) \rightarrow (\phi) \& (\psi)</tex>
#<tex>(\phi) \& (\psi) \rightarrow (\phi)</tex>
#<tex>(\phi) \& (\psi) \rightarrow (\psi)</tex>
#<tex>(\phi) \rightarrow (\phi) \vee (\psi)</tex>
#<tex>(\psi) \rightarrow (\phi) \vee (\psi)</tex>
#<tex>((\phi) \rightarrow (\pi)) \rightarrow ((\psi) \rightarrow (\pi)) \rightarrow ((\phi) \vee (\psi) \rightarrow (\pi))</tex>
#<tex>((\phi) \rightarrow (\psi)) \rightarrow ((\phi) \rightarrow \neg (\psi)) \rightarrow \neg (\phi)</tex>
#<tex>\neg \neg (\phi) \rightarrow (\phi)</tex>
, а правила вывода - все правила, порожденные согласованной заменой букв в <tex>\langle{}\phi, (\phi) \rightarrow (\psi), \psi\rangle</tex>.
}}
[[Категория: Математическая логика]]
