что следует из теоремы Геделя

[Alexey Romanov]

epros в сообщении #202770 писал(а):

Вы про иерархию типов что-нибудь слышали?

Да, разумеется. Если Вы думаете, что все объекты в теории должны быть на одном уровне иерархии -- Вы глубоко заблуждаетесь.

[epros]

Alexey Romanov писал(а):

epros в сообщении #202770 писал(а):

Вы про иерархию типов что-нибудь слышали?

Да, разумеется. Если Вы думаете, что все объекты в теории должны быть на одном уровне иерархии -- Вы глубоко заблуждаетесь.

Я так не думаю. Но $\mathbb{N}$ в конструктивной теории не может быть на одном уровне иерархии с натуральным числом.

[Alexey Romanov]

epros в сообщении #202777 писал(а):

Но $\mathbb{N}$ в конструктивной теории не может быть на одном уровне иерархии с натуральным числом.

С этим я не спорю. Вы утверждали, напомню:

Цитата:

А в конструктивном смысле типы объектов сами по себе объектами не являются. Хотя все объекты конечного типа можно собрать в совокупность, которую допустимо рассматривать как объект.

Я утверждаю, что $\mathbb{N}$ вполне можно рассматривать как объект, находящийся, естественно, на другом уровне иерархии. Более того, его подтипы -- тоже объекты, независимо от того, конечны ли они.

Они не являются объектами арифметики Гейтинга -- ровно так же, как $\mathbb{N}$ и его подмножества не являются объектами арифметики Пеано.

Они являются объектами теории типов, которую можно использовать как метатеорию для арифметики -- ровно так же, как $\mathbb{N}$ и его подмножества являются объектами теории множеств $ZFC$, которую можно использовать как метатеорию для арифметики.

[Pi]

epros в сообщении #202725 писал(а):

Pi писал(а):
до Лабочевского "пятый постулат" являлся однозначной теоремой который никто не мог доказать

Ну и ну Exclamation
А я-то полагал, что "теоремой" по определению называется то, что доказуемо в теории.

Нет, теоремой называется то что считается можно доказать, пример, великая теорема Ферма. Столетиями ее не могли доказать, но при этом никто не отказывал ей в звании теоремы.

А вообще весь этот раговор об абстракции бесконечности бессмысленный. В математике можно утверждать тот факт что бесконечность есть. Формулирование что такое бесконечность и какие виды ее бывают это уже является сущностью отдельных теорий.

[epros]

Alexey Romanov писал(а):

epros в сообщении #202777 писал(а):

Но $\mathbb{N}$ в конструктивной теории не может быть на одном уровне иерархии с натуральным числом.

С этим я не спорю. Вы утверждали, напомню:

Цитата:

А в конструктивном смысле типы объектов сами по себе объектами не являются. Хотя все объекты конечного типа можно собрать в совокупность, которую допустимо рассматривать как объект.

Я утверждаю, что $\mathbb{N}$ вполне можно рассматривать как объект, находящийся, естественно, на другом уровне иерархии.

Видите ли в чём дело: Речь была об актуальной бесконечности, причём я утверждал, что бесконечные типы определимы, но их "существование" нельзя конструктивно утверждать в том же смысле, в котором утверждается существование объектов соответствующего типа. Так что Ваше возражение формально верно, но не совсем по существу. $\mathbb{N}$, конечно же, "можно рассматривать как объект", но совсем не в том смысле, в котором рассматриваются натуральные числа.

Натуральное число - это строка вертикальных чёрточек (такое определение использует Марков). Таким образом, $\mathbb{N}$ - это совокупность всех строк вертикальных чёрточек. Ну нет такой теории, в которой бы "существовал" такой объект именно в таком буквальном смысле. Но тем не менее $\mathbb{N}$ может рассматриваться как объект некой теории, ибо в конструктивном понимании свойство "быть натуральным числом" - это ни что иное, как алгоритм, проверяющий предъявленную в качестве аргумента строку на предмет того, что она является строкой вертикальных чёрточек. Код этого алгоритма - это конечная строка, которая, конечно же, "существует" как объект соответствующей теории.

Но одно дело - объект "код алгоритма, проверяющий строку", а другое дело - тип "натуральное число", который бесконечен. Это совсем разные логические уровни рассмотрения понятия: первый рассматривает буковки, из которых состоит код, а второй - результат его выполнения. Нельзя их смешивать, говоря: "Вот Вам объект $\mathbb{N}$, который бесконечен". Даже если Вы рассматриваете и строки из вертикальных чёрточек, и строки, определяющие коды алгоритмов, в рамках одной теории!

