А если мы конечные наты определим в теории типов при

Question

А если мы конечные наты определим в теории типов при

помощи рекурсии-индукции или рекурсии-рекурсии или типа того? Примерно так:
1. 0 — натуральное число
2. suc n — натуральное число, если n — натуральное число, которое мы уже определили

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

0

03.01.2024

16 ответов

47 просмотров

Alexander Chichigin Автор вопроса

Nikita Repeev
Просто есть дополнительное требование которое мы х...

Стикер

0

10 месяцев назад

Alexander Chichigin Автор вопроса

Nikita Repeev
Просто есть дополнительное требование которое мы х...

Стикер

0

10 месяцев назад

Nikita Repeev

Если "это не проблема" то ты решил её не решать. А мы хотим рассмотреть.

0

10 месяцев назад

Nikita Repeev

Ну примени конечное число раз, потом примени конечное но большее число раз. Потом повтори это бесконечность раз. Уйдёшь в бесконечность.

0

10 месяцев назад

Alexander Chichigin Автор вопроса

Nikita Repeev
Если "это не проблема" то ты решил её не решать. А...

Так вы сперва создаёте себе проблему, а потом пытаетесь её решать. Не добавляйте аксиому бесконечности — у вас вообще не будет возможности что-то применять бесконечное число раз. Нет аксиомы — нет проблем! 😁

0

10 месяцев назад

Nikita Repeev

Alexander Chichigin
Так вы сперва создаёте себе проблему, а потом пыта...

Стикер

0

10 месяцев назад

Alexander Chichigin Автор вопроса

Nikita Repeev
Ну примени конечное число раз, потом примени конеч...

Стикер

0

10 месяцев назад

Nikita Repeev

Alexander Chichigin
Так вы сперва создаёте себе проблему, а потом пыта...

Стикер

0

10 месяцев назад

Alexander Chichigin Автор вопроса

Я не понимаю, чем вас не устраивает решение "не создавать проблему". Т.е. вы хотите понять какую-то другую проблему, но так и не можете сформулировать, какую именно. Поэтому всё время обсуждаете какие-то не-проблемы.

0

10 месяцев назад

Nikita Repeev

Alexander Chichigin
Я не понимаю, чем вас не устраивает решение "не со...

Логический интерес я же сказал

0

10 месяцев назад

Nick Ivanych

А как делать \forall по таким определениям?

0

10 месяцев назад

Nikita Repeev

Nikita Repeev
Просто есть дополнительное требование которое мы х...

Стикер

0

10 месяцев назад

Alexander Chichigin Автор вопроса

Nick Ivanych
А как делать \forall по таким определениям?

А зачем? 😁

0

10 месяцев назад

Nick Ivanych

Alexander Chichigin
А зачем? 😁

Нутам, свойства записывать... Что для любого натурального числа то-то и то-то...

0

10 месяцев назад

Alexander Chichigin Автор вопроса

Nick Ivanych
Нутам, свойства записывать... Что для любого натур...

А, в этом смысле "∀ по определениям"... Раз уж я сказал, что определение в теории типов, то ∀ — Π-типами... 😁

0

10 месяцев назад

Nikita Repeev · Accepted Answer

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

Похожие чаты

А если мы конечные наты определим в теории типов при

16 ответов

Похожие вопросы