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


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

480 ПРИЛОЖЕНИЕ [и
В качестве исходных формул в выводах допускаются: 1. Рекурсивные равенства, построенные по схеме примитивной рекурсии, и, значит, в частности, рекурсивные равенства для сложения и умножения, а также рекурсивные равенства для функций sgn(n) и sgn(n):
sgn(0) = 0, sgn(n') = 0', !gn~(0) = 0'(
2. Явные определения вида
f(nb .... nc) = t(n1, ..., /г,.),
где f — некоторый г-местный (ранее не использовавшийся) функциональный знак, a t(ni, ..., яг) — терм с единственными свободными переменными nlt ..., пк,
3. Формулы вида
Ъ (t (x), а) = sgn (t (a)) • &х (t (х), a') + sgn(t (a)) • а
JM(*) = Mt(*), 0),
где t (а) — какой-либо рекурсивный терм [схема формул (р,)].
Разрешаются следующие способы перехода от уже имеющихся формул к новым:
1. Подстановка какого-либо терма вместо всех вхождений данной свободной индивидной переменной в данную формулу.
2. Схема замены
о = Ь, Я (а)
где 91 (а) означает формулу, получающуюся из выражения 91 (г/) в результате замены буквы (именной переменно и) у термом a, a 91 (b) получается из 91 (у) в результате замены у термом Ь.
Замечание. Эту именную переменную мы не причисляем к свободным индивидным переменным, которые у нас считаются термами. Она используется лишь для описания схемы замены.
Описанный нами формализм (Z°) не содержит ни логических символов, ни формульных переменных. В качестве единственной
не формулируется. Это ограничение в рассматриваемом формализме оказывается на самом деле ненужным, так как не разрешается в качестве операции построения термов применять р.-символ к какому-либо терму, в котором уже содержится некоторый Д-символ, и поэтому терм вида jl^f (x, \ix\ (x, х)) может возникнуть лишь в результате замены какой-нибудь индивидной переменной термом НдД (х, х). Это обстоятельство позволяет нам обходиться здесь переменной х в качестве единственной связанной переменной.

 

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 481 482 483 484 485 486 487 488 489 490 500 510 520 530 540 550 560 570 580 590 600 610 620 630 640 650


Математика