Исчисление высказываний — различия между версиями

Материал из Викиконспекты
Перейти к: навигация, поиск
м (rollbackEdits.php mass rollback)
 
(не показано 11 промежуточных версий 9 участников)
Строка 1: Строка 1:
[[Матлогика | На главную]][[Лекция 3 | >>]]
+
[[Математическая логика | На главную <<]][[Лекция 3 | >>]]
 +
 
 +
[[Категория: Математическая логика]]
  
 
==Язык исчисления высказываний==
 
==Язык исчисления высказываний==
 
===Определения===
 
===Определения===
 +
{{Определение
 +
|definition=
 +
Одним из базовых понятий логики высказываний является пропозициональная переменная — переменная, значением которой может быть логическое высказывание
 +
}}
 +
 
{{Определение
 
{{Определение
 
|definition=
 
|definition=
Строка 16: Строка 23:
 
<nowiki><пропозициональная переменная></nowiki> формально не определяется. Договоримся, что это - буква латинского алфавита (возможно, с нижним индексом).
 
<nowiki><пропозициональная переменная></nowiki> формально не определяется. Договоримся, что это - буква латинского алфавита (возможно, с нижним индексом).
 
}}
 
}}
 +
 
===Расстановка скобок===
 
===Расстановка скобок===
 
Так построенная грамматика предписывает определенный способ расстановки
 
Так построенная грамматика предписывает определенный способ расстановки
Строка 39: Строка 47:
  
 
==Вычисление значений высказываний==
 
==Вычисление значений высказываний==
<wikitex>Попробуем научиться вычислять значение высказываний.
+
Попробуем научиться вычислять значение высказываний.
 
Зададим некоторое множество истинностных значений $V$ и функции
 
Зададим некоторое множество истинностных значений $V$ и функции
 
оценки $f_\&, f_\vee, f_\to: V \times V \to V$, и $f_\neg: V \to V$,  
 
оценки $f_\&, f_\vee, f_\to: V \times V \to V$, и $f_\neg: V \to V$,  
 
по функции на каждую из связок и на отрицание. Также зададим ''оценку''
 
по функции на каждую из связок и на отрицание. Также зададим ''оценку''
 
переменных, функцию, сопоставляющую множеству переменных $P$ некоторого  
 
переменных, функцию, сопоставляющую множеству переменных $P$ некоторого  
высказывания $\alpha$ --- функцию $f_P: P \to V$.</wikitex>
+
высказывания $\alpha$ --- функцию $f_P: P \to V$.
  
 
{{Определение
 
{{Определение
|definition=<wikitex>Если дано некоторое высказывание $\alpha$, в котором используются пропозициональные
+
|definition=Если дано некоторое высказывание $\alpha$, в котором используются пропозициональные
переменные $v_1 \dots v_n$, то ''оценку'' данного высказывания $|\alpha|$ мы определим  
+
переменные $v_1 \dots v_n$, то ''оценку'' данного высказывания $\left\vert\alpha\right\vert$ мы определим  
 
следующим рекурсивным образом.
 
следующим рекурсивным образом.
  
Строка 54: Строка 62:
  
 
* пропозициональная переменная $v_i$: $f_P (v_i)$
 
* пропозициональная переменная $v_i$: $f_P (v_i)$
* конъюнкция выражений $\alpha$ и $\beta$: $f_\& (|\alpha|,|\beta|)$
+
* конъюнкция выражений $\alpha$ и $\beta$: $f_\& (\left\vert\alpha\right\vert,\left\vert\beta\right\vert)$
* дизъюнкция выражений $\alpha$ и $\beta$: $f_\vee (|\alpha|,|\beta|)$
+
* дизъюнкция выражений $\alpha$ и $\beta$: $f_\vee (\left\vert\alpha\right\vert,\left\vert\beta\right\vert)$
* импликация выражений $\alpha$ и $\beta$: $f_\to (|\alpha|,|\beta|)$
+
* импликация выражений $\alpha$ и $\beta$: $f_\to (\left\vert\alpha\right\vert,\left\vert\beta\right\vert)$
* отрицание выражения $\alpha$: $f_\neg (|\alpha|)$
+
* отрицание выражения $\alpha$: $f_\neg (\left\vert\alpha\right\vert)$
* во всех остальных случаях оценка выражения равна оценке потомка в дереве.</wikitex>
+
* во всех остальных случаях оценка выражения равна оценке потомка в дереве.
 
}}
 
}}
  
Строка 65: Строка 73:
 
Любое выражение оценивается по этому определению
 
Любое выражение оценивается по этому определению
 
|proof=
 
