Математическая логика и теория алгоритмов. Для изучающих компьютерные науки

Однако все же приведем аксиому параллельности как для евклидовой геометрии (аксиома Евклида), так и для неевклидовой геометрии (аксиома Лобачевского). Аксиома Евклида. Пусть а - произвольная прямая и ^ - точка, лежащая вне прямой а, тогда в плоскости, определенной точкой А и прямой а, можно провести не более одной прямой, проходящей через ^ и не пересекающей а. Аксиома Лобачевского. Пусть а - произвольная прямая и ^ - точка, лежащая вне прямой а, тогда в плоскости, определенной точкой А и прямой а, можно провести не менее двух прямых, не пересекающихся с заданной прямой а. Если примем первые четыре группы аксиом и аксиому Евклида, то получим евклидову геометрию. Если примем первые четыре группы аксиом и аксиому Лобачевского, то получим неевклидову геометрию (геометрию Лобачевского - Бойаи - Гаусса). Из аксиом логическими методами уже получаются теоремы геометрии, однако этим заниматься не будем. Еще раз отметим, что в полуформальной аксиоматической теории система логических правил, т.е. методы доказательств, считаются известными из опыта изучения математики. В математической практике аксиоматические теории обычно описываются, как и геометрия, в виде полуформальных теорий и предполагается, что логика, используемая в этой теории, есть та интуитивная логика, которая усваивается в ходе изучения математики. Для самой науки надобно было всегда желать, чтобы она стала на твёрдом основании, чтобы строгость и ясность сохранялись в самих её началах. Н. Лобачевский § 5. Формальные аксиоматические теории Как уже известно, формальная аксиоматическая теория В считается заданной, если: 1. Задано некоторое множество символов - алфавит теории В. Конечная последовательность букв алфавита называется выражением теории. Алфавит, следовательно, и выражения теории задаются эффективным образом. 2. Заданы формулы теории В как некоторое подмножество выражений теории. Формулы тоже обычно задаются эффективным образом. 3. Заданы аксиомы теории В как подмножество множества формул. Если аксиом конечное число, то их можно задать перечислением. Если же их бесконечное множество, то задают с помощью схем, т.е. правил построения аксиом. Если аксиомы заданы эффективным образом, то теория В называется эффективно аксиоматизированной. 106