Формальный аксиоматический метод

Формальный аксиоматический метод отличается от неформального тем, что совершенно чётко определяет не только исходные понятия и записанные в виде аксиом исходные положения, но и дозволенные способы рассуждения. Точно указываются допустимые логические переходы. Более того, и аксиомы, и разрешённые логические переходы должны быть оформлены таким образом, чтобы первые можно было использовать, а вторые – делать чисто механически, не вникая в их содержание, так чтобы и то и другое было по силам исполнительному лаборанту, а теперь и компьютеру. Для этого нужно уметь оперировать с используемыми в доказательствах утверждениями, опираясь только на их внешний вид, а не на содержание, непонятное ни лаборанту, ни компьютеру. Такое оперирование довольно затруднительно, если утверждения записаны на естественном языке, т. е. на одном из тех языков, которыми пользуются люди в повседневной жизни. Приходится записывать утверждения на специальном языке, отражающем структуру утверждений.

Скажем, тот факт, что из A следует B, на русском языке может быть записан многими разными способами: «из A следует B», «из A вытекает B», «если A, то B», «B верно при условии, что верно A», «B верно при условии, что справедливо A», «B справедливо при условии, что верно А» – и ещё многими другими, которые, без сомнения, сможет предложить любезный читатель. Заставить компьютер во всём этом разбираться было бы слишком накладно. А ведь помимо русского языка существует ещё немало других. В специальном, искусственном языке математической логики (точнее было бы сказать – в одном из орфографических вариантов такого языка) указанный факт записывается так: (A ⇒ B). Аналогично, вместо того чтобы анализировать все способы, которыми в русском языке можно выразить тот факт, что утверждение A неверно, пишут просто ¬A.