Cтраница 2
Исчисление предикатов занимается теорией вывода, основанной на структуре предложений, использующей связки, предикаты и кванторы. Таким образом, оно, в частности, представляет собой расширение исчисления высказываний. Тот тип исчисления предикатов, который мы будем рассматривать, допускает применение кванторов только к предметным переменным. Чтобы отличить этот простой тип исчисления от других, его обычно называют узким исчислением предикатов или исчислением предикатов первого порядка. [16]
Хотя в период разработки формализма господствовало убеждение, что формулы суть отображения более абстрактных и, главное, более истинных математических высказываний, они и манипуляции с ними не были самоцелью; формулы служили для того, чтобы выразить и передать математические факты. Тогда, в самом начале двадцатого столетия, еще до того, как формализм принял до некоторой степени окончательный облик, произошли два события: во-первых, обнаружилось, что неограниченное применение кванторов фактически приводит к противоречиям, и, во-вторых, Брауэр ( еще в своей диссертации Over de grondslagen der wiskunde 11, Амстердам и Лейпциг, 1907) выяснил, что принцип tertium non datur12 не может апеллировать к очевидности, если он применяется к высказываниям, в которых кванторы существуют и все относятся не к множеству отдельно указанных объектов, а к бесконечным множествам, таким, как, например, множество натуральных чисел или даже множество всех возможных бесконечных последовательностей таких чисел. В результате открылись два пути: брауэровский интуиционизм, который ограничивается наглядно очевидными высказываниями ( основанными на математической праинтуиции) и не превращает открытый в бесконечность ряд натуральных чисел в замкнутую область существующих самих по себе элементов, и гильбертовский формализм, в котором высказывания заменены лишенными смысла формулами, и поэтому применение кванторов ограничивается лишь заботой о том, чтобы не возникало никаких противоречий. [17]