Модальды логикада Сальквист формулалары – ерекше қасиеттері бар модальды формулалар. Теорема, каноникалық және бірінші реттік формулалармен анықталатын Kripke жүйелерімен сәйкес келеді.
Ағылшыншамен салыстырыңыз: абзацты басыңыз — түпнұсқа терезеде ашылады. Абзац астындағы EN түймесі оны мәтін ішінде көрсетеді.
Мазмұны
Кіріспе
Модальдық логикада Сальквист формулалары – ерекше қасиеттері бар модальдық формулалардың белгілі бір түрі. Сальквист сәйкестік теоремасы бойынша, кез келген Сальквист формуласы каноникалық болып табылады және бірінші реттік формуламен сипатталатын Крипке кадрларының класына сәйкес келеді. Сальквисттің берген анықтамасы бірінші реттік сәйкестіктері бар модальдық формулалардың шешімді жиынын анықтайды. Шагрова теоремасына сәйкес, кез келген модальдық формуланың бірінші реттік сәйкестігі бар-жоғы шешілмейтіндіктен, Sahlqvist [Chagrova 1991] емес, бірінші реттік кадр талаптарына ие формулалар бар (төмендегі мысалдарды қараңыз). Осылайша, Сальквист формулалары бірінші реттік сәйкестіктері бар модальдық формулалардың тек шешімді кіші жиынын ғана анықтайды.
In modal logic, Sahlqvist formulas are a certain kind of modal formula with remarkable properties. The Sahlqvist correspondence theorem states that every Sahlqvist formula is canonical, and corresponds to a class of Kripke frames definable by a first order formula. Sahlqvist's definition characterizes a decidable set of modal formulas with first order correspondents. Since it is undecidable, by Chagrova's theorem, whether an arbitrary modal formula has a first order correspondent, there are formulas with first order frame conditions that are not Sahlqvist [Chagrova 1991] (see the examples below). Hence Sahlqvist formulas define only a (decidable) subset of modal formulas with first order correspondents.
Анықтама
Сальквист формулалары импликациялардан құрылады, онда соңы оң, ал алды шектеулі формада болады. Қорапталған атом – санның (мүмкін 0) алдында тұратын логикалық атом, яғни (көбінесе деп қысқартылады) түріндегі формула. Сальквист алды – ∧, ∨ және қорапталған атомдардан, сондай-ақ теріс формулалардан (оның ішінде ⊥ және ⊤ тұрақтыларынан) құрылған формула. Сальквист импликациясы – A → B формуласы, мұнда A – Сальквист алды, ал B – оң формула. Сальквист формуласы Сальквист импликацияларынан ∧ және (шектеусіз) операторларын қолдану арқылы, ал ортақ айнымалылары жоқ формулаларда ∨ операторын қолдану арқылы құрастырылады.
Sahlqvist formulas are built up from implications, where the consequent is positive and the antecedent is of a restricted form. A boxed atom is a propositional atom preceded by a number (possibly 0) of boxes, i. e. a formula of the form (often abbreviated as for ). A Sahlqvist antecedent is a formula constructed using ∧, ∨, and from boxed atoms, and negative formulas (including the constants ⊥, ⊤). A Sahlqvist implication is a formula A → B, where A is a Sahlqvist antecedent, and B is a positive formula. A Sahlqvist formula is constructed from Sahlqvist implications using ∧ and (unrestricted), and using ∨ on formulas with no common variables.
Сальквистке жатпайтын формулалардың мысалдары
Бұл МакКинзи формуласы; оның бірінші реттік шеңберлік шарты жоқ. Лёб аксиомасы Сальквист аксиомасы емес; қайта, оның да бірінші реттік шеңберлік шарты жоқ. МакКинзи формуласы мен (4) аксиомасының қосылысы бірінші реттік шеңберлік шартқа ие (транзитивтілік қасиетінің белгілі бір қасиетпен қосылысы), бірақ ол кез келген Сальквист формуласына тең емес.
This is the McKinsey formula; it does not have a first order frame condition. The Löb axiom is not Sahlqvist; again, it does not have a first order frame condition. The conjunction of the McKinsey formula and the (4) axiom has a first order frame condition (the conjunction of the transitivity property with the property ) but is not equivalent to any Sahlqvist formula.
Крахт теоремасы
Сальквист формуласы қалыпты модальді логикада аксиома ретінде қолданылғанда, логика аксиома анықтайтын кадрлардың негізгі элементарлық класына қатысты толықтығы кепілдігі беріледі. Бұл нәтиже Сальквист толықтығы теоремасынан [Modal Logic, Blackburn et al., Theorem 4.42] туындайды. Бірақ сондай-ақ кері теорема да бар, яғни Сальквист формулаларының қай бірінші реттік шарттарға сәйкес келетінін көрсететін теорема. Крахт теоремасы кез келген Сальквист формуласы жергілікті түрде Крахт формуласына сәйкес келеді десе, керісінше, әрбір Крахт формуласы Крахт формуласынан тиімді түрде алуға болатын бір Сальквист формуласының жергілікті бірінші реттік сәйкестігі болып табылады [Modal Logic, Blackburn et al., Theorem 3.59].
When a Sahlqvist formula is used as an axiom in a normal modal logic, the logic is guaranteed to be complete with respect to the basic elementary class of frames the axiom defines. This result comes from the Sahlqvist completeness theorem [Modal Logic, Blackburn et al., Theorem 4.42]. But there is also a converse theorem, namely a theorem that states which first order conditions are the correspondents of Sahlqvist formulas. Kracht's theorem states that any Sahlqvist formula locally corresponds to a Kracht formula; and conversely, every Kracht formula is a local first order correspondent of some Sahlqvist formula which can be effectively obtained from the Kracht formula [Modal Logic, Blackburn et al., Theorem 3.59].