Interested Article - Аффинная логика

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

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

Аффинная логика появилась раньше линейной логики. В.Н. Гришин использовал эту логику в 1974 году, заметив, что парадокс Рассела невозможно вывести в теории множеств , без контракции , даже с аксиомой неограниченного понимания ( ). Аналогичным образом данная логика составила основу разрешимого подраздела теории логики первого порядка , названной « » (Кетонен и Вехраух, 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. 32:297-307.
J. Ketonen and G. Bellin, 1989. A decision procedure revisited: notes on Direct Logic. In Linear Logic and its Implementation .