Русская Википедия:Аффинная логика

Материал из Онлайн справочника
Перейти к навигацииПерейти к поиску

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

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

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

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

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

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

Литература

  • В.Н. Гришин, 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'. Message to the TYPES mailing list.
  2. Grishin, 1974, and later, Grishin, 1981.
  3. Cf. Frederic Fitch's demonstrably consistent set theory

Шаблон:Логика