2. Канонические системы

Канонические системы были изобретены Постом в 1941 году при попытке найти наиболее общий вид формальных систем, таких, например, как Principia Mathematica.

Будем предполагать, что дан список знаков и другой список символов, называемых переменными, и

отличных от знаков. Терм — это любая цепочка знаков и переменных, а производящая схема (короче, схема) — это фигура вида

где все суть термы. Термы называются посылками, заключением схемы. Схема без посылок называется аксиомой.

Каноническая система, или система Поста, состоит из списка знаков, списка переменных и конечного множества схем. Знаки образуют алфавит канонической системы.

Применение схемы получается из схемы путем подстановки цепочек знаков вместо всех переменных, причем вместо всех вхождений одной и той же переменной подставляется одна и та же цепочка.

Если дана каноническая система, то определим по индукции понятие доказательства некоторого слова, т. е. цепочки знаков.

1. Применение аксиомы — доказательство этого применения.

2. Если доказательства соответственно слов и

— применение некоторой схемы, то

-доказательство слова а.

Слово доказуемо в канонической системе, если мы можем найти его доказательство.

Пример. Слова, доказуемые в следующей системе Поста, — это в точности четные числа.

знак

переменная

схемы

Пример. Альтернирующие цепочки знаков

(см. скан)