Аксиоматический метод в логике высказываний и формализация математических теорий

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

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

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

Правило отделения:
"Если истинно утверждение j и истинно, что из j следует y, то истинно и утверждение y".
Формально это правило записывается в следующей форме:

Правило силлогизма:
"Если истинно утверждение, что из j следует y, и истинно утверждение, что из y следует x, то истинно и утверждение, что из j следует x" или, формально,

Правило эквивалентной замены:
"Если утверждение j истинно и в него входит утверждение y, о котором известно, что оно эквивалентно другому утверждению x, то истинно и утверждение, полученное из j заменой любых вхождений y на x" или, формально,

Это правило аналогично часто используемому в математике правилу замены "на равное"

Правило подстановки:
"Если утверждение j истинно независимо от истинности или ложности входящего в него утверждения y, то истинно и утверждение, полученное из j заменой всех вхождений y на любое утверждение x" или, формально,

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