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

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

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

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

Аффинная логика может быть включена в линейную логику путём переписывания аффинной стрелки ${\displaystyle A\rightarrow B}$ в линейную стрелку ${\displaystyle A\multimap B\otimes \top }$.

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

Аффинная логика составляет основу лудики^[англ.], анализа принципов.

Литература

• В.Н. Гришин, 1974. «Об одной нестандартной логике и её применении к теории множеств». Исследования по формализованным языкам и неклассической логике, 135-171. Издательство «Наука», Москва.
• В.Н. Гришин, 1981. «Предикатные и теоретико-множественные исчисления, основанные на логике без сокращений». Известия Академии наук СССР Серия математическая 45(1): 47-68. 239. Математика. Изв. СССР, 18, №1, Москва.
• J. Ketonen and R. Weyhrauch, 1984, A decidable fragment of predicate calculus. Theoretical Computer Science 32:297-307.
• J. Ketonen and G. Bellin, 1989. A decision procedure revisited: notes on Direct Logic. In Linear Logic and its Implementation.

См. также

• Релевантная логика
• Система аффинного типа^[англ.], система субструктурного типа^[англ.]

Примечания

1. Jean-Yves Girard, 1997. 'Affine Архивная копия от 1 августа 2023 на Wayback Machine'. Message to the TYPES mailing list.
2. Grishin, 1974, and later, Grishin, 1981.
3. Cf. Frederic Fitch's demonstrably consistent set theory