Cтраница 1
Исчисление равенств в определенном смысле ( более широком, чем тот, который имеется в виду в предыдущей фразе) яВоТяется фундаментом разрабатываемого Гудстейпом варианта конструктивного математического анализа; этот вариант Гудстейн называет рекурсивным математическим анализом. [1]
С этой точки зрения исчисление равенств Гудстейна имеет ощутимое преимущество перед исчислением равенств Карри. [2]
Гудстейн, говоря о формализации рекурсивного анализа посредством исчисления равенств, подразумевает, по-видимому, возможность обоснования рассмотренных им ( и многих других) теорем вида ( 19) и упомянутых в § 8 видов в определенном сильном смысле, соответствующем определенному, сильному конструктивному истолкованию утверждений этих видов, которое полностью согласуется с используемым в конструктивной ма-тематике более общим истолкнованием суждений о конструктивных объектах, но предполагает относительную простоту определенных конструкций и связей. [3]
С этой точки зрения исчисление равенств Гудстейна имеет ощутимое преимущество перед исчислением равенств Карри. [4]
В настоящее время опубликовано уже значительное количество работ различных авторов, посвященных исчислениям равенств Для рекурсивных функций, функционалов и операторов различных Конкретных типов. Настоящая книга отражает лишь один из существенных этапов развития этого круга идей. [5]
Важную роль в понимании некоторых разделов этой книги играет следующее обобщение понятия вывода в исчислении равенств. [6]
Этот результат применим почти ко всем известным разрешимым теориям в логике, за исключением пропозиционального исчисления и исчисления чистого равенства. [7]
В следующем далее изложении рекурсивной арифметики мы показываем, что логику и арифметику можно строить одновременно в исчислении равенств со свободными переменными, в котором единственными утверждениями являются равенства вида а bt где а и & означают функциональные выражения. С помощью этого исчисления равенств можно построить логику и арифметику с самого начала, с полной строгостью и со всеми деталями на значительно более элементарном уровне, чем было возможно до сих пор, и есть надежда, что первая половина этой книги окажется до Ступной первокурснику университета, специализирующемуся по математике. [8]
Гудстейн в предисловии к монографии РА утверждает, что рекурсивный анализ ( так он называет разрабатываемый им вариант конструктивного математического анализа) формализуем в исчислении равенств, однако нигде в тексте РА не поясняет, какой смысл он вкладывает здесь в термин формализация. Конкретный материал, содержащийся в РА, свидетельствует о том, что это утверждение Гудстейна нельзя понимать в том смысле, что все теоремы рекурсивного анализа допускают запись в виде равенств и эти равенства выводимы в исчислении равенств. [9]
Можно провести рассуждение, опирающееся на формирующиеся в опыте обобщенные представления о натуральных числах и о процессах вычисления значении рекурсивных функций, результатом которого является заключение: любая формула, выводимая в исчислении равенств, представляет собой равенство, верное при любых значениях входящих в него предметных переменных. [10]
Эти функции на самом деле являются таблицами истинности, имеющими требуемые значения О, 1 для значений О, 1 переменных: функция а, связанная с доказуемым предложением А, удовлетворяет доказуемому равенству а 0 ( доказуемому, например, в исчислении равенств) и, обратно, предложение А доказуемо ( в некоторой формализации логики предложений), если равенство й 0 доказуемо. Обратно, если равенство а 0 доказуемо, то предложение Л, соответствующее а, доказуемо, ибо функция а является истинностной функцией для А, которая имеет значение О ( истина) для всех значений ( включая О, 1) своих переменных, а всегда верное предложение доказуемо. [11]
В следующем далее изложении рекурсивной арифметики мы показываем, что логику и арифметику можно строить одновременно в исчислении равенств со свободными переменными, в котором единственными утверждениями являются равенства вида а bt где а и & означают функциональные выражения. С помощью этого исчисления равенств можно построить логику и арифметику с самого начала, с полной строгостью и со всеми деталями на значительно более элементарном уровне, чем было возможно до сих пор, и есть надежда, что первая половина этой книги окажется до Ступной первокурснику университета, специализирующемуся по математике. [12]
Термин рекурсивная функция относят часто к ц-рекурси ным функциям. Именно Кли доказал эквивалентность общерекурсивных функций ( задава мых исчислением равенств) и ( л-рекурсивных функций. [13]
В монографии РТЧ устанавливается также, что теорема о неполноте аксиоматизаций арифметики, доказанная К. Геде-лем для традиционной аксиоматизации арифметики и ее расширений, переносится и на исчисление равенств и его расширения. [14]
Гильберта и Бернайса выводимы в его исчислении, а расшифровки всех правил вывода исчисления Гильберта и Бернайса являются допустимыми в его исчислении правилами вывода. В 1941 году Гудстейн представил в печать работу [6] ( опубликованную в 1945 году), в которой построено исчисление равенств, существенно от-личающееся по своему типу от исчисления Карри. Гудстейн доказал в этой работе ( ссылаясь на некоторые результаты Бернайса и Сколема), что его исчисление обладает всеми упомянутыми свойствами исчисления Карри. [15]