Поэтому я и говорю: неправильно говорить о существовании типа в том же смысле, в котором говорится о существовании объектов данного типа. Даже если теория рассматривает несколько уровней иерархии типов (а это возможно - например, метатеория, определяющая язык и синтаксис арифметики Пеано, может сама использовать натуральные числа как собственные объекты), она всё равно не должна забывать, что это объекты "разного уровня".

Alexey Romanov писал(а):

Они являются объектами теории типов, которую можно использовать как метатеорию для арифметики -- ровно так же, как $\mathbb{N}$ и его подмножества являются объектами теории множеств $ZFC$, которую можно использовать как метатеорию для арифметики

Только в ZFC нет никакой "иерархии множеств" - все они равноправны. Именно это позволяет одновременно утверждать две вещи: 1) бесконечность количества объектов, обладающих неким свойством, и 2) существование в том же мире объекта, "составленного" из всех этих объектов. Конструктивно объединить эти два утверждения никак не получится.

Добавлено спустя 17 минут 41 секунду:

Pi писал(а):

Нет, теоремой называется то что считается можно доказать, пример, великая теорема Ферма. Столетиями ее не могли доказать, но при этом никто не отказывал ей в звании теоремы.

Ну, мало ли что как называли в околоматематической беллетристике. Если так рассуждать, то пятый постулат Евклида - это именно "постулат", а никакая не теорема, ибо именно так его "называли". Да и теорему Ферма, может быть, называли теоремой именно потому, что полагали, что Ферма её доказал, только изложить доказательство для публики не успел. По крайней мере, вначале так и думали, ну а потом как-то и привыкли уже теоремой называть.

Но вообще-то при рассмотрении формальных теорий "теоремой" называется именно результат формального вывода.

Pi писал(а):

В математике можно утверждать тот факт что бесконечность есть. Формулирование что такое бесконечность и какие виды ее бывают это уже является сущностью отдельных теорий.

С обоими утверждениями я не согласен. Конструктивно утверждать, что "бесконечность есть", нет никаких оснований. А вот формулирование того, что такое бесконечность (независимо от её типа), как раз возможно и даже вполне тривиально: это отсутствие конца (доказуемое) в соответствующих построениях.

[Someone]

epros в сообщении #202725 писал(а):

Э-эээ... Я в недоумении, ибо таких философских вопросов не понимаю.

Это не философский вопрос. Вы утверждаете, что вопрос об актуальной бесконечности имеет конкретное математическое значение. Вот и сформулируйте это в конкретных математических терминах применительно к теории множеств. Пока Вы усиленно увиливаете. Сначала Вы утверждали, что бесконечность в теории множеств - это актуальная бесконечность в отличие от бесконечности в конструктивной теории. На просьбу дать математическое определение актуальной бесконечности я пока ничего внятного не услышал. Вы просто назвали бесконечное (в смысле Дедекинда) множество актуально бесконечным, никак это не мотивируя. Потом Вы заявили, что не хотели давать определения, а просто указали, чтó Вы хотите называть актуально бесконечным. Теперь заявляете, что вопрос вообще к математике отношения не имеет.

Вывод (который мне был ясен с самого начала): Вы вообще не понимаете, о чём говорите. В математике нет понятий актуальной и потенциальной бесконечности, эти понятия носят псевдофилософский характер и связаны со способом интерпретации множеств, не более того. Возможна любая интерпретация множеств, хоть "актуальная", хоть "потенциальная". Говорить, что "классическая математика плохая, потому что использует абстракцию актуальной бесконечности", а "конструктивная математика хорошая, потому что использует абстракцию потенциальной осуществимости", математически бессмысленно. Реальные различия классической и конструктивной математики находятся совсем в другом месте.

epros в сообщении #202725 писал(а):

А теперь подумайте, можно ли в теории, формализованной в логике первого порядка, приписать какие либо характеристики свойству? Например, вот Вам свойство:
$isPrime(x)$ - "число $x$ является простым".
Как бы Вы записали утверждение о бесконечности типа простых чисел, не прибегая к аксиоматике теории множеств? Может быть как-то так:
$isInfinite(isPrime)$?
Увы, логика первого порядка не позволяет подставлять предикатные символы вместо переменных в другие предикаты.

