Исчисление высказываний — различия между версиями
Proshev (обсуждение | вклад) |
(minor fix wikitex) (Метки: правка с мобильного устройства, правка из мобильной версии) |
||
(не показано 6 промежуточных версий 5 участников) | |||
Строка 1: | Строка 1: | ||
− | [[ | + | [[Математическая логика | На главную <<]][[Лекция 3 | >>]] |
+ | |||
+ | [[Категория: Математическая логика]] | ||
==Язык исчисления высказываний== | ==Язык исчисления высказываний== | ||
Строка 53: | Строка 55: | ||
{{Определение | {{Определение | ||
− | |definition= | + | |definition=Если дано некоторое высказывание $\alpha$, в котором используются пропозициональные |
переменные $v_1 \dots v_n$, то ''оценку'' данного высказывания $|\alpha|$ мы определим | переменные $v_1 \dots v_n$, то ''оценку'' данного высказывания $|\alpha|$ мы определим | ||
следующим рекурсивным образом. | следующим рекурсивным образом. | ||
Строка 64: | Строка 66: | ||
* импликация выражений $\alpha$ и $\beta$: $f_\to (|\alpha|,|\beta|)$ | * импликация выражений $\alpha$ и $\beta$: $f_\to (|\alpha|,|\beta|)$ | ||
* отрицание выражения $\alpha$: $f_\neg (|\alpha|)$ | * отрицание выражения $\alpha$: $f_\neg (|\alpha|)$ | ||
− | * во всех остальных случаях оценка выражения равна оценке потомка в дереве. | + | * во всех остальных случаях оценка выражения равна оценке потомка в дереве. |
}} | }} | ||
Строка 87: | Строка 89: | ||
{{Определение | {{Определение | ||
+ | |id=valid | ||
|definition= | |definition= | ||
Назовем выражение общезначимым, если его оценка истинна при любой оценке входящих в него пропозициональных переменных. Запись: <tex>\models \alpha</tex>. | Назовем выражение общезначимым, если его оценка истинна при любой оценке входящих в него пропозициональных переменных. Запись: <tex>\models \alpha</tex>. | ||
Строка 110: | Строка 113: | ||
Расширим грамматику из предыдущего раздела: | Расширим грамматику из предыдущего раздела: | ||
− | * <nowiki><выражение></nowiki> ::= <nowiki>< | + | * <nowiki><выражение></nowiki> ::= <nowiki><импликация></nowiki><tex>| \psi | \phi | \pi</tex> |
− | * <nowiki>< | + | * <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>\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>\&</tex> <nowiki><терм></nowiki> | ||
Строка 127: | Строка 130: | ||
|definition= | |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>. | , а правила вывода - все правила, порожденные согласованной заменой букв в <tex>\langle{}\phi, (\phi) \rightarrow (\psi), \psi\rangle</tex>. | ||
}} | }} | ||
[[Категория: Математическая логика]] | [[Категория: Математическая логика]] |
Версия 14:29, 6 февраля 2019
Содержание
Язык исчисления высказываний
Определения
Определение: |
Одним из базовых понятий логики высказываний является пропозициональная переменная — переменная, значением которой может быть логическое высказывание |
Определение: |
Языком исчисления высказываний мы назовем язык
| , порождаемый следующей грамматикой со стартовым нетерминалом <выражение>:
Определение: |
<пропозициональная переменная> формально не определяется. Договоримся, что это - буква латинского алфавита (возможно, с нижним индексом). |
Расстановка скобок
Так построенная грамматика предписывает определенный способ расстановки опущенных скобок, при этом скобки у конъюнкции и дизъюнкции расставляются слева направо, а у импликации --- справа налево (это соответствует традиционному чтению), так что выражение
следует понимать как . Все выражения, которые отличаются только наличием дополнительных незначащих скобок (не изменяющих порядок операций), мы будем считать одинаковыми.Иногда полезно ограничивать свободу расстановки скобок:
- <выражение> ::= <импликация>
- <импликация> ::= <дизъюнкция> (<дизъюнкция> <импликация>)
- <дизъюнкция> ::= <конъюнкция> (<дизъюнкция> <конъюнкция>)
- <конъюнкция> ::= <терм> (<конъюнкция> <терм>)
- <терм> ::= <пропозициональная переменная> (<выражение>) <терм>
Определение: |
Высказывание - любая формула, порожденная данными грамматиками. |
Вычисление значений высказываний
<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>
Определение: |
Если дано некоторое высказывание $\alpha$, в котором используются пропозициональные переменные $v_1 \dots v_n$, то оценку данного высказывания $ |
Теорема: |
Любое выражение оценивается по этому определению |
Доказательство: |
<wikitex>Докажем индукцией по длине формулы, $n$; это традиционный способ доказательств различных фактов про выражения. Данное доказательство подходит для первого варианта грамматики. База: $n=1$. Анализ грамматики показывает, что такая строка может состоять только из имени пропозициональной переменной. Очевидно, что указанный способ оценки позволяет такую строку оценить всегда. Переход: пусть $n\ge 1$ и для $n$ все доказано. Рассмотрим строку длины $n+1$. В дереве разбора данной строки есть некоторый корень, рассмотрим его. Он может быть:
|
Зафиксируем множество истинностных значений всюду всегда достаточно И, Л (И - истина, Л - ложь). Зафиксируем оценки для связок ( ) и отрицания, придав им традиционные значения. В таком случае, единственный произвол в оценке выражения связан с выбором оценки пропозициональных переменных .
Определение: |
Назовем выражение общезначимым, если его оценка истинна при любой оценке входящих в него пропозициональных переменных. Запись: | .
Формальная система
Определение: |
Формальная система - упорядоченная тройка | , где --- некоторый язык, --- множество аксиом, а - множество правил вывода
Правило вывода (элемент ) - упорядоченная -ка выражений, где первое выражение --- посылка, а последнее --- заключение правила.
Определение: |
Доказательство в формальной системе | - конечная последовательность выражений из , такая, что либо , либо получается с использованием правил вывода из предыдущих выражений.
Определение: |
Высказывание | называется доказуемым, если существует доказательство , в котором . Запись: .
Расширим грамматику из предыдущего раздела:
- <выражение> ::= <импликация>
- <импликация> ::= <дизъюнкция> <дизъюнкция> <импликация>
- <дизъюнкция> ::= <конъюнкция> <дизъюнкция> <конъюнкция>
- <конъюнкция> ::= <терм> <конъюнкция> <терм>
- <терм> ::= <пропозициональная переменная> (<выражение>)
Назовем
схемами выражений. Если вместо всех данных букв подставить корректные выражения из грамматики, получим корректное выражение. При этом, одинаковые буквы должны меняться на одинаковые выражения.
Определение: |
Все выражения, полученные из схемы путем подстановки выражений вместо букв | , назовем выражениями, порожденными схемой.
Определение: |
Исчисление высказываний - формальная система, использующая в качестве языка язык исчисления высказываний, в качестве аксиом - следующие схемы выражений:
|