Изменения

Формальная система - упорядоченная тройка <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>\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>.