Ну например, арифметика пеано (PA) или теория цермело-франкеля (ZF). Именованные аксиомы (индукции в PA или подстановки в ZF) являются «схемами» аксиом - «рецептами» для получения бесконечного количества аксиом, с помощью подстановки в схему разных логических формул
интересно, что если ты попробуешь придумать процедуру, генерирующую бесконечную аксиоматику - она не станет от этого полной или консистентной, т.к. ее можно будет точно так же расписать по геделю. Если я правильно понял твой великий план ))))
вещи типа PA являлись фундаментом формализации важнейших вещей в математике (арифметика, свойства целых и натуральных чисел, итп), что в свою очередь привело ко всему, что мы сейчас имеем. Можно ли на основании этого сделать вывод, что оно используется везде?
это инфа не сто процентов, но для написания курсача можно глянуть на Type Arithmetic, которая в Haskell реализована в пакете type-level, который такой тормозной именно потому, что симулирует PA на десятичных числах. Практическая мотивация этому объяснена в статье Number-parameterized types
я же сморозил чушь) Например, очевидно что возможность бесконечных подстановок не означает настоящей бесконечности: в каждый фиксированный момент вычисления программы, система аксиом будет фиксированного размера. То есть, это даже не чушь, а скорей очередное капитанство
каждый фиксированный момент вычисления программы, система аксиом будет фиксированного размера не означает настоящей бесконечности
Не понимаю, что в данном случае настоящая бесконечность.
Например, для неконечного подмножества предложений аксиомы будут создаваться из схем аксиом. Какая разница, что в какой-то конкретный момент, на основании входных данных, мы создадим конечное количество аксиом? Разве я не пересказываю, что ты говорил?
О, кстати, погугли историю установки мемориальной доски на доме, где родился Кантор. Буквально, форму 9 или её аналог требовали. От 1845 года. И таки пришлось найти.
по изначальному топику непонятно, каких целей ты хочешь добиться) Изобрести новый язык программирования, доказать что гедель был неправ, написать курсач неважно какой, написать курсач _важно_ какой, изобрести формулу бога и открыть цифровое бессмертие, итп. Если тебя в такой постановке все устраивает, то это отлично - задача решена