Если оставаться в рамках языка арифметики, я бы рассматривал $isInfinite(isPrime)$ как сокращение формулы $isPrime(2)\&\forall x(isPrime(x)\Rightarrow\exists y(y>x\& isPrime(y)))$. Эта формула в арифметике доказуема и подозрительно похожа на формулу, выражающую аксиому бесконечности.

Так Вы мне не ответили: язык теории множеств отнóсится к логике первого порядка или нет?

epros в сообщении #202725 писал(а):

Я хочу сказать, что в ZFC множества рассматриваются не только как свойства, но и как объекты. А в конструктивном смысле типы объектов сами по себе объектами не являются. Хотя все объекты конечного типа можно собрать в совокупность, которую допустимо рассматривать как объект.

Мне это надоело. В книге Кушнера, на которую я не раз ссылался, и который является конструктивистом, множества рассматриваются как конструктивные объекты - независимо от того, называть ли их множествами, свойствами или типами, и независимо от того, конечны они или нет. Он обращается с ними, как с объектами. В одной и той же теории. Совершенно предметной. Ему я верю, а Вашим увёрткам - нет.

epros в сообщении #202725 писал(а):

Это Вы сейчас апеллируете не к тому. Из философских рассуждений вокруг актуальной бесконечности действительно мало что можно почерпнуть. Как я понимаю, в этом и состояла Ваша претензия к этому понятию: что оно "не математическое". А я Вам говорю, что оно математически определимо.

И где определение? Только не повторяйте своё "определение". Вы уже сами признали, что оно ничего не определяет, а только "указывает, что Вы хотите этим словом называть".

epros в сообщении #202725 писал(а):

утверждение об актуальном (т.е. в предметной теории) существовании бесконечности (т.е. объекта, содержащего все объекты бесконечного типа) является нетривиальной особенностью теории

совершенно одинаково справедливой как для классической теории множеств, так и для конструктивного рекурсивного анализа. Читайте Кушнера.

epros в сообщении #202732 писал(а):

В предметной теории (например, в арифметике) тип предметных объектов (например, $\mathbb{N}$) не получится определить как конструктивный объект. Но, естественно, тип предметных объектов является объектом метатеории.

Господи, далась Вам эта метатеория, что Вы её везде видите и везде втыкаете, бóльшей частью совершенно не к месту.

Арифметика - очень сильная теория. Я в одной из тем показывал, что она эквивалентна теории наследственно конечных множеств (в том смысле, что в арифметике можно интерпретировать теорию множеств так, что все аксиомы теории множеств, кроме аксиомы бесконечности, будут теоремами арифметики (все множества в этой интерпретации равномощны натуральным числам), а арифметику, в свою очередь, можно интерпретировать в теории наследственно конечных множеств (с аксиомами индукции вместо аксиомы бесконечности) так, что все аксиомы арифметики будут теоремами теории множеств).
Но этого мало. В арифметике можно интерпретировать гораздо бóльшие фрагменты теории множеств, включающие много бесконечных множеств, в том числе, и $\mathbb{N}$. Известно, например, что можно определить все ординалы, меньшие первого так называемого эпсилонового ординала (так называются ординалы, удовлетворяющие уравнению $\omega^{\varepsilon}=\varepsilon$). И можно использовать трансфинитную индукцию до любого ординала, меньшего этого самого $\varepsilon$.

epros в сообщении #202897 писал(а):

Видите ли в чём дело: Речь была об актуальной бесконечности, причём я утверждал, что бесконечные типы определимы, но их "существование" нельзя конструктивно утверждать в том же смысле, в котором утверждается существование объектов соответствующего типа. Так что Ваше возражение формально верно, но не совсем по существу. $\mathbb{N}$, конечно же, "можно рассматривать как объект", но совсем не в том смысле, в котором рассматриваются натуральные числа.

Читайте Кушнера. И натуральные числа, и натуральный ряд рассматриваются совершенно равноправно и являются конструктивными объектами в одинаковом смысле. И то, и другое - слова в заданном алфавите, которые совершенно одинаково могут быть входными данными и результатом работы алгоритмов.

epros в сообщении #202897 писал(а):

Натуральное число - это строка вертикальных чёрточек (такое определение использует Марков). Таким образом, $\mathbb{N}$ - это совокупность всех строк вертикальных чёрточек. Ну нет такой теории, в которой бы "существовал" такой объект именно в таком буквальном смысле.