|proof=
<wikitex>Докажем индукцией по длине формулы, $n$; это традиционный способ доказательств
+
Докажем индукцией по длине формулы, $n$; это традиционный способ доказательств
 
различных фактов про выражения. Данное доказательство подходит для первого
 
различных фактов про выражения. Данное доказательство подходит для первого
 
варианта грамматики.
 
варианта грамматики.
Строка 75: Строка 83:
 
* термом --- при этом это не пропозициональная переменная, так как длина строки больше 1. Значит, это либо выражение в скобках --- тогда все доказано по предположению индукции, поскольку длина выражения в скобках --- $n-1$, либо отрицание. Тогда применение функции $f_\neg$ к оценке строки длины $n$ даст оценку выражения.
 
* термом --- при этом это не пропозициональная переменная, так как длина строки больше 1. Значит, это либо выражение в скобках --- тогда все доказано по предположению индукции, поскольку длина выражения в скобках --- $n-1$, либо отрицание. Тогда применение функции $f_\neg$ к оценке строки длины $n$ даст оценку выражения.
 
* импликацией, конъюнкцией или дизъюнкцией, при этом примененный вариант правила добавляет новые терминальные символы в строку. Значит, здесь дерево разбора разделит строку на две, причем длины строго меньшей, чем $n$. В этом случае очевидно, что значение выражения будет вычислено.
 
* импликацией, конъюнкцией или дизъюнкцией, при этом примененный вариант правила добавляет новые терминальные символы в строку. Значит, здесь дерево разбора разделит строку на две, причем длины строго меньшей, чем $n$. В этом случае очевидно, что значение выражения будет вычислено.
* выражением, импликацией, конъюнкцией или дизъюнкцией, при этом примененный вариант правила не добавляет новых терминальных символов. В этом случае, спустившись (возможно, несколько раз) вниз по дереву мы дойдем либо до терма, либо до вариантов правил для импликации, конъюнкции или дизъюнкции, добавляющих терминальные символы, и окажемся в условиях предыдущих пунктов.</wikitex>
+
* выражением, импликацией, конъюнкцией или дизъюнкцией, при этом примененный вариант правила не добавляет новых терминальных символов. В этом случае, спустившись (возможно, несколько раз) вниз по дереву мы дойдем либо до терма, либо до вариантов правил для импликации, конъюнкции или дизъюнкции, добавляющих терминальные символы, и окажемся в условиях предыдущих пунктов.
 
}}
 
}}
  
