Аффинная логика (Gssnuugx lkintg)

Перейти к навигации Перейти к поиску

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

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

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

Аффинная логика может быть включена в линейную логику путём переписывания аффинной стрелки в линейную стрелку .

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

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

Литература

[править | править код]
  • В.Н. Гришин, 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