В таком "буквальном" смысле его нет и в ZFC.

epros в сообщении #202897 писал(а):

Только в ZFC нет никакой "иерархии множеств" - все они равноправны.

Да есть там иерархия. Существование этой иерархии в ряде случаев сильно облегчает жизнь, хотя слишком уж большой роли она и не играет. Поэтому Вы о ней и не знаете (или умышленно забыли, поскольку в теме, посвящённой актуальной бесконечности, о ней речь заходила). Можно рассматривать теории множеств, в которых полной (охватывающей все множества) иерархии нет. Но частичную иерархию обычно можно построить, если теория не слишком уж ограниченная.

epros в сообщении #202897 писал(а):

Именно это позволяет одновременно утверждать две вещи: 1) бесконечность количества объектов, обладающих неким свойством, и 2) существование в том же мире объекта, "составленного" из всех этих объектов. Конструктивно объединить эти два утверждения никак не получится.

У других конструктивистов получается, только у Вас почему-то не получается.

P.S. Просто поразительно. Стоит в какой-нибудь теме появиться Nxx или eprosу, в ней сразу начинается обсуждение актуальной бесконечности и "преимуществ" конструктивной математики. Посмотрите на название этой темы. Много ли сообщений в ней посвящено именно теореме Гёделя?

[Alexey Romanov]

epros в сообщении #202897 писал(а):

бесконечные типы определимы, но их "существование" нельзя конструктивно утверждать в том же смысле, в котором утверждается существование объектов соответствующего типа.

В том же самом смысле -- $\mathbb{N}$ вполне нормальный объект типа $\mathrm{Type}_0$, так же как $3$ -- это объект типа $\mathbb{N}$. Оба они задаются конкретными конечными строчками символов.

epros в сообщении #202897 писал(а):

Нельзя их смешивать, говоря: "Вот Вам объект $\mathbb{N}$, который бесконечен"

Разумеется, $\mathbb{N}$ -- конечный объект в том смысле, что у него есть конечное описание. И нельзя утверждать, что $\mathbb{N}$ "состоит из" своих объектов. Но в этом тип $\mathbb{N}$ ничем не отличается от конечных типов.

Добавлено спустя 6 минут 51 секунду:

Советую также почитать Set Theory: Constructive and Intuitionistic ZF. Обратите внимание на наличие в обеих теориях вполне обычной аксиомы бесконечности.

[epros]

Alexey Romanov писал(а):

В том же самом смысле -- $\mathbb{N}$ вполне нормальный объект типа $\mathrm{Type}_0$, так же как $3$ -- это объект типа $\mathbb{N}$. Оба они задаются конкретными конечными строчками символов.

Ну так разных же уровней иерархии объекты. Понятное дело, что код алгоритма, перечисляющего строки вертикальных чёрточек, это тоже конечная строка. Но этот объект (строка кода) никак не связан с совокупностью объектов, которые перечисляет алгоритм. Поэтому утверждение о существовании этой строки кода не имеет никакого отношения к утверждению о существовании совокупности всех строк чёрточек.

Вот я и говорю: "разные логические уровни". Одно дело - сказать, что процедура перечисления натуральных чисел существует, но не имеет конца (это "потенциальная бесконечность" и с моей точки зрения конструктивно), а другое дело - сказать, что существует совокупность всех натуральных чисел (это "актуальная бесконечность" и ничего конструктивного я в этом не вижу).

Alexey Romanov писал(а):

Разумеется, $\mathbb{N}$ -- конечный объект в том смысле, что у него есть конечное описание. И нельзя утверждать, что $\mathbb{N}$ "состоит из" своих объектов. Но в этом тип $\mathbb{N}$ ничем не отличается от конечных типов.

Ну так и в чём тогда проблема?

Alexey Romanov писал(а):

Советую также почитать Set Theory: Constructive and Intuitionistic ZF. Обратите внимание на наличие в обеих теориях вполне обычной аксиомы бесконечности.

Спасибо за ссылку. Пока не успел внимательно вчитаться, но у меня такое чувство, что здесь предпринята попытка просто наложить аксиоматику ZF (с некоторыми ограничениями) на интуиционистскую логику и провозгласить, что это "конструктивно". Я пока не могу этого принять. С моей точки зрения всякое утверждение о существовании должно быть подкреплено процедурой построения конкретного экземпляра (иное "неконструктивно"). Поэтому я не вижу возможности принять аксиому бесконечности как конструктивную, ибо не вижу процедуры построения конкретного объекта, существование которого она утверждает (индуктивного множества).

