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

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

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

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

Аффинная логика может быть включена в линейную логику путём переписывания аффинной стрелки $A\rightarrow B$ в линейную стрелку $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.

См. также

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