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

Вид материала

Реферат

Содержание Math. Annalen Revue de Métaphysique et de Morale Revue de Métaphysique et de Morale Formulaire Mathématique Grundgesetze der Arithmetik Principles of Mathematics American Journal of Mathematics Proc. London Math. Soc

Подобный материал:

• Рабочей программы учебной дисциплины дв2 Математическая логика и теория алгоритмов, 50.1kb.
• Математическая логика, 1012.22kb.
• Рабочая программа по дисциплине в 2-Математическая логика и теория алгоритмов шифр, 316.78kb.
• Программы кандидатского экзамена по специальности 01. 01. 06 "Математическая логика,, 50.44kb.
• Рабочая учебная программа по дисциплине математическая логика, 72.41kb.
• Рабочая учебная программа по дисциплине «Математическая логика и теория алгоритмов», 69.99kb.
• Н. В. Папуловская Математическая логика Методическое пособие, 786.38kb.
• Уакиев Валериан Савирович рекомендуемая литература, 334.04kb.
• Аннотация программы учебной дисциплины «Дискретная математика и математическая логика, 55.65kb.
• Рабочей программы дисциплины математическая логика по направлению подготовки 220400, 21.67kb.

:   C‘P . ! . _ . !( – ‘‘)} Df.;


т.е. P порождает вполне упорядоченные ряды, если Р есть отношение ряда, и любой класс , содержащийся в поле Р и не являющийся нулевым, имеет первый член. (Отметим, что ‘‘ суть члены, входящие после некоторого члена ).

Если как No‘P обозначить ординальное число вполне упорядоченного отношения Р, а как NO класс ординальных чисел, то мы получим:


No = {P .  = ‘P} Df.,

NO = No‘‘.


Из определения No мы получаем:


├ : P  .  . No‘P = ‘P ,

├ : (P ) .  . E!No‘P.


Если теперь мы проверим наши определения с точки зрения их связи с теорией типов, мы увидим, прежде всего, что определения ‘Ser’ и  включают поля отношений ряда. Поле же значимо только тогда, когда отношение является однородным; следовательно, отношения, которые не являются однородными, не порождают ряд. Например, можно подумать, что отношение  порождает ряд ординального числа , типа


x, ‘x, ‘‘x, … ⁿ‘x, …,


и этим способом мы можем попытаться доказать существование  и א₀. Но х и ‘x относятся к различным типам и, следовательно, согласно нашему определению, такого ряда нет. Ординальное число ряда индивидов, согласно приведённому выше определению No, есть класс отношений индивидов. Следовательно, он по типу отличается от любого индивида, и не может образовывать часть какого-то ряда, в котором встречаются индивиды. Опять же, предположим, что все конечные ординалы имеют место как ординальные числа индивидов; т.е. как ординалы рядов индивидов. Тогда, конечные ординалы сами образуют ряд, чьё ординальное число есть ; таким образом,  существует как ординальное число ординалов, т.е. как ординал ряда ординалов. Но тип ординального числа ординалов – это тип классов отношений классов отношений индивидов. Таким образом, существование  доказывалось в рамках более высокого типа, чем тип конечных ординалов. Опять таки, кардинальное число ординальных чисел вполне упорядоченного ряда, который может быть создан из конечных ординалов, есть א₁; следовательно, א₁ имеет место в типе классов классов классов отношений классов отношений индивидов. К тому же, ординальные числа вполне упорядоченных рядов, составленных из конечных ординалов, могут быть упорядочены в порядке величины, и результатом будет вполне упорядоченный ряд, чьё ординальное число есть ₁. Следовательно, ₁ имеет место как ординальное число ординалов ординалов. Этот процесс можно повторить любое конечное число раз и, таким образом, мы можем в соответствующих типах установить существование א_n и _n для любого конечного значения n.

Но вышеуказанный процесс порождения более не ведёт к какой-то целостности всех ординалов, поскольку, если мы возьмём все ординалы какого-то заданного типа, всегда существуют более высокие ординалы в более высоких типах; и мы не можем объединить множество ординалов, тип которого превышает любую конечную границу. Таким образом, ординалы в каком-то типе могут быть упорядочены в порядке величины во вполне упорядоченный ряд, который имеет ординальное число более высокого типа, чем тип ординалов, составляющих ряд. В новом типе этот новый ординал не является наибольшим. Фактически, не существует наибольшего ординала в каком-то типе, но в каждом типе все ординалы меньше, чем некоторый ординал более высокого типа. Невозможно завершить ряд ординалов, поскольку это приводило бы к типам, превышающим каждую приписываемую конечную границу; таким образом, хотя каждый сегмент ряда ординалов вполне упорядочен, мы не можем сказать, что вполне упорядочен весь ряд, поскольку ‘весь ряд’ является фикцией. Следовательно, парадокс Бурали-Форти исчезает.

Из двух последних разделов обнаруживается, что если принять, что число индивидов не является конечным, то можно доказать существование всех канторовских кардинальных и ординальных чисел, за исключением א_ и _. (Хотя вполне возможно, чтобы их существование было доказуемым.) Существование всех конечных кардинальных и ординальных чисел можно доказать без предпосылки о существовании чего бы то ни было. Ибо, если кардинальное число членов в каком-то типе есть n, число членов в следующем типе есть 2ⁿ. Таким образом, если бы индивидов не существовало, то был бы один класс (а именно, нуль-класс), два класса классов (а именно, тот, что не содержит классов, и тот, что содержит нуль-класс), четыре класса классов классов, и в общем 2^n–1 классов n-го порядка. Но мы не можем объединить члены различных типов и, поэтому, не можем этим способом доказать существование какого-то бесконечного класса.

Теперь мы можем подвести итог всему рассмотрению. После установления некоторых парадоксов логики, мы нашли, что все они вырастают из того факта, что выражение, указывающее на всё из некоторой совокупности, по-видимому, обозначает само себя как одно из этой совокупности; как, например, ‘все пропозиции являются либо истинными, либо ложными’ само, по видимости, является пропозицией. Мы решили, что там, где это, судя по всему, встречается, мы имеем дело с ложной целостностью, и что, фактически, ничего вообще нельзя значимо сказать обо всём из предполагаемой совокупности. Чтобы дать ход этому решению, мы объяснили доктрину типов переменных, придерживающуюся принципа, что любое выражение, которое указывает на всё из некоторого типа, должно, если оно что-либо обозначает, обозначать нечто более высокого типа, чем всё то, на что оно указывает. Там, где указывается на всё из некоторого типа, есть мнимая переменная, принадлежащая этому типу. Таким образом, любое выражение, содержащее мнимую переменную, относится к более высокому типу, чем эта переменная. Это – фундаментальный принцип доктрины типов. Изменение в способе, которым конструируются типы, (это следует доказать с необходимостью) оставило бы решение противоречий незатронутым до тех пор, пока соблюдается этот фундаментальный принцип. Метод конструирования типов, объяснённый выше, продемонстрировал нам, как возможно установить все фундаментальные определения математики и в то же время избежать всех известных противоречий. И оказалось, что на практике доктрина типов уместна лишь там, где затрагиваются теоремы о существовании, или там, где необходимо перейти к некоторому частному случаю.

Теория типов ставит ряд трудных философских вопросов, касающихся её интерпретации. Однако эти вопросы в сущности отделимы от математического развития этой теории и, подобно всем философским вопросам, вводят элемент неопределённости, который не относятся к самой теории. Следовательно, по-видимому, лучше формулировать эту теорию без ссылки на философские вопросы, оставляя их для независимого исследования.