Строка 81: Строка 89:
  
 
{{Определение
 
{{Определение
 +
|id=valid
 
|definition=
 
|definition=
 
Назовем выражение общезначимым, если его оценка истинна при любой оценке входящих в него пропозициональных переменных. Запись: <tex>\models \alpha</tex>.
 
Назовем выражение общезначимым, если его оценка истинна при любой оценке входящих в него пропозициональных переменных. Запись: <tex>\models \alpha</tex>.
Строка 104: Строка 113:
  
 
Расширим грамматику из предыдущего раздела:
 
Расширим грамматику из предыдущего раздела:
* <nowiki><выражение></nowiki> ::= <nowiki><конъюнкция></nowiki><tex>| \psi | \phi | \pi</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>\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>
Строка 121: Строка 130:
 
|definition=
 
|definition=
 
Исчисление высказываний - формальная система, использующая в качестве языка язык исчисления высказываний, в качестве аксиом - следующие схемы выражений:
 
Исчисление высказываний - формальная система, использующая в качестве языка язык исчисления высказываний, в качестве аксиом - следующие схемы выражений:
*<tex>(\phi) \rightarrow ((\psi) \rightarrow (\phi))</tex>
+
#<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) \rightarrow (\psi) \rightarrow (\pi)) \rightarrow ((\phi) \rightarrow (\pi))</tex>
*<tex>(\phi) \rightarrow (\psi) \rightarrow (\phi) \& (\psi)</tex>
+
#<tex>(\phi) \rightarrow (\psi) \rightarrow (\phi) \& (\psi)</tex>
*<tex>(\phi) \& (\psi) \rightarrow (\phi)</tex>
+
#<tex>(\phi) \& (\psi) \rightarrow (\phi)</tex>
*<tex>(\phi) \& (\psi) \rightarrow (\psi)</tex>
+
#<tex>(\phi) \& (\psi) \rightarrow (\psi)</tex>
*<tex>(\phi) \rightarrow (\phi) \vee (\psi)</tex>
+
#<tex>(\phi) \rightarrow (\phi) \vee (\psi)</tex>
*<tex>(\psi) \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 (\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>((\phi) \rightarrow (\psi)) \rightarrow ((\phi) \rightarrow \neg (\psi)) \rightarrow \neg (\phi)</tex>
*<tex>\neg \neg (\phi) \rightarrow (\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>.  
 
}}
 
}}
 +
 +
[[Категория: Математическая логика]]

Текущая версия на 19:21, 4 сентября 2022

На главную << >>

Язык исчисления высказываний

Определения

Определение:
Одним из базовых понятий логики высказываний является пропозициональная переменная — переменная, значением которой может быть логическое высказывание


Определение:
Языком исчисления высказываний мы назовем язык [math]L[/math], порождаемый следующей грамматикой со стартовым нетерминалом <выражение>:
  • <выражение> ::= <импликация>
  • <импликация> ::= <дизъюнкция> [math]|[/math] <дизъюнкция> [math]\rightarrow[/math] <импликация>
  • <дизъюнкция> ::= <конъюнкция> [math]|[/math] <дизъюнкция> [math]\vee[/math] <конъюнкция>
  • <конъюнкция> ::= <терм> [math]|[/math] <конъюнкция> [math]\&[/math] <терм>
  • <терм> ::= <пропозициональная переменная> [math]|[/math] (<выражение>) [math]|[/math] [math]\neg[/math] <терм>


Определение:
<пропозициональная переменная> формально не определяется. Договоримся, что это - буква латинского алфавита (возможно, с нижним индексом).


Расстановка скобок

Так построенная грамматика предписывает определенный способ расстановки опущенных скобок, при этом скобки у конъюнкции и дизъюнкции расставляются слева направо, а у импликации --- справа налево (это соответствует традиционному чтению), так что выражение [math]A \rightarrow B\&C\&D \rightarrow E[/math] следует понимать как [math]A \rightarrow (((B\&C)\&D) \rightarrow E)[/math]. Все выражения, которые отличаются только наличием дополнительных незначащих скобок (не изменяющих порядок операций), мы будем считать одинаковыми.

Иногда полезно ограничивать свободу расстановки скобок:

  • <выражение> ::= <импликация>
  • <импликация> ::= <дизъюнкция> [math]|[/math] (<дизъюнкция> [math]\rightarrow[/math] <импликация>)
  • <дизъюнкция> ::= <конъюнкция> [math]|[/math] (<дизъюнкция> [math]\vee[/math] <конъюнкция>)
  • <конъюнкция> ::= <терм> [math]|[/math] (<конъюнкция> [math]\&[/math] <терм>)
  • <терм> ::= <пропозициональная переменная> [math]|[/math] (<выражение>) [math]|[/math] [math]\neg[/math] <терм>


Определение:
Высказывание - любая формула, порожденная данными грамматиками.


Вычисление значений высказываний

Попробуем научиться вычислять значение высказываний. Зададим некоторое множество истинностных значений $V$ и функции оценки $f_\&, f_\vee, f_\to: V \times V \to V$, и $f_\neg: V \to V$, по функции на каждую из связок и на отрицание. Также зададим оценку переменных, функцию, сопоставляющую множеству переменных $P$ некоторого высказывания $\alpha$ --- функцию $f_P: P \to V$.


Определение:
Если дано некоторое высказывание $\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)$
  • во всех остальных случаях оценка выражения равна оценке потомка в дереве.


Теорема:
Любое выражение оценивается по этому определению
Доказательство:
[math]\triangleright[/math]

Докажем индукцией по длине формулы, $n$; это традиционный способ доказательств различных фактов про выражения. Данное доказательство подходит для первого варианта грамматики.

База: $n=1$. Анализ грамматики показывает, что такая строка может состоять только из имени пропозициональной переменной. Очевидно, что указанный способ оценки позволяет такую строку оценить всегда.

Переход: пусть $n\ge 1$ и для $n$ все доказано. Рассмотрим строку длины $n+1$. В дереве разбора данной строки есть некоторый корень, рассмотрим его. Он может быть:

  • термом --- при этом это не пропозициональная переменная, так как длина строки больше 1. Значит, это либо выражение в скобках --- тогда все доказано по предположению индукции, поскольку длина выражения в скобках --- $n-1$, либо отрицание. Тогда применение функции $f_\neg$ к оценке строки длины $n$ даст оценку выражения.
  • импликацией, конъюнкцией или дизъюнкцией, при этом примененный вариант правила добавляет новые терминальные символы в строку. Значит, здесь дерево разбора разделит строку на две, причем длины строго меньшей, чем $n$. В этом случае очевидно, что значение выражения будет вычислено.
  • выражением, импликацией, конъюнкцией или дизъюнкцией, при этом примененный вариант правила не добавляет новых терминальных символов. В этом случае, спустившись (возможно, несколько раз) вниз по дереву мы дойдем либо до терма, либо до вариантов правил для импликации, конъюнкции или дизъюнкции, добавляющих терминальные символы, и окажемся в условиях предыдущих пунктов.
[math]\triangleleft[/math]

Зафиксируем множество истинностных значений [math]V[/math]. Почти всюду всегда достаточно [math]V = \{[/math]И, Л[math]\}[/math] (И - истина, Л - ложь). Зафиксируем оценки для связок ([math]\&, |, \rightarrow[/math]) и отрицания, придав им традиционные значения. В таком случае, единственный произвол в оценке выражения связан с выбором оценки пропозициональных переменных [math]f_p[/math].


Определение:
Назовем выражение общезначимым, если его оценка истинна при любой оценке входящих в него пропозициональных переменных. Запись: [math]\models \alpha[/math].


Формальная система

Определение:
Формальная система - упорядоченная тройка [math]\langle L, A, R \rangle[/math], где [math]L[/math] --- некоторый язык, [math]A \subset L[/math] --- множество аксиом, а [math]R \subset (L^2 \cup L^3 \cup ...)[/math] - множество правил вывода


Правило вывода (элемент [math]R[/math]) - упорядоченная [math]n[/math]-ка выражений, где первое [math]n - 1[/math] выражение --- посылка, а последнее --- заключение правила.


Определение:
Доказательство в формальной системе [math]\langle L, A, R \rangle[/math] - конечная последовательность выражений [math]\alpha_1, ..., \alpha_n[/math] из [math]L[/math], такая, что [math]\forall i \le n[/math] либо [math]\alpha_i \in A[/math], либо [math]\alpha_i[/math] получается с использованием правил вывода из предыдущих выражений.


Определение:
Высказывание [math]\alpha[/math] называется доказуемым, если существует доказательство [math]\alpha_1, ..., \alpha_k[/math], в котором [math]\alpha_k == \alpha[/math]. Запись: [math]\vdash \alpha[/math].


Расширим грамматику из предыдущего раздела:

  • <выражение> ::= <импликация>[math]| \psi | \phi | \pi[/math]
  • <импликация> ::= <дизъюнкция> [math]|[/math] <дизъюнкция> [math]\rightarrow[/math] <импликация>
  • <дизъюнкция> ::= <конъюнкция> [math]|[/math] <дизъюнкция> [math]\vee[/math] <конъюнкция>
  • <конъюнкция> ::= <терм> [math]|[/math] <конъюнкция> [math]\&[/math] <терм>
  • <терм> ::= <пропозициональная переменная> [math]|[/math] (<выражение>)

Назовем [math]\psi, \phi, \pi[/math] схемами выражений. Если вместо всех данных букв подставить корректные выражения из грамматики, получим корректное выражение. При этом, одинаковые буквы должны меняться на одинаковые выражения.


Определение:
Все выражения, полученные из схемы путем подстановки выражений вместо букв [math]\psi, \phi, \pi[/math], назовем выражениями, порожденными схемой.


Определение:
Исчисление высказываний - формальная система, использующая в качестве языка язык исчисления высказываний, в качестве аксиом - следующие схемы выражений:
  1. [math](\phi) \rightarrow ((\psi) \rightarrow (\phi))[/math]
  2. [math]((\phi) \rightarrow (\psi)) \rightarrow ((\phi) \rightarrow (\psi) \rightarrow (\pi)) \rightarrow ((\phi) \rightarrow (\pi))[/math]
  3. [math](\phi) \rightarrow (\psi) \rightarrow (\phi) \& (\psi)[/math]
  4. [math](\phi) \& (\psi) \rightarrow (\phi)[/math]
  5. [math](\phi) \& (\psi) \rightarrow (\psi)[/math]
  6. [math](\phi) \rightarrow (\phi) \vee (\psi)[/math]
  7. [math](\psi) \rightarrow (\phi) \vee (\psi)[/math]
  8. [math]((\phi) \rightarrow (\pi)) \rightarrow ((\psi) \rightarrow (\pi)) \rightarrow ((\phi) \vee (\psi) \rightarrow (\pi))[/math]
  9. [math]((\phi) \rightarrow (\psi)) \rightarrow ((\phi) \rightarrow \neg (\psi)) \rightarrow \neg (\phi)[/math]
  10. [math]\neg \neg (\phi) \rightarrow (\phi)[/math]
, а правила вывода - все правила, порожденные согласованной заменой букв в [math]\langle{}\phi, (\phi) \rightarrow (\psi), \psi\rangle[/math].