Войти в систему

Home
    - Создать дневник
    - Написать в дневник
       - Подробный режим

LJ.Rossia.org
    - Новости сайта
    - Общие настройки
    - Sitemap
    - Оплата
    - ljr-fif

Редактировать...
    - Настройки
    - Список друзей
    - Дневник
    - Картинки
    - Пароль
    - Вид дневника

Сообщества

Настроить S2

Помощь
    - Забыли пароль?
    - FAQ
    - Тех. поддержка



Пишет kouzdra ([info]kouzdra)
@ 2010-04-04 18:08:00


Previous Entry  Add to memories!  Tell a Friend!  Next Entry
Про аксиому фундирования
В одном треде возник вопрос о мотивированности аксиомы фундирования AKA регулярности (которая запрещает в числе прочего и множества, содержащие себя в качестве элемета - вроде x = {x}). Это довольно поздняя аксиома - в канон ZF она, ЕМНИМП, попала в 1925 году стараниями фон Неймана. Традиционный аргумент в ее пользу - что это объекты настолько странные, что "и ну их нафиг".

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

Это преамбула. А амбула в том, что самоприменимые функции - вролне бытовая реальность кучи языков программирования - вот простейший пример из Haskell:

dup f = λx → f (f x)


Сысл понят:ен: она берет одноместную функцию и возвращает ее в удвоенном виде:

dup sin 1.0 ≡ sin (sin 1.0)

Вполне понятно, что dup dup f x ≡ dup (dup f) x ≡ f (f (f (f x)))

Что несложно проверить опытным путем:

main = print ((dup dup) (+1) 0)

выводит, как и следовало ожидать, чисто 4

Это, разумеется, не единственный пример самоприменимых функций, но imho достаточно показательный.


(Читать комментарии) - (Добавить комментарий)


[info]kouzdra
2010-04-05 21:03 (ссылка)
Аксиоматизация исторически была связана как раз с рефлексивными парадоксами (самый известный - Рассела) - к которым несчетность никаким боком.

какая-то "самоприменимость" в уголке околосчётных фитюлек формализуется.

Да она и в уголке несчетных формализуется - вообще говоря, нигде не сказано, что множество констант в &lambda-исчислении c константами должно быть счетным. В том и дело - что формализуется, но через известное место: одна из причин, почему в этой науке так любят теорию категорий: на нее это просто 1 в 1 ложится: например - типизированная лямбда в точности соответствует классу декартово замкнутых категорий.

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]ppkk
2010-04-05 21:40 (ссылка)
к которым несчетность никаким боком
Для решения проблем типа парадокса Рассела ограничили возможность задавать множества заданием подмножеств уже "имеющихся" множеств. Сама по себе регулярность не разрешает парадокса Рассела: .

Аксиома же регулярности понадобилась для удобной борьбы со всякими монстрами. См., например, что Коэн о ней писал в своей книге: "… упрощает наше определение порядкового числа…"— и т.п. Про фундированные множества тоже…

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]kouzdra
2010-04-05 22:14 (ссылка)
Аксиома фундирования вообще разрешает ровно одну проблему: доказательства того, что универсум фон Неймана является единственной содержательной моделью для ZF за пределами V жизни нет. Ценность этого результата imho крайне сомнительна - и примеры содержательных автореферентных конструкций сомнения усугубляют.

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]ppkk
2010-04-05 23:05 (ссылка)
Если уж такими словами разговор идёт, тоже грубо повторю: в те времена любили надрачивать на всякие ординалы-кардиналы, хотелось ответить на старые вопросы и т.п., так что отказываться от них не хотелось, вот и ввели аксиомку. Но это предположение. Во всяком случае не из-за парадокса Рассела эту аксиому, как я уже написал, вводили, похоже, с этим Вы согласны.

(Ответить) (Уровень выше)


(Читать комментарии) -