Математическая логика и теория алгоритмов

вил, т.е. методы доказательств, считаются известными из опыта изу­ чения математики. В математической практике аксиоматические теории обычно описываются, как и геометрия, в виде полуформальных теорий и предполагается, что логика, используемая в этой теории, есть та интуитивная логика, которая усваивается в ходе изучени?! математики. Для самойнаукинадобно быловсегдажелать, чтобыона сталана твердом основании, чтобы строгость иясность сохранялись в амих ееначалах. Н. Лобачевский § 5. Формальные аксиоматические теории Как уже известно, формальная аксиоматическая теория В счита­ ется заданной, если: 1. Задано некоторое множество символов ~ алфавит теории В. Конечная последовательность букв алфавита называется выраясением теории. Алфавит, следовательно, и выражения теории задаются эф­ фективным образом. 2. Заданы формулы теории В как некоторое подмножество выражений теории. Формулы тоже обычно задаются эффективным образом. 3. Заданы аксиомы теории В как подмножество;множества фор­ мул. Если аксиом конечное число, то их можно задать перечислением. Если же их бесконечное множество, то задают с помощью схем, т.е. правил построения аксиом. Если аксиомы заданы эффективным обра­ зом, то теория В называется эффективно аксиоматизированной. 4. Задано конечное число правил вывода r\, rj,..., r „, согласно кадедому из которых некоторая формула, именуемая н е п о с р е д с т в е н - н ь шследствием (заключением), непосредственно выводима из неко­ торого конечного множества формул, называемых посылками. При этом для каждого i?, существует целое положительное к такое, что для 146