Изменения
→Вычисление значений высказываний
[[Математическая логика | На главную <<]][[Лекция 3 | >>]]
[[Категория: Математическая логика]]
==Язык исчисления высказываний==
===Определения===
{{Определение
|definition=
Одним из базовых понятий логики высказываний является пропозициональная переменная — переменная, значением которой может быть логическое высказывание
}}
{{Определение
|definition=
<nowiki><пропозициональная переменная></nowiki> формально не определяется. Договоримся, что это - буква латинского алфавита (возможно, с нижним индексом).
}}
===Расстановка скобок===
Так построенная грамматика предписывает определенный способ расстановки
==Вычисление значений высказываний==
Зададим некоторое множество истинностных значений $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=<wikitex>Если дано некоторое высказывание $\alpha$, в котором используются пропозициональныепеременные $v_1 \dots v_n$, то ''оценку'' данного высказывания $|\left\vert\alpha|\right\vert$ мы определим
следующим рекурсивным образом.
* пропозициональная переменная $v_i$: $f_P (v_i)$
* конъюнкция выражений $\alpha$ и $\beta$: $f_\& (|\left\vert\alpha|\right\vert,|\left\vert\beta|\right\vert)$* дизъюнкция выражений $\alpha$ и $\beta$: $f_\vee (|\left\vert\alpha|\right\vert,|\left\vert\beta|\right\vert)$* импликация выражений $\alpha$ и $\beta$: $f_\to (|\left\vert\alpha|\right\vert,|\left\vert\beta|\right\vert)$* отрицание выражения $\alpha$: $f_\neg (|\left\vert\alpha|\right\vert)$* во всех остальных случаях оценка выражения равна оценке потомка в дереве.</wikitex>
}}
Любое выражение оценивается по этому определению
|proof=
различных фактов про выражения. Данное доказательство подходит для первого
варианта грамматики.
* термом --- при этом это не пропозициональная переменная, так как длина строки больше 1. Значит, это либо выражение в скобках --- тогда все доказано по предположению индукции, поскольку длина выражения в скобках --- $n-1$, либо отрицание. Тогда применение функции $f_\neg$ к оценке строки длины $n$ даст оценку выражения.
* импликацией, конъюнкцией или дизъюнкцией, при этом примененный вариант правила добавляет новые терминальные символы в строку. Значит, здесь дерево разбора разделит строку на две, причем длины строго меньшей, чем $n$. В этом случае очевидно, что значение выражения будет вычислено.
* выражением, импликацией, конъюнкцией или дизъюнкцией, при этом примененный вариант правила не добавляет новых терминальных символов. В этом случае, спустившись (возможно, несколько раз) вниз по дереву мы дойдем либо до терма, либо до вариантов правил для импликации, конъюнкции или дизъюнкции, добавляющих терминальные символы, и окажемся в условиях предыдущих пунктов.</wikitex>
}}
{{Определение
|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> - множество правил вывода
}}
Расширим грамматику из предыдущего раздела:
* <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>
|definition=
Исчисление высказываний - формальная система, использующая в качестве языка язык исчисления высказываний, в качестве аксиом - следующие схемы выражений:
, а правила вывода - все правила, порожденные согласованной заменой букв в <tex>\langle{}\phi, (\phi) \rightarrow (\psi), \psi\rangle</tex>.
}}
[[Категория: Математическая логика]]
