Изменения

Формальная система - упорядоченная тройка <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><\langle L, A, R>\rangle</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> получается с использованием правил вывода из предыдущих выражений.

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