Добавлено спустя 2 часа 3 минуты 13 секунд:

Someone писал(а):

Вы утверждаете, что вопрос об актуальной бесконечности имеет конкретное математическое значение. Вот и сформулируйте это в конкретных математических терминах применительно к теории множеств.

Что Вы имеете в виду под "значением", которое "применительно к теории множеств"?

Someone писал(а):

Вы просто назвали бесконечное (в смысле Дедекинда) множество актуально бесконечным, никак это не мотивируя.

А как я должен "мотивировать" определение?

Someone писал(а):

Потом Вы заявили, что не хотели давать определения, а просто указали, чтó Вы хотите называть актуально бесконечным.

Нет, я не заявлял, что "не хотел давать определения". Я заявлял, что указание способа проверки того, подходит ли термин к объекту, - это и есть "определение" понятия.

Someone писал(а):

Теперь заявляете, что вопрос вообще к математике отношения не имеет.

Какой вопрос? Вопрос актуальности бесконечности - имеет. А рассуждения про "завершённость" множества - вряд ли.

Someone писал(а):

Реальные различия классической и конструктивной математики находятся совсем в другом месте.

Совершенно верно. Реальные различия лежат в трактовке понятия "существования". А вопрос об актуальной бесконечности - это частный случай, ибо соответствующая аксиома тоже является утверждением о существовании.

Someone писал(а):

Если оставаться в рамках языка арифметики, я бы рассматривал $isInfinite(isPrime)$ как сокращение формулы $isPrime(2)\&\forall x(isPrime(x)\Rightarrow\exists y(y>x\& isPrime(y)))$. Эта формула в арифметике доказуема и подозрительно похожа на формулу, выражающую аксиому бесконечности.

Нет, ну Вы интересную интерпретацию дали, конечно. Я не стану спорить с тем, что Ваша формула имеет отношение к бесконечности простых чисел. Но я-то Вас спросил о записи предиката бесконечности применительно свойству "простоты" числа (что явно видно из формы записи, хотя она и недопустима в логике первого порядка). Это значит, что свойство "простоты" стоит в позиции аргумента предиката бесконечности и может быть заменено каким-нибудь другим свойством объектов предметной теории. Можете Вы в Вашей записи заменить свойство "является простым числом", например, на свойство "является положительным рациональным числом меньше единицы"? Или, по-просту говоря, где общая форма записи предиката бесконечности, в которой при необходимости достаточно заменить лишь аргумент?

Someone писал(а):

Так Вы мне не ответили: язык теории множеств отнóсится к логике первого порядка или нет?

Разумеется. Обычно теория множеств формализуется именно в этом языке. Разве я где-то намекал на противоположное?

Someone писал(а):

Читайте Кушнера. И натуральные числа, и натуральный ряд рассматриваются совершенно равноправно и являются конструктивными объектами в одинаковом смысле. И то, и другое - слова в заданном алфавите, которые совершенно одинаково могут быть входными данными и результатом работы алгоритмов.

"Натуральный ряд" - это не "слово в алфавите". На самом деле это бесконечная строка:
"1, 2, 3, ..."
Конечным словом в алфавите является код алгоритма, который генерирует натуральные числа. Но называть этот код "натуральным рядом" просто некорректно. Не знаю, где Вы у Кушнера вычитали иное.

Someone писал(а):

epros в сообщении #202897 писал(а):

Натуральное число - это строка вертикальных чёрточек (такое определение использует Марков). Таким образом, $\mathbb{N}$ - это совокупность всех строк вертикальных чёрточек. Ну нет такой теории, в которой бы "существовал" такой объект именно в таком буквальном смысле.

В таком "буквальном" смысле его нет и в ZFC.

А в каком же смысле он есть в ZFC? В том смысле, что мы можем придумать для него специальный значок $\omega_0$ и договориться о том, как его "правильно" интерпретировать, когда он встречается в соответствующих формулах? Причем остаётся масса случаев, когда неизвестно как его нужно интерпретировать.

Someone писал(а):

epros в сообщении #202897 писал(а):

Только в ZFC нет никакой "иерархии множеств" - все они равноправны.

