97
правок
Изменения
Нет описания правки
|definition=
Назовем выражение общезначимым, если его оценка истинна при любой оценке входящих в него пропозициональных переменных. Запись: <tex>\models \alpha</tex>.
}}
==Формальная система==
{{Определение
|definition=
Формальная система - упорядоченная тройка <tex><L, A, R></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><L, A, R></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>.
}}
