Выделяется подмножество формул, называемых аксиомами теории. Подмножество может быть и бесконечным; во всяком случае, оно должно быть разрешимо.

3. Задаются правила вывода теории. Правило вывода R(F₁, … ,F_n, σ) – это вычисляемое отношение на множестве формул. Если формулы F₁, … ,F_n, σ находятся в отношении R, то формула σ называется непосредственно выводимой из F₁, … ,F_n по правилу R.

Часто правило R(F₁, … ,F_n ,σ ) записывается в виде (F₁, … ,F_n)/σ. Формулы F₁, … , F_n называются посылками правила R, а σ – его следствием или заключением. Примеры аксиом и правил вывода будут приведены не­сколько позднее. Выводом формулы В из формул A₁, … ,A_n называется по­следовательность формул F₁, … , F_m, такая, что F_m=B, а любая F_ί (ί=1,2, … ,m) есть либо аксиома, либо одна из исходных формул А₁, … ,А_n, либо не­посредственно выводима из формул F₁, … ,F_ί-1 (или какого-нибудь из под­множеств) по одному из правил вывода. Если существует вывод В из А₁, …,А_n, то говорят, что В выводима из A₁, … ,A_n. Этот факт обозначается так: A₁, … ,A_n├ B. Формулы A₁, … ,A_n называются гипотезами или посыл­ками вывода. Переход в выводе от F_ί–1 к F_ί называется ί-м шагом вы­вода.

Доказательством формулы В в теории Т называется вывод В из пус­того множества формул, т.е. вывод, в котором в качестве исходных формул используются только аксиомы. Формула В, для которой существует доказа­тельство, называется формулой, доказуемой в теории Т, или теоремой тео­рии Т; факт доказуемости В обозначается ├ В.

Очевидно, что присоединение формул к гипотезам не нарушает выводи­мости. Поэтому если ├ В, то А ├ В, и если А₁, . . . ,А_n ├ В, то А₁, . . . , А_n, А_n+1├ В для любых А₁ и А_n+1. Порядок гипотез в списке несуще­ствен.

При изучении формальных теорий мы имеем дело с двумя типами вы­сказываний: во-первых, с высказываниями самой теории (теоремами), кото­рые рассматриваются как чисто формальные объекты, определенные ранее, а во-вторых, с высказываниями о теории (о свойствах ее теорем, доказа­тельств и т.д.), которые формулируются на языке, внешнем по отношению к теории, – метаязыке и называются метатеоремами. Различие между тео­ремами и метатеоремами не всегда будут проводиться явно, но его обяза­тельно надо иметь в виду.

Например, если удалось построить вывод В из А₁, . . . , А_n, то высказы­вание “А₁, . . . ,А_n ├ В ” является метатеоремой; ее можно рассматри­вать как дополнительное (“произвольное”) правило вывода, которое можно присоединить к исходным и использовать в дальнейшем.

Ясно, что общезначимые (тождественно-истинные) высказывания типа А Ú Ā или "´R(x) Þ R(Y), имеющие силу общих логических законов, должны содержаться в любой теории, претендующей на логический смысл. Поэтому изучение конкретных формальных теорий начнём с исчислений, порождаю­щих все общеизвестные формулы.