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

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

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


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

Секвенциальные двухуровневые дедуктивные системы

Расширим теперь S2 за счет дополнительных структурных правил. Первое из них получается путем замены правила

на два правила

где двойная черта означает, что данное правило работает как вверх, так и вниз.

Затем вводим следующие дополнительные правила:

Системы S2 для некоторой системы S разрабатываются, как правило, для записи производных операций в S, а не для операций, допустимых для S, т.е. таких, что, будучи добавленными к S, они не приводят к увеличению количества доказуемых стрелок. Операции, которые, например, могут привести нас от TV А»В к Тн А, допустимы для NL (см. главу вторую), но в формулировке NL у нас нет операций на стрелках, примитивных или производных, которые можно применить к TV А»В для получения Тн- А. Соответственно, в NL2 (или в некотором из его расширений типа NL2 + ( ), ( )*2, (Assoc), (Perm)) у нас не будет для каждого А и В секвенции (Тн Л»5)-> (TV А). Таким образом, если мы должны сформулировать систему в Р с примитивной операцией, которая допустима для нашей системы, но мы не хотим иметь ее во всех расширениях, то нам следует не рассматривать эту операцию в рамках i( > - (°). Не каждая формулировка системы S может служить в качестве исходного пункта для построения S2 и ее расширений.

С помощью структурных правил мы получаем следующие системы в Р2:

В расширениях SK следующее правило

дает такой же результат, как и (Expans). С его помощью мы опреде- леяем S™ как

SRM = SR + (Mingle).

Пусть теперь L обозначает одну из систем NL, AL, ... , J, a SL будет одной из выше сформулированных в Р2 систем. Если мы введем в Р2 связки *2, з2 и с2, связывающие стрелки Р, и константу Т2, а затем расширим SL с помощью правил

то мы получим удвоение логики системы L в Р2для Р. Таким образом, в SL возникают две логики, одна на низшем уровне S, а вторая на высшем уровне SL, и эти две логики не обязательно должны быть тождественными. Одна из них может быть более слабой, или даже они могут быть не сравнимыми между собой.

Все наши металогики SL достоверны для S настолько, насколько это касается доказуемых стрелок, т.е. легко можно доказать следующее

Предложение 4. Секвенция 0 —> / доказуема в двухуровневом дедуктивном исчислении SL тогда и только тогда, когда / есть стрелка S.

Доказательство. Слева направо показываем по длине доказательства, что если X —» /доказуема в SL, то все стрелки из X будут стрелками S лишь тогда, когда / содержится в S. В противоположную сторону индукция проходит также без затруднений. ?

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