Аффинная логика

Аффинная логика — это субструктурная логика теория доказательства которой отвергает структурное правило сокращения , . Ее также можно охарактеризовать как линейную логику с ослаблением .

Название «аффинная логика» связано с линейной логикой , от которой она отличается разрешением правила ослабления. Жан-Ив Жирар ввел это имя как часть геометрии взаимодействия семантики линейной логики, которая характеризует линейную логику с точки зрения линейной алгебры ; здесь он ссылается на аффинные преобразования в векторных пространствах . ^[1]

Аффинная логика предшествовала линейной логике. Эту логику использовал В. Н. Гришин в 1974 г. ^[2] после того, как заметил, что парадокс Рассела не может быть выведен в теории множеств без сжатия, даже с аксиомой неограниченного понимания . ^[3] Аналогичным образом, эта логика легла в основу разрешимой подтеории логики предикатов , названной «Прямая логика» (Кетонен и Вераух, 1984; Кетонен и Беллин, 1989).

Аффинную логику можно встроить в линейную логику, переписав аффинную стрелку. $A\rightarrow B$ как линейная стрелка $A\multimap B\otimes \top$ .

В то время как полная линейная логика (т.е. пропозициональная линейная логика с мультипликативами, добавками и экспонентами) неразрешима, полная аффинная логика разрешима.

Аффинная логика составляет основу лудики .

Примечания [ править ]

^ Жан-Ив Жирар , 1997. « Аффин ». Сообщение в список рассылки TYPES.
^ Grishin, 1974, and later, Grishin, 1981.
^ См. Фитча Фредерика Очевидно последовательная теория множеств

Ссылки [ править ]

В. Н. Гришин, 1974. «Нестандартная логика и ее приложение к теории множеств». Исследования по формализованным языкам и неклассической логике (русский), 135–171. Издат, «Наука», Москва.
V.N. Grishin, 1981. “Predicate and set-theoretic calculi based on logic without contraction rules,” (Russian). Izvestiya Akademii Nauk SSSR Seriya Matematicheskaya 45(1):47-68. 239. Math. USSR Izv., 18, no.1, Moscow.
Дж. Кетонен и Р. Вейраух, 1984, Разрешимый фрагмент исчисления предикатов. Теоретическая информатика 32:297-307.
Дж. Кетонен и Г. Беллин, 1989. Еще раз о процедуре принятия решения: заметки о прямой логике. В книге «Линейная логика и ее реализация» .

См. также [ править ]

Эта логике статья, посвященная , незавершена . Вы можете помочь Википедии, расширив ее .

[1] Жан-Ив Жирар , 1997. « Аффин ». Сообщение в список рассылки TYPES.

[2] Grishin, 1974, and later, Grishin, 1981.

[3] См. Фитча Фредерика Очевидно последовательная теория множеств

[1]

[2]

[3]