С. В. Попов об устранимости аксиомы индукции



Скачать 257.1 Kb.
страница1/4
Дата08.11.2012
Размер257.1 Kb.
ТипДокументы
  1   2   3   4



РОССИЙСКАЯ АКАДЕМИЯ НАУК

ОРДЕНА ЛЕНИНА ИНСТИТУТ ПРИКЛАДНОЙ МАТЕМАТИКИ

ИМЕНИ М.В. КЕЛДЫША


С.В.Попов
ОБ УСТРАНИМОСТИ АКСИОМЫ ИНДУКЦИИ


Москва, 2005г.


УДК 517.5

Попов С.В. Об устранимости аксиомы индукции. Препринт Института прикладной математики им. М.В. Келдыша РАН. Москва, 2005г.

Устанавливается, что в арифметических доказательствах формул, которые не содержат индивидных переменных, устранима аксиома индукции.
Popov S.V. About eliminating of induction axiom. Preprint of the Keldysh Institute of Applied Mathematics of RAS. Moscow, 2005.

It is established, that in arithmetic proofs of formulas which do not contain individual variables, the axiom of an induction is eliminated.

ИМП им. М.В. Келдыша РАН. Москва, 2005г.


Введение. Рассматривается формальная арифметика S, содержащая константу 0, числовые переменные, равенство, функциональные символы + (сложения), (умножения) и  (прибавления 1) и логические связки. Термы строятся из константы 0 и переменных с помощью функциональных символов. В частности, натуральные числа изображаются термами вида

0 . Атомарные формулы – это равенства термов; остальные формулы строятся с помощью логических связок и кванторов.

