Избранное
ЭБ Нефть
и Газ
Главная
Оглавление
Поиск +
Еще книги ...
Энциклопедия
Помощь
Для просмотра
необходимо:


Книга: Главная » Гильберт Д.N. Основания математики Теория доказательств
 
djvu / html
 

550 ПРИЛОЖЕНИЕ flV
Всякое явное определение представляет собой формулу одного ; из следующих трех видов: ;
здесь t — терм, g — функционал, с — свободная индивидная пере- , менная, *& — формула, а ё, f и S — выражения, состоящие из вновь вводимого символа и его аргументов. При этом в обеих частях соответствующего равенства или эквивалентности должны фигурировать одни и те же свободные переменные. Аргументные места формульных переменных, фигурирующих в качестве аргументов вновь вводимых символов, указываются путем заполнения "• связанными индивидными или соответственно функциональными'' переменными; аргументное место фигурирующей в качестве аргумента функциональной переменной а во вновь вводимом символе,, указывается только тогда, когда в правой части определения i переменная л не фигурирует сама по себе, но и в этом случае. это аргументное место можно не указывать. Связанные перемен-: ные, используемые для указания аргументных мест аргументов вновь вводимых символов, должны быть попарно различны; помимо соответствующих аргументных мест, они записываются и. у самого этого символа — в качестве индексов или каким-нибудь } другим образом. '
Схема явного определения представляет собой правило, согласно которому любое явное определение может быть ; добавлено к формализму в качестве исходной формулы, причем выражение, состоящее из введенного символа и его аргументов,7 а также любое выражение, получающееся из него в результате ! каких-либо подстановок вместо его свободных переменных (если ', при этом не происходит коллизий между связанными переменными), допускается в качестве терма, или функционала, или формулы, смотря по тому, какой — первый, второй или третий — вид имеет ; это явное определение. Разумеется, правило переименования связанных переменных распространяется и на связанные переменные вновь введенных символов. :>
Присоединение этой схемы к формализму Я0 дает нам новый ' формализм, который мы будем называть формализмом Я. При; исследовании вопроса о непротиворечивости Я формализм этот ; с помощью общего метода исключения явных определений може*^ быть сведен к формализму Я0. В самом деле, наши соглашения^? касающиеся внешнего вида явных определений, выбраны с таким-расчетом, чтобы этот метод оказался применимым *). •
:„<
г) Особого рассмотрения требует случай, когда вновь вводимый символ. имеет одну или несколько функциональных переменных в качестве аргументов.

 

1 10 20 30 40 50 60 70 80 90 100 110 120 130 140 150 160 170 180 190 200 210 220 230 240 250 260 270 280 290 300 310 320 330 340 350 360 370 380 390 400 410 420 430 440 450 460 470 480 490 500 510 520 530 540 550 551 552 553 554 555 556 557 558 559 560 570 580 590 600 610 620 630 640 650


Математика