Полная версия

Главная arrow Логика arrow КАТЕГОРНАЯ ЛОГИКА

  • Увеличить шрифт
  • Уменьшить шрифт


<<   СОДЕРЖАНИЕ ПОСМОТРЕТЬ ОРИГИНАЛ   >>

Двухуровневая теорема дедукции

Рассмотрим теперь, как S может отражаться в ее метапогике SL, т.е. когда мы можем записывать в SL производные операции из S. Мы увидим, что S способна это делать, если SL замкнута относительно правила

т.е. когда правило (Ded) допустимо для SL. Заметим, что для SL правило (Ded) эквивалентно правилу

потому что в NL у нас имеются операции для перехода от В-С к Тн В <= С и обратно, а также от А»В- С к Ah В <= С и обратно («эквивалентность» здесь означает, что SL, замкнута относительно (Ded')).

В направлении снизу-вверх правило (Ded), которое мы отметим как (Ded)T, тривиально выводится во всех системах с помощью (TI- А), (А»В- Q -> (T*Bl- Q

Но в обратном направлении (Ded), т.е. (Ded)4 получается более сложным образом.

Заметим, что если SL замкнуто относительно (Ded), то система S должна представлять собой расширение М (не обязательно собственное). Мы имеем следующий вывод:

и аналогично мы выводим 0 —> ((А»В)»0- A»(B»Q) и 0 —> (A»Bh В»А) (для последней секвенции мы используем стрелки Тг^ и Tr's). Заметим, что мы не использовали (Assoc) и (Perm) в этих выводах. Таким образом, стрелки ВАВ.с, В°кв,с и Са.в необходимы для (Ded). Покажем теперь, что вместе с добавочными условиями этого достаточно.

Рассмотрим следующий перевод, т.е. биекцию 1 из Р2 в Р:

Мы можем доказать следующее предложение:

Предложение 5. Если М с S a L с S, то X —>/доказуема в

SL тогда и только тогда, когда t{X —> f) есть стрелка в S.

Доказательство. Слева направо доказываем индукцией по длине доказательства X -»/ в SL. Проблематическим случаем является ситуация, когда S сильна настолько же, насколько и М, при рассмотрении переводов аксиом, полученных по (»). Например, мы должны иметь в S стрелку (A z> В)»(С z> D)h (A»Q ->(B»D). Когда мы рассматриваем применение структурных правил, то видим, что L не может быть сильнее.

Справа налево по предложению 1 получаем 0 —> (t(X)h t(f)) как доказуемую стрелку в SL, а потом применяем стрелку («) с операцией ° и сечение, получая (TV t(X)) —> (Т(- /(/)). Если X имеет форму YZ, то мы используем операцию • и Т-стрелки, чтобы получить (TV /(У)), (TV t(Z)) -> (TV

Действуя аналогично, мы доходим до стрелок в последовательности Xи для каждой такой стрелки Ah В получаем (Ah В) -» (Ti- А з В). Используя обратную секвенцию для/, получаем X —>f. я

Предложение 6. Если М с S и L с S, то SL замкнуто относительно правила (Ded).

Доказательство. Мы имеем:

  • (1) (ТI— ^4) А' —>? (Bh С) в SL тогда и только тогда, когда (Tz>A)»t(X)h В z) С) в S по предложению 5,
  • (2) тогда и только тогда, когда t(X)h (А*В) => С в S,
  • (3) тогда и только тогда, когда X —> (A »Bh С) в SL. ?

Таким образом, стрелки вАвс, В°кв.с и Ca,s необходимы и достаточны для (Ded), при условии, что металогика S не сильнее S. Структурные правила (Assoc) и (Perm), ассоциированные с этими стрелками, не обязательно должны приниматься для металогики SL логики S. Но тот факт, что нам не потребовались структурные правила для SL, не означает, что SL не будет замкнута относительно этих структурных правил. Если SL и L будут такими, как в предложении 5 и 6, система S будет индуцировать структурные правила в SL, как это показывает следующее предложение.

Предложение 7. Если М с S и L с S, то SL и Ss содержат те же самые доказуемые секвенции.

Доказательство. Предположим X —>/есть стрелка в SL, а р: X' —» / получается из <р по одному из структурных правил (Assoc), ..., (Thin), которые мы имеем в SL. Тогда по предложению 5 слева направо, мы получаем стрелку /(ср) в S и без труда выводим, что t(i) также будет стрелкой в S. Следовательно, по предложению 5, справа налево получаем, что у:Х'—>/также будет стрелкой в SL. ?

 
<<   СОДЕРЖАНИЕ ПОСМОТРЕТЬ ОРИГИНАЛ   >>