Исчисление базируется на классическом исчислении предикатов и включает следующие дополнительные аксиомы: x = y  x = y; ( x = 0); x = y  .x = zy = z; x = y x = y; x + 0 = x; x + y = (x = y); x 0 = 0; x y = (x y) + x и схему индукции (АИ): A(0)  .x(A(x)  A(x)  xA(x). Логическое исчисление первого порядка выглядит не совсем обычно, что объясняется требованием выделить характерные свойства выводов, которые позволяют сформулировать основной результат работы, состоящий в том, что при доказательстве фундаментальных формул (т.е. формул без переменных) можно обойтись без АИ.

Формулы первого порядка строятся над базисом , f, . Для наглядности, формулы вида X1  .X2  . ...  .Xn X, n  0 представляются в виде Г  Х, используя знак  в качестве многоместной импликации. При этом порядок посылок Г = {X1, X2, ..., Xn} несущественен.

Единственная аксиомная схема логического исчисления имеет вид: ХХ.
При этом формула Х называется заключением аксиомы. Правила исчисления следующие:

обобщенное правило modus ponens

Г1  .Х Y Г2Х (здесь Г = Г1  Г2)

Г  Y
снятие двойного отрицания

Г  .(Х f) f

Г  X

положительное кванторное правило

Г  Х(a) (переменная а не входит в Г)

Г  xX(x)

отрицательное кванторное правило

Г  .( (y)) . ( Х(t))  Y (t - произвольный терм)

Г  . ((y))  Y
Достаточно просто показать, что это исчисление совпадает с классическим.
1. Определение синтаксического дерева. Определим более компактную форму вывода в приведенном исчислении (т.н. синтаксическое дерево), что позволит установить ряд свойств выводов, которые трудно заметить при обычном определении.

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

1. Корню с.д. DU приписана формула U, висячим узлам - аксиомы, остальным узлам формулы, вид которых определяется типом узлов, которым они приписаны. В аксиоме ХХ обе формулы Х называются двойственными.

2. Каждый не висячий узел DU является либо В-узлом, либо З-узлом, либо положительным кванторным узлом, либо отрицательным кванторным узлом.
В-узлом называется следующая конструкция.

Самому В-узлу приписана формула Г  .(Х1 .Х2 . ...  .Хn Х)  Х, а непосредственно выше расположены в точности n узлов, каждому из которых приписана единственная формула, полученная из Г  .(Х1  .Х2 . ... .Хn Х)  Хi, i = 1, 2, ..., n отбрасыванием некоторых посылок. При этом для данного В-узла формула Х называется изменяемой, а Х1 .Х2. ... .Хn Х - используемой. Два вхождения формулы Х – заключение используемой формулы и изменяемая формула, называются двойственными.
З-узлом называется следующая конструкция.

Самому З-узлу приписана формула Г  Х, а непосредственно выше расположен в точности один узел, которому приписана формула, полученная выбрасыванием некоторых посылок из Г  .(Х f) f. При этом формула Х называется запоминаемой.
Положительным кванторным узлом (обозначается +) называется следующая конструкция.

Самому +-узлу приписана формула Г  xX(x), а непосредственно выше расположен единственный узел, которому приписана формула, полученная из Г  Х(a) выбрасыванием некоторого числа ее посылок. При этом переменная а (собственная переменная этого узла) не входит в Г.
Отрицательным кванторным узлом (обозначается -) называется следующая конструкция.

Самому --узлу приписана формула Г  .((y))  Y, а непосредственно выше расположен единственный узел, которому приписана формула, полученная из формулы

Г  .( (y)) . ( Х(t))  Y

выбрасыванием некоторого числа посылок. При этом терм t называется собственным для этого узла.
Будем представлять синтаксические деревья в виде, который обычно принят при изображении выводов в виде деревьев. Так, если формулы А1, А2, …, Аn располагаются непосредственно выше формулы В, то будем представлять это так:

А1, А2, …, Аn
  1   2   3   4

Похожие:

С. В. Попов об устранимости аксиомы индукции iconЛекция аксиомы Единства
Анонс. В 1831 году английский физик Майкл Фарадей открыл закон электромагнитной индукции – экспериментальный фундамент существующей...
С. В. Попов об устранимости аксиомы индукции iconЛекция аксиомы Единства Посвящается искателям научных истин
Анонс. В 1831 году английский физик Майкл Фарадей открыл закон электромагнитной индукции – экспериментальный фундамент существующей...
С. В. Попов об устранимости аксиомы индукции iconПроблема индукции: опыт генерализации
Но теории индукции в различных дисциплинах являются специальными, не связанными друг с другом. Поэтому представляется возможным поставить...
С. В. Попов об устранимости аксиомы индукции iconАксиоматическая теория множеств
Наследственно конечные множества – интерпретация, в которой истинны все аксиомы, кроме аксиомы бесконечности
С. В. Попов об устранимости аксиомы индукции icon«Аксиомы стереометрии и некоторые следствия из них» Вопросы. Три аксиомы стереометрии: сформулировать аксиомы
...
С. В. Попов об устранимости аксиомы индукции iconЛабораторная работа №4 определение взаимной индуктивности контуров (катушек)
Изучение явлений электромагнитной индукции, самоиндукции, взаимной индукции; экспериментальная проверка закона электромагнитной индукции...
С. В. Попов об устранимости аксиомы индукции iconИ соотношение л. Л. Попов, Ю. И. Мигачев, С. В. Тихомиров
Лев Леонидович Попов заслуженный деятель науки Российской Федерации, доктор юридических наук, профессор
С. В. Попов об устранимости аксиомы индукции iconАксиомы кольца, аксиомы поля. Примеры колец и полей (поле из двух элементов)
Пусть r непустое множество. В r введены 2 операции: сложение и умножение. Эти операции бинарны: +
С. В. Попов об устранимости аксиомы индукции iconРассказ первого экскурсовода [1], [2], [3], [5], [7] Попов Александр Степанович 16. 03. 1859 13. 01. 1906
Попов родился в поселке Турьинские Рудники Пермской губернии на Урале. Отец Александра был священником
С. В. Попов об устранимости аксиомы индукции iconЛекция №25 электромагнитная индукция план
Опыт Фарадея. Магнитный поток. Эдс индукции. Вывод основного закона электромагнитной индукции. Правило Ленца. Токи Фуко
Разместите кнопку на своём сайте:
ru.convdocs.org


База данных защищена авторским правом ©ru.convdocs.org 2016
обратиться к администрации
ru.convdocs.org