Да есть там иерархия. Существование этой иерархии в ряде случаев сильно облегчает жизнь, хотя слишком уж большой роли она и не играет. Поэтому Вы о ней и не знаете (или умышленно забыли, поскольку в теме, посвящённой актуальной бесконечности, о ней речь заходила).

Это совсем не та иерархия. В иерархическом отношении $\{\} \in \{\{\}\}$ нет особого смысла, ибо и $\{\}$, и $\{\{\}\}$ записываются строками символов, которые сопоставимы с помощью строковых операций. Но $\{\}$ и $\omega_0$ невозможно сопоставить с помощью строковых операций - для этого придётся привлекать невесть откуда взятую аксиоматику.

Someone писал(а):

P.S. Просто поразительно. Стоит в какой-нибудь теме появиться Nxx или eprosу, в ней сразу начинается обсуждение актуальной бесконечности и "преимуществ" конструктивной математики. Посмотрите на название этой темы. Много ли сообщений в ней посвящено именно теореме Гёделя?

Между прочим, в этой теме об этом Вы заговорили первый, я лишь Вам отвечал.

[Pi]

epros в сообщении #202897 писал(а):

Конструктивно утверждать, что "бесконечность есть", нет никаких оснований. А вот формулирование того, что такое бесконечность (независимо от её типа), как раз возможно и даже вполне тривиально: это отсутствие конца (доказуемое) в соответствующих построениях.

Ваша точка зрения уникальна. И противоречит всей матиматике.
Аксиомы математики.
Аксиома 1. Бесконечности существуют.
Аксиома 2. Вид Бесконечности определяется теорией.
Пример, в p-адических числах она записывается как ...(9)9.
\infty в проективной геометрии это особая точка.
И тд.

Ваше определение бесконечности это одно из многих определений, и то что вы лично запрещаете давать другие определения это просто не правильно или хуже того .....
Никто с вами никогда не согласится, потому-что всем очевидна ошибочность и бесперспективность этого подхода...

[epros]

Pi писал(а):

Аксиомы математики.
Аксиома 1. Бесконечности существуют.
Аксиома 2. Вид Бесконечности определяется теорией.

Не выдумывайте. "Аксиомы математики" - это вообще слишком сильно сказано. Есть некоторые аксиомы в некоторых конкретных теориях, которые что-то утверждают о том, что называется "бесконечностью".

Pi писал(а):

Ваше определение бесконечности это одно из многих определений, и то что вы лично запрещаете давать другие определения это просто не правильно или хуже того .....

Во-первых, я ничего никому не запрещаю.
Во-вторых, в последнее время на этом форуме я давал определение только термину "актуальная бесконечность", причём исключительно в контексте теории множеств (в её терминологии). Так что трактовать это как "моё определение бесконечности" (без добавки "актуальная") - это не вполне корректно. К тому же с моей точки зрения конструктивного в этом определении ничего нет, а поэтому я могу его "сформулировать", но не могу "принять".
В третьих, я считаю конструктивным (и могу принять) потенциальную бесконечность, а именно, понятие бесконечного типа. Но я вроде бы его пока не определял (хотя это несложно). Но тут как раз возникает вопрос о том, в каком смысле "существуют" типы, из которого и вырастают различия между "актуальной" и "потенциальной" бесконечностью.

[Pi]

epros в сообщении #203102 писал(а):

различия между "актуальной" и "потенциальной" бесконечностью

Скорее это вопрос филосовский, чем математический. Математике наплевать каким образом мы вводим или определяем бесконечности. Она с ними работает через теории. А как их интерпретировать, это уже философия.
Я не думаю что хоть чтото можно извлечь из этой разници математически полезное, без филосовствований.

[epros]

Pi писал(а):

Математике наплевать каким образом мы вводим или определяем бесконечности.

Различия, о которых идёт речь, касаются не того, "каким образом мы определяем бесконечности", а того, каким образом мы вводим утверждение об их существовании. Когда Вы проводите карандашом на бумаге прямую, то считаете, что она состоит из "точек" (нанесённых грифелем), которые Вы можете продолжить "сколь угодно далеко". Последнее - это есть утверждение о "потенциальном" существовании бесконечности. А вот если Вы скажете, что "существует бесконечная точка" (как в проективной геометрии) - это уже будет утверждение об "актуальном" существовании бесконечности.

Это на уровне философии. А математически: Есть иерархия типов. Тип всегда является объектом более высокого уровня иерархии, чем те объекты, для которых он является типом. Утверждение о потенциальном существовании бесконечности состоит в том, что "существует бесконечный тип". Утверждение об актуальном существовании бесконечности состоит в том, что "среди объектов данного уровня иерархии есть объект, содержащий все объекты бесконечного типа объектов данного уровня иерархии".

Так что "актуально" (существует) означает "как объект того же предметного мира (уровня иерархии типов), к которому относятся объекты, о бесконечном количестве которых идёт речь".

Pi писал(а):

Я не думаю что хоть чтото можно извлечь из этой разници математически полезное, без филосовствований.

Но если эту разницу игнорировать, то из этого можно извлечь массу бесполезного. Это уж точно.

[Pi]

epros в сообщении #203121 писал(а):

Различия, о которых идёт речь, касаются не того, "каким образом мы определяем бесконечности", а того, каким образом мы вводим утверждение об их существовании. Когда Вы проводите карандашом на бумаге прямую, то считаете, что она состоит из "точек" (нанесённых грифелем), которые Вы можете продолжить "сколь угодно далеко". Последнее - это есть утверждение о "потенциальном" существовании бесконечности. А вот если Вы скажете, что "существует бесконечная точка" (как в проективной геометрии) - это уже будет утверждение об "актуальном" существовании бесконечности.

Без разницы. Мы имеем право и так и так вводить бесконечность.

epros в сообщении #203121 писал(а):

Есть иерархия типов. Тип всегда является объектом более высокого уровня иерархии, чем те объекты, для которых он является типом. Утверждение о потенциальном существовании бесконечности состоит в том, что "существует бесконечный тип". Утверждение об актуальном существовании бесконечности состоит в том, что "среди объектов данного уровня иерархии есть объект, содержащий все объекты бесконечного типа объектов данного уровня иерархии".

В теории типов объект данного типа не может содержать в себе никакой другой объект данного типа. Там строгая иерархия. Иначе ваше утверждение эквивалентно "множеству всех множеств".
Поэтому ваш текст логически противоричив и не понятен.

[epros]

Pi писал(а):

Без разницы. Мы имеем право и так и так вводить бесконечность.

Разница есть (в частности, проективная геометрия отличается от аффинной). И дело не в "праве": никто не отнимает у Вас право пользоваться неконструктивными теориями.

Pi писал(а):

epros в сообщении #203121 писал(а):

Есть иерархия типов. Тип всегда является объектом более высокого уровня иерархии, чем те объекты, для которых он является типом. Утверждение о потенциальном существовании бесконечности состоит в том, что "существует бесконечный тип". Утверждение об актуальном существовании бесконечности состоит в том, что "среди объектов данного уровня иерархии есть объект, содержащий все объекты бесконечного типа объектов данного уровня иерархии".

В теории типов объект данного типа не может содержать в себе никакой другой объект данного типа. Там строгая иерархия. Иначе ваше утверждение эквивалентно "множеству всех множеств".
Поэтому ваш текст логически противоричив и не понятен.

Если слово "содержать" характеризует именно принадлежность к типу. Но, по-моему, это слово для этого случая плохо подходит. Вот Вам такой пример:
Есть бесконечный тип "натуральное число". К нему относятся такие объекты (строки): "1", "2", "3" и т.п. Есть другой тип (конечный): "натуральное число не больше трёх". К нему относятся только три указанных объекта (без "и т.п."). А есть такой объект того же уровня иерархии - "список натуральных чисел не более трёх": строка "1,2,3". Последний объект "содержит" все объекты последнего типа в том смысле, что они извлекаются из списка соответствующим алгоритмом. Как видите, здесь слово "содержит" не подразумевает принадлежность объекта к типу (объекту следующего уровня иерархии).

[Alexey Romanov]

Pi в сообщении #203122 писал(а):

В теории типов объект данного типа не может содержать в себе никакой другой объект данного типа. Там строгая иерархия.

Неверно. Во многих вариантах теории типов 1-тип "тип всех 0-типов" является подтипом 2-типа "тип всех 1-типов", то есть любой 0-тип является и 1-типом (и 2-типом, и т.д.) Таким образом, все объекты 1-типа "тип всех 0-типов" сами -- 1-типы.

Pi в сообщении #203122 писал(а):

Иначе ваше утверждение эквивалентно "множеству всех множеств".

Разумеется, тип всех 1-типов -- не 1-тип.