Logika afiniczna

Logika afiniczna jest logiką podstrukturalną , której teoria dowodu odrzuca strukturalną regułę kontrakcji . Można go również scharakteryzować jako logikę liniową z osłabieniem .

Nazwa „logika afiniczna” jest związana z logiką liniową , od której różni się dopuszczeniem reguły osłabienia. Jean-Yves Girard wprowadził tę nazwę jako część geometrii semantyki interakcji logiki liniowej, która charakteryzuje logikę liniową w kategoriach algebry liniowej ; tutaj nawiązuje do przekształceń afinicznych w przestrzeniach wektorowych .

Logika afiniczna wyprzedziła logikę liniową. VN Grishin użył tej logiki w 1974 roku, po zaobserwowaniu, że paradoksu Russella nie można wyprowadzić z teorii mnogości bez skrócenia, nawet z aksjomatem nieograniczonego rozumienia . Podobnie logika stanowiła podstawę rozstrzygalnej podteorii logiki predykatów , zwanej „logiką bezpośrednią” (Ketonen i Wehrauch, 1984; Ketonen i Bellin, 1989).

$displaystyle$ przepisując strzałkę afiniczną strzałkę liniową $A \ rightarrow B$ }

Podczas gdy pełna logika liniowa (tj. liniowa logika zdaniowa z multiplikatywami, dodatkami i wykładniczymi) jest nierozstrzygalna, pełna logika afiniczna jest rozstrzygalna.

Podstawą ludyki jest logika afiniczna .

Notatki

• VN Grishin, 1974. „Niestandardowa logika i jej zastosowanie w teorii mnogości” (rosyjski). Studies in Formalized Languages ​​and Nonclassical Logics (rosyjski), 135–171. Izdat, „Nauka”, Moskwa.
• VN Grishin, 1981. „Rachunki predykatów i teorii mnogości oparte na logice bez reguł kontrakcji” (rosyjski). Izvest Akademiiya Nauk SSSR Seriya Matematicheskaya 45(1):47-68. 239. Matematyka. ZSRR Izv., 18, nr 1, Moskwa.
• J. Ketonen i R. Weyhrauch, 1984, Rozstrzygalny fragment rachunku predykatów. Informatyka teoretyczna 32:297-307.
• J. Ketonen i G. Bellin, 1989. Ponowna analiza procedury decyzyjnej: uwagi dotyczące logiki bezpośredniej. W logice liniowej i jej implementacji .

Zobacz też

• Ścisła logika i odpowiednia logika
• System typu afinicznego , system typu podstrukturalnego