2. Понятие формальной теории

Хотя для проверки логических рассуждений можно использовать алгебру логики, сами рассуждения представляют собой цепочку утверждений, каждое из которых либо является исходной посылкой (постулатом, аксиомой, гипотезой), либо получается из предыдущих утверждений с помощью определённых правил - правил логического вывода. Эти правила вывода применяются к утверждениям формально, т.е., исходя только из их формы, структуры, а не содержания. Весь содержательный анализ происходит при формулировании аксиом. 

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

Наиболее убедительным примером применения аксиоматического метода явился математический трактат "Начала" древнегреческого математика Евклида (ок. 300 г. до н.э.). По примеру Евклида нидерландский философ Бенедикт Спиноза применил аксиоматический метод в своём основном труде «Этика, доказанная в геометрическом порядке» (1675), а великий русский учёный Михаил Ломоносов аксиоматически изложил основы физической химии.

Более двух тысяч лет учёные старались выяснить, какими же правилами вывода пользуются люди в логически правильных рассуждениях. Крупные достижения были сделаны и древнегреческими философами (Аристотель), и средневековыми европейскими схоластами, и учёными-логиками конца 19 - начала 20 века.

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

Чтобы задать формальную аксиоматическую теориюT, необходимо определить:

1. некоторое счётное множество символов (алфавит) – символов теории T (конечные последовательности символов теории T называются выражениями или словами теории T);

2. подмножество выражений теории T, называемых формулами;

3. подмножество формул теории T, называемых аксиомами;

4. конечное множество R1, R2, ..., Rm отношений между формулами, называемых правилами вывода.

Если формула A и формулы A1, A2, ..., Ai находятся в некотором отношении Rk, то A называется непосредственным следствием из формул A1, A2, ..., Ai, полученным по правилу Rk. Это обозначается так , при этом формулыA1, A2, ..., Ai называются посылками, формула A – заключением.

Выводом формулы A из формул F₁, …,F_k в теории T называется всякая последовательность A1, A2, ..., Ai, …,A_n формул такая, что A_n=A и для любого i формула A_i есть либо аксиома теории T, либо одна из формул F_j, либо непосредственное следствие из ранее полученных формул. Если в теории T существует вывод формулы A из формул F₁, …,F_k , то записывают это так F₁, …,F_k ├_T A, при этом формулы F₁, …,F_k называются гипотезами вывода.

Если ├_T A, то формула А называется теоремой теории T (т.е. выводима только из аксиом без гипотез). Вывод теоремы называется доказательством.