Когерентность в декартово замкнутых генценовских дедуктивных мультикатегориях
Данная теорема позволяет не только отождествить стрелки, но и различить их, что особенно важно в случае использования только одной переменной. Так, если воспользоваться нашими стрелками и gc{(fh'T) то даже в случае секвенции АН Ал (А з А) эти стрелки легко различаются своей общностью. Теорема когерентности. Если hu h2: ГI- А представляют собой свободные от сечения стрелки в свободной декартово… Читать ещё >
Когерентность в декартово замкнутых генценовских дедуктивных мультикатегориях (реферат, курсовая, диплом, контрольная)
Итак, согласно результатам предыдущего параграфа, чтобы проверить, коммутирует ли диаграмма стрелок, достаточно вычертить связи стрелок из диаграммы и проверить, равны ли они. Для декартово замкнутых генценовских дедуктивных мультикатегорий (т.е. генценовских мультикатегорий, надстроенных над декартово замкнутой генценовской дедуктивной системой) существует еще более простой способ обнаружения подобной когерентности (см. [Szabo 1989]).
Будем говорить, что все стрелки нашей мультикатегории расширены до конгруэнтных стрелок, если они заменены на стрелки, не включающие в свою конструкцию фрагменты, эквивалентные стрелке ослабления, и в которых стрелки типа g{f} предшествуют стрелкам типа / лg, всегда, когда это синтаксически возможно. Теперь в качестве стрелок будут рассматриваться только свободные от сечения расширенные стрелки. С каждой стрелкой f: TV А мы ассоциируем пару, а > [3 последовательностей аир букв, устанавливающих упорядоченную связь между переменной в заключении/ и ее прототипами в исходных стрелках, по которым сконструирована / Будем называть пару, а > Р алфавитным следом f Последовательность а получается путем замещения каждого вхождения переменной в последовательность формул Г, А по порядку слева направо на различающиеся между собой буквы. Мы допускаем, что для этой цели у нас в распоряжении имеется бесконечный алфавит. Если Г, А не содержит переменных, то а пуста. Затем мы переписываем доказательство, переименовывая все прототипы переменной согласно их новым именам в а. Последовательность р представляет собой последовательность букв, полученных путем считывания имен по мере их появления в исходных стрелках конструкции /слева направо. Если н Т является единственной исходной стрелкой f то р пуста. Таким образом, также разрешаются «пары» 0 > р и 0 > 0.
Пусть, например, у нас имеются два доказательства.
Их алфавитные следы будут выглядеть следующим образом:
Определение. Общность (generality) стрелки / Гн А еегь алфавитный след расширения/": ГН А стрелки/.
Используя понятие общности, можно доказать следующую теорему [Szabo 1989, р. 294].
Теорема когерентности. Если hu h2: ГI- А представляют собой свободные от сечения стрелки в свободной декартово замкнутой генценовской дедуктивной мультикатегории, то ht = h2 тогда и только тогда, когда h и h2 имеют одну и ту же общность.
Данная теорема позволяет не только отождествить стрелки, но и различить их, что особенно важно в случае использования только одной переменной. Так, если воспользоваться нашими стрелками и gc{(fh'T) то даже в случае секвенции АН Ал (А з А) эти стрелки легко различаются своей общностью.