Большое количество числа сада

Большое количество числа сада (англ. Large Number Garden Number, яп. 巨大数庭園数, также сокращённо "БКЧС" (англ. "LNGN")) — сокращённое название большого числа, равного $f^{10}(10 \uparrow^{10} 10)$, где $f$ — значение функции, определённой в теории первого порядка за пределами теории множеств более высокого порядка. Термин был введён пользователем англоязычной гугология вики P進大好きbot. Оригинальное название БКЧС на японском языке переводится на английский как

"Давайте, друзья, сад больших чисел наконец-то завершён! Позвольте мне объяснить назначение этого сада. Первое — функция определения адреса и поэтажного плана. Когда строка символов считывается, она автоматически определяет, какой адрес миниатюрного сада она представляет и в каком миниатюрном саду может быть воспроизведён поэтажный план сада с большим количеством числа. Второе — функция анализа поэтажного плана. Если вы укажете адрес миниатюрного сада и прочтёте там поэтажный план воспроизводимого сада с большим количеством растений, он подскажет вам, какое большое количество растений может производить сад. Третья важная функция — способность генерировать большие числа. После ввода натурального числа выполняется поиск по всем символьным строкам в пределах верхнего предела количества символов, и каждая строка считывается в функцию определения адреса и плана этажа, оставляя только воспроизводимый план этажа для каждого миниатюрного сада. Перечислив их и загрузив в функцию анализа поэтажного плана, вы можете получить большие числа, которые они могут выдать, и, сложив их все вместе, вы можете создать новые большие числа! А? Можете ли вы действительно получить большое количество с помощью этого? Как обычно, мой помощник настроен скептически. Но, эй, вот поэтажный план самого большого сада. Если вы загрузите это в функцию анализа, она сообщит вам, насколько большие числа вы можете сгенерировать. А? Сколько символов содержится в этом поэтажном плане? Какой смысл знать такие вещи?"

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

Определение

Теория

Во-первых, язык L определяется путём добавления символа одномерной функции U к языку теории множеств первого порядка со счётным числом символов переменных членов и символом отношения принадлежности множеству ∈. Определите ZF_L как набор L-формул, принадлежащих аксиомам ТМЦФ. Здесь схема понимания и замены аксиом в ZF_L параметризована всеми L-формулами, т.е. формулами, которые может включать U.

Определите формальный язык L логики первого порядка, добавив счётное количество символов постоянных членов, счётное количество символов функций, счётное количество символов отношений и новый 1-арный функциональный символ Θ (тета) к явной формализации L с использованием явного соответствия Гедёля. Затем мы обозначим через ZFC_L множество L-формул, принадлежащих аксиомам ТМЦФ, здесь схема понимания и замены аксиом в ZFC_L параметризуются всеми L-формулами, т.е. формулами, которые могут включать в себя формализацию U, дополнительные символы постоянных членов, дополнительные символы функций, дополнительные символы отношений и Θ.

Мы явно кодируем ординалы ниже ε₀ и L-формулы в натуральные числа в ТМЦФ и формализуем аксиому Хенкина, гласящую, что "Если существует x, удовлетворяющий P, то Θ(n) удовлетворяет P" для каждого символа члена переменной x, каждой L-формулы P с кодом n, формализованной в ZFC_L путём повторения последующих операций.

Обозначим через ZFCH_L теорию ZFC_L, дополненную схемой аксиомы Хенкина. Новый функциональный символ Θ играет роль "семейства констант Хенкина". Пожалуйста, не путайте базовую теорию ZF_L и формализованную теорию ZFCH_L.

Обозначим через U1 L-формулу "Для любого ординала α, U(α)⊨ZFCH_L". При ZF_L, дополненном {U1}, U(α) формирует модель ZFC_L и, следовательно, формирует L-структуру для любого ординала α. Мы обозначаем через U^U(α) интерпретацию U в U(α). Обозначим через U2 L-формулу "Для любого ординала α и любого β∈α, U^U(α)(β)=U(β)", а через U3 L-формулу "Для любого ординала α существует ординал β такой, что |U(α)|=V_β и для любого x∈V_β и любого y∈V_β, x∈^U(α)y эквивалентно x∈y", где V_β обозначает иерархию фон Неймана. Определите T как множество ZF_L∪{U1,U2,U3} L-формул.

Встраивание

Присваивая каждой атомной формуле x_i∈x_j в ТМЦФ L-формулу (x_i∈x_j)∧(x_j∈U(0)), теорию T можно рассматривать как расширение ТМЦФ. В частности, множество N, определённое в ТМЦФ, интерпретируется в U(0) как член T, который совпадает с термином N, определённым в ZF_L, поскольку U(0) является переходной моделью ZFC_L. Следовательно, большое число, определяемое в ТМЦФ, также определяется в T и образует член, который является большим числом. Более того, поскольку L допускает счётно бесконечное множество символов постоянных членов, символов функций и символов отношений, даже замкнутая формула в теории, полученная путём добавления счётно большого количества символов постоянных членов, символов функций и символов отношений к ТМЦФ, может быть интерпретирована при U(0) как замкнутая формула формула в T. Далее, путём присвоения каждой атомной формуле x_i∈x_j в несортированной теории множеств MK L-формулы (x_i∈x_j)∧(x_j∈U(0)), теорию T можно рассматривать как расширение теории множеств MK.

Грубо говоря, U(0) формально играет роль универсума теории множеств первого порядка, степенное множество U(0) формально играет роль универсума теории множеств второго порядка и теории классов первого порядка, а его степенное множество формально играет роль универсума из теории множеств третьего порядка. Поскольку все они включены в U(1), U формально играет роль строго возрастающей последовательности универсумов теорий множеств более высокого порядка. Обратите внимание, что существование такой строго возрастающей последовательности может быть построено в ТМЦФ, дополненной универсальной аксиомой Гротендика, которая появляется в обычной математике.

Большое число

Явно определите сюръективное отображение: CNF: N→ε₀; i↦CNF(i), используя нормальную форму Кантора.

Для L-формулы P обозначим через IsDefinition(P) L-формулу "Существует x такой, что P и для любого i, (P) [i/x] подразумевает i =x". Обозначим через Definable(m,i,P) L-формулу "i∈N, P является L-формулой, U(CNF(i))⊨IsDefinition(P), а U(CNF(i))⊨(P)[m/x]", где m в (P)[m/x] рассматривается как параметр явным образом.

Для n∈N определите f(n) как сумму m∈N, удовлетворяющую i∈n, P∈n и определяемую (m,i,P), таким образом, в конечном итоге существует невычислимая большая функция f: N→N; n↦f(n). Отсюда большое число — это $f^{10}(10 \uparrow^{10} 10)$.

Внешние ссылки

• koteitan, pdf-перевод из первоисточника, Dropbox.
• koteitan, 巨大数寄席 Часть 2, ニコニコ動画. (Видеозапись, прочитанная 巨大数庭園数 вслух.)
• 西宮 七南-解説channel, ゆっくりと学ぶ巨大数論～巨大数庭園数～, ютуб. (Видео, знакомящее с 巨大数庭園数.)