Рұқсат етілген ереже - Admissible rule

Жылы логика, а қорытынды жасау ережесі болып табылады рұқсат етілген ішінде ресми жүйе егер жиынтығы теоремалар бұл ереже жүйенің бар ережелеріне қосылған кезде жүйенің өзгеруі болмайды. Басқаша айтқанда, әрқайсысы формула болуы мүмкін алынған бұл ережені қолдану онсыз да осы ережеден туындайтындықтан, белгілі бір мағынада бұл артық. Рұқсат етілген ереже ұғымы енгізілді Пол Лоренсен (1955).

Анықтамалар

Құрылымдық ережелер жағдайында ғана рұқсат ету жүйелі түрде зерттелген ұсыныстық классикалық емес логика, оны келесіде сипаттайтын боламыз.

Негізгі жиынтығы болсын пропозициялық байланыстырғыштар бекітілген (мысалы, ${ displaystyle { to, land, lor, bot }}$ жағдайда суперинтуитивті логика, немесе ${ displaystyle { to, bot, Box }}$ жағдайда мономодальды логика ). Жақсы құрылған формулалар а-дан осы қосылғыштарды қолдану арқылы еркін салынған шексіз жиынтығы пропозициялық айнымалылар б₀, б₁, .... A ауыстыру σ - бұл қосылғыштармен жүретін формулалардан формулаларға дейінгі функция, яғни.

${ displaystyle sigma f (A_ {1}, нүктелер, A_ {n}) = f ( sigma A_ {1}, нүктелер, sigma A_ {n})}$

әр қосылғыш үшін f, және формулалар A₁, ..., A_n. (Сондай-ақ, біз as формулалар жиынтығына алмастыруларды қолдана аламыз σΓ = {σA: A ∈ Γ}.) Тарский стилі салдарлық қатынас^[1] қатынас болып табылады ${ displaystyle vdash}$ формулалар жиынтығы мен формулалар арасында, мысалы

барлық формулалар үшін A, B, және формулалар жиынтығы Γ, Δ. Осыған байланысты қатынас

барлық ауыстырулар үшін σ деп аталады құрылымдық. (Мұнда және төменде қолданылған «құрылымдық» термині ұғымымен байланысты емес екенін ескеріңіз құрылымдық ережелер жылы дәйекті кальций.) Құрылымдық салдарлық қатынас а деп аталады ұсыныстық логика. Формула A - логиканың теоремасы ${ displaystyle vdash}$ егер ${ displaystyle varnothing vdash A}$.

Мысалы, біз суперинтуициялық логиканы анықтаймыз L оның стандартты салдарлық қатынасымен ${ displaystyle vdash _ {L}}$ аксиоматизацияланатын modus ponens және аксиомалар, және біз а қалыпты модальді логика оның әлемдік салдарлық қатынасымен ${ displaystyle vdash _ {L}}$ модус поненстерімен, қажеттілігімен және аксиомаларымен аксиоматизацияланған.

A құрылымдық қорытынды ережесі^[2] (немесе жай ереже қысқаша) жұппен беріледі (Γ,B), әдетте ретінде жазылады

${ displaystyle { frac {A_ {1}, нүктелер, A_ {n}} {B}} qquad { text {or}} qquad A_ {1}, нүктелер, A_ {n} / B, }$

мұндағы Γ = {A₁, ..., A_n} - формулалардың ақырлы жиыны, және B формула болып табылады. Ан данасы ереже болып табылады

${ displaystyle sigma A_ {1}, нүктелер, sigma A_ {n} / sigma B}$

ауыстыру үшін σ. Ереже Γ /B болып табылады туынды жылы ${ displaystyle vdash}$, егер ${ displaystyle Gamma vdash B}$. Бұл рұқсат етілген егер ереженің әрбір данасы үшін болса, σB барлық формулалар теорема болған кезде теорема болады.^[3] Басқаша айтқанда, егер логикаға қосылған кезде жаңа теоремаларға әкелмесе, ереже рұқсат етіледі.^[4] Біз де жазамыз ${ displaystyle Gamma , | ! ! ! sim B}$ егер Γ /B рұқсат етілген. (Ескертіп қой ${ displaystyle | ! ! ! sim}$ - бұл құрылымдық салдарлық қатынас.)

Кез-келген туындайтын ереже рұқсат етіледі, бірақ жалпы керісінше емес. Логика - бұл құрылымдық жағынан толық егер әрбір рұқсат етілген ереже туынды болса, яғни ${ displaystyle { vdash} = {, | ! ! ! sim}}$.^[5]

Жақсы мінезді логикада конъюнкция дәнекер (суперинтуициялық немесе модальды логика сияқты), ереже ${ displaystyle A_ {1}, нүкте, A_ {n} / B}$ дегенге тең ${ displaystyle A_ {1} land dots land A_ {n} / B}$ қол жетімділікке және туындыға қатысты. Сондықтан тек онымен күресу әдетке айналған унарий ережелер A/B.

Мысалдар

• Классикалық пропозициялық есептеу (КҚК) құрылымдық жағынан аяқталған.^[6] Шынында да, солай деп ойлаңыз A/B туынды емес ереже болып табылады және тапсырманы бекітеді v осындай v(A) = 1, және v(B) = 0. Әрбір айнымалы үшін itution алмастырғышын анықтаңыз б, σб = ${ displaystyle top}$ егер v(б) = 1 және σб = ${ displaystyle bot}$ егер v(б) = 0. Сонда σA теорема, бірақ σB емес (шын мәнінде, ¬σB теорема болып табылады). Осылайша ереже A/B рұқсат етілмейді. (Дәл осындай дәлел кез келгенге қатысты көп мәнді логика L логикалық матрицаға қатысты барлық элементтері тілінде аталады L.)
• The Крейзель –Путнам ереже (а.к.а.) Харроп ережесі немесе алғышарт ережесінің тәуелсіздігі)

${ displaystyle ({ mathit {KPR}}) qquad { frac { neg p to q lor r} {( neg p to q) lor ( neg p to r)}}}$

рұқсат етілген интуитивтік пропозициялық есептеу (IPC). Шындығында, бұл кез-келген суперинтуициялық логикада рұқсат етіледі.^[7] Екінші жағынан, формула

${ displaystyle ( neg p to q lor r) to (( neg p to q) lor ( neg p to r))}$

интуитивті тавтология емес, демек КПР туынды емес IPC. Соның ішінде, IPC құрылымдық жағынан толық емес.

• Ереже

${ displaystyle { frac { Box p} {p}}}$

сияқты көптеген модальды логикаларда рұқсат етіледі Қ, Д., Қ4, S4, GL (қараңыз мына кесте модальді логика атаулары үшін). Бұл туынды S4, бірақ ол туынды емес Қ, Д., Қ4, немесе GL.

• Ереже

${ displaystyle { frac { Diamond p land Diamond neg p} { bot}}}$

әрбір қалыпты модальді логикада рұқсат етіледі.^[8] Бұл туынды GL және S4.1, бірақ ол туынды емес Қ, Д., Қ4, S4, S5.

• Лобтың ережесі

${ displaystyle ({ mathit {LR}}) qquad { frac { Box p - p} {p}}}$

негізгі модальді логикада рұқсат етілген (бірақ туынды емес) Қ, және ол туынды болып табылады GL. Алайда, LR рұқсат етілмейді Қ4. Атап айтқанда, бұл емес тұтастай алғанда, логикаға сәйкес келетін ереже L оның кеңейтілуіне жол берілуі керек.

• The Годель - Дамметт логикасы (LC) және модальді логика Grz.3 құрылымдық жағынан аяқталған.^[9] The өнімнің анық емес логикасы құрылымдық жағынан да аяқталған.^[10]

Шешімділік және төмендетілген ережелер

Берілген логиканың рұқсат етілген ережелері туралы негізгі сұрақ - барлық рұқсат етілген ережелер жиынтығы ма шешімді. Логиканың өзі (яғни, оның теоремалар жиынтығы) болса да, мәселе нривиальды емес екенін ескеріңіз шешімді: ереженің рұқсат етілуін анықтау A/B шексіз байланысты әмбебап квантор барлық пропозициялық ауыстырулардың үстінен априори біз тек шешімді логикада ережеге жол берілетіндігін білеміз ${ displaystyle Pi _ {1} ^ {0}}$ (яғни оның толықтырушысы болып табылады рекурсивті түрде санауға болады ). Мысалы, бимодальды логикада рұқсат етілетіні белгілі Қ_сен және Қ4_сен (кеңейтімдері Қ немесе Қ4-пен әмбебап модальділік ) шешілмейді.^[11] Бір қызығы, негізгі модальді логикада рұқсаттың шешімділігі Қ негізгі ашық проблема болып табылады.

Дегенмен, көптеген модальді және суперинтуициялық логикаларда ережелердің рұқсат етілуі шешуші болып табылады. Негізгі өтпелі модальді логикада рұқсат етілген ережелер бойынша алғашқы шешім процедураларын құрастырды Рыбаков, пайдаланып ережелердің қысқартылған нысаны.^[12] Айнымалылардағы модальды ереже б₀, ..., б_к формасы болса, кішірейтілген деп аталады

${ displaystyle { frac { bigvee _ {i = 0} ^ {n} { bigl (} bigwedge _ {j = 0} ^ {k} neg _ {i, j} ^ {0} p_ { j} land bigwedge _ {j = 0} ^ {k} neg _ {i, j} ^ {1} Box p_ {j} { bigr)}} {p_ {0}}},}$

қайда ${ displaystyle neg _ {i, j} ^ {u}}$ не бос, не жоққа шығару ${ displaystyle neg}$. Әр ереже үшін р, біз қысқартылған ережені тиімді құра аламыз с (қысқартылған түрі деп аталады р) кез-келген логика мойындайтын (немесе шығаратын) р егер ол мойындаса (немесе шығарса) с, енгізу арқылы кеңейтілетін айнымалылар барлық субформулалар үшін A, және нәтижені толығымен білдіру дизъюнктивті қалыпты форма. Осылайша, қысқартылған ережелердің рұқсат етілуі үшін шешім алгоритмін құру жеткілікті.

Келіңіздер ${ displaystyle textstyle bigvee _ {i = 0} ^ {n} varphi _ {i} / p_ {0}}$ жоғарыдағыдай қысқартылған ереже болыңыз. Біз әр конъюнктураны анықтаймыз ${ displaystyle varphi _ {i}}$ жиынтығымен ${ displaystyle { neg _ {i, j} ^ {0} p_ {j}, neg _ {i, j} ^ {1} Box p_ {j} mid j leq k }}$ оның жалғаулықтары. Кез-келген ішкі жиын үшін W жиынтықтың ${ displaystyle { varphi _ {i} mid i leq n }}$ барлық қосылғыштардың ішінен а анықтайық Крипке моделі ${ displaystyle M = langle W, R, { Vdash} rangle}$ арқылы

${ displaystyle varphi _ {i} Vdash p_ {j} iff p_ {j} in varphi _ {i},}$

${ displaystyle varphi _ {i} , R , varphi _ {i '} iff forall j leq k , ( Box p_ {j} in varphi _ {i} Rightarrow { p_ {j}, Box p_ {j} } subseteq varphi _ {i '}).}$

Содан кейін келесі рұқсаттың алгоритмдік критерийін ұсынады Қ4:^[13]

Теорема. Ереже ${ displaystyle textstyle bigvee _ {i = 0} ^ {n} varphi _ {i} / p_ {0}}$ болып табылады емес рұқсат етілген Қ4 егер ол бар болса ғана ${ displaystyle W subseteq { varphi _ {i} mid i leq n }}$ осындай

1. ${ displaystyle varphi _ {i} nVdash p_ {0}}$ кейбіреулер үшін ${ displaystyle i leq n,}$
2. ${ displaystyle varphi _ {i} Vdash varphi _ {i}}$ әрқайсысы үшін ${ displaystyle i leq n,}$
3. әр ішкі жиын үшін Д. туралы W элементтер бар ${ displaystyle alpha, beta in W}$ эквиваленттер

${ displaystyle alpha Vdash Box p_ {j}}$ егер және егер болса ${ displaystyle varphi Vdash p_ {j} land Box p_ {j}}$ әрқайсысы үшін ${ displaystyle varphi in D}$

${ displaystyle alpha Vdash Box p_ {j}}$ егер және егер болса ${ displaystyle alpha Vdash p_ {j}}$ және ${ displaystyle varphi Vdash p_ {j} land Box p_ {j}}$ әрқайсысы үшін ${ displaystyle varphi in D}$

бәріне арналған j.

Логикаға ұқсас өлшемдерді табуға болады S4, GL, және Grz.^[14] Сонымен қатар, интуитивтік логикаға жол берілу рұқсат етілгенге дейін азайтылуы мүмкін Grz пайдаланып Годель – МакКинси – Тарский аудармасы:^[15]

${ displaystyle A , | ! ! ! sim _ {IPC} B}$ егер және егер болса ${ displaystyle T (A) , | ! ! ! sim _ {Grz} T (B).}$

Рыбаков (1997) транзиттік (шексіз) классына қолданылатын рұқсат етімділіктің шешімділігін көрсететін әлдеқайда күрделі әдістерді дамытты (яғни кеңейтеді). Қ4 немесе IPC) модальді және суперинтуитивті логика, соның ішінде. S4.1, S4.2, S4.3, KC, Т_к (сонымен бірге жоғарыда аталған логика IPC, Қ4, S4, GL, Grz).^[16]

Шешімді бола тұра, рұқсат ету проблемасы салыстырмалы түрде жоғары есептеу күрделілігі, қарапайым логикада да: негізгі өтпелі логикадағы ережелердің рұқсат етілуі IPC, Қ4, S4, GL, Grz болып табылады coNEXP -толық.^[17] Мұны осы логикадағы туындылық проблемасымен (ережелер немесе формулалар үшін) қарама-қарсы қою керек, яғни PSPACE -толық.^[18]

Проективтілік және унификация

Ұсыныстар логикасындағы жол берілу біртұтастырумен тығыз байланысты теңдеу теориясы туралы модальды немесе Алгебралар. Байланысты Гиларди дамытты (1999, 2000). Логикалық қондырғыда а біріктіруші формуладан A логикада L (ан L-қысқартқыш) дегеніміз σ болатындай subst ауыстыруA теоремасы болып табылады L. (Осы ұғымды қолдана отырып, біз ереженің рұқсат етілуін қайта түсіндіре аламыз A/B жылы L сияқты «әрқайсысы L- біріктіруші A болып табылады L- біріктіруші B«.) Ан L- біріктіруші σ болып табылады жалпы емес қарағанда Lun, егер a ауыстыру болса, σ ≤ τ деп жазылған un біріктіруші

${ displaystyle vdash _ {L} sigma p leftrightarrow upsilon tau p}$

әр айнымалы үшін б. A біріктіргіштердің толық жиынтығы формуладан A жиынтық S туралы L- біріктірушілер A осылай әрқайсысы L- біріктіруші A кейбір біріктіргіштен гөрі жалпы емес S. A ең жалпы біріктіргіш (mgu) of A - бұл біріктіргіш is, сондықтан {σ} - бұл біріктіргіштердің толық жиынтығы A. Бұдан шығатыны: егер S қосылғыштарының толық жиынтығы болып табылады A, содан кейін ереже A/B болып табылады L- егер әр σ дюйм болса ғана рұқсат етіледі S болып табылады L- біріктіруші B. Осылайша, біз біртұтастырғыштардың жақсы жиынтығын таба алсақ, рұқсат етілген ережелерді сипаттай аламыз.

Жалпы біріктіргіш формулалардың маңызды класы болып табылады проективті формулалар: бұл формулалар A a-ны біріктіргіш бар болатындай етіп A осындай

${ displaystyle A vdash _ {L} B leftrightarrow sigma B}$

әрбір формула үшін B. Σ -ның mgu екенін ескеріңіз A. Транзитивті модальды және суперинтуициялық логикада ақырғы модель қасиеті (fmp), проективті формулаларды мағыналық тұрғыдан ақырғы жиынтығы ретінде сипаттауға болады L-модельдерде кеңейту қасиеті:^[19] егер М ақырлы Крипке L-түбірі бар модель р оның кластері а синглтон және формула A барлық нүктелерінде ұстайды М қоспағанда р, содан кейін айнымалылардың бағасын өзгертуге болады р жасау үшін A шын р сонымен қатар. Сонымен қатар, дәлелдеу проективті формула үшін mgu-дің нақты құрылысын ұсынады A.

Негізгі өтпелі логикада IPC, Қ4, S4, GL, Grz (және көбінесе фмп кез-келген өтпелі логикада, ақырлы раманың жиыны кеңейту қасиетінің басқа түрін қанағаттандырады), біз кез-келген формула үшін тиімді құра аламыз A оның проекциялық жақындату Π (A):^[20] проективті формулалардың ақырлы жиынтығы

1. ${ displaystyle P vdash _ {L} A}$ әрқайсысы үшін ${ displaystyle P in Pi (A),}$
2. әрбір біріктіруші A Π формуласын біріктіруші болып табыладыA).

Бұдан Π элементтерінің мг жиынтығы шығады (A) - бұл біріктіргіштердің толық жиынтығы A. Сонымен қатар, егер P проективті формула болып табылады

${ displaystyle P , | ! ! ! sim _ {L} B}$ егер және егер болса ${ displaystyle P vdash _ {L} B}$

кез-келген формула үшін B. Осылайша, біз рұқсат етілген ережелердің келесі тиімді сипаттамасын аламыз:^[21]

${ displaystyle A , | ! ! ! sim _ {L} B}$ егер және егер болса ${ displaystyle forall P in Pi (A) , (P vdash _ {L} B).}$

Рұқсат етілген ережелердің негіздері

Келіңіздер L логика бол. Жинақ R туралы L- рұқсат етілген ереже а деп аталады негіз^[22] егер рұқсат етілген ережелер болса, рұқсат етілген ережелер туралы Γ /B алынуы мүмкін R және туынды ережелері L, ауыстыруды, құрамын және әлсіреуін қолдана отырып. Басқа сөздермен айтқанда, R егер және ол болса ғана негіз болып табылады ${ displaystyle | ! ! ! sim _ {L}}$ қамтитын ең кіші құрылымдық салдарлық қатынас ${ displaystyle vdash _ {L}}$ және R.

Шешімді логиканың рұқсат етілген ережелерінің шешімділігі рекурсивті (немесе рекурсивті түрде санауға болады ) негіздер: бір жағынан, жиынтығы барлық рұқсат етілген ереже - егер рұқсатты шешуге болатын болса, рекурсивті негіз болып табылады. Екінші жағынан, рұқсат етілген ережелер жиынтығы әрқашан тең, мысалы, егер бізде бұдан әрі r.е. негізі, ол сонымен қатар, мысалы, шешімді болып табылады. (Басқаша айтқанда, біз рұқсат етілетінін шеше аламыз A/B келесі алгоритм: біз параллель екіден бастаймыз толық іздеулер, біреуін біріктіретін for ауыстыру үшін A бірақ жоқ B, ал біреуі туынды үшін A/B бастап R және ${ displaystyle vdash _ {L}}$. Іздеудің біреуі соңында жауап беруі керек.) Шешімділіктен басқа, кейбір қосымшалар үшін рұқсат етілетін ережелердің нақты негіздері пайдалы. жылы дәлелдеу күрделілігі.^[23]

Берілген логика үшін оның рекурсивті немесе жоқ екенін сұрай аламыз ақырлы рұқсат етілген ережелердің негізі және айқын негіздеме. Егер логиканың түпкілікті негізі болмаса, оның негізі болуы мүмкін тәуелсіз негіз: негіз R осылай дұрыс жиынтығы жоқ R негіз болып табылады.

Жалпы, қажетті қасиеттерге ие негіздердің болуы туралы өте аз нәрсе айтуға болады. Мысалы, while кестелік логика әдетте өзін-өзі жақсы ұстайды және әрдайым аксиоматизирленген, ережелердің ақырғы немесе тәуелсіз негіздері жоқ кестелік модальды логика бар.^[24] Шекті негіздер салыстырмалы түрде сирек кездеседі: тіпті негізгі өтпелі логика IPC, Қ4, S4, GL, Grz рұқсат етілген ережелердің шектеулі негіздері жоқ,^[25] олардың тәуелсіз негіздері болса да.^[26]

Негіздердің мысалдары

• Бос жиын - негізі L-жағдай ережелері және егер болса L құрылымдық жағынан аяқталған.
• Модальды логиканың барлық кеңеюі S4.3 (оның ішінде, атап айтқанда, S5) бірыңғай ережеден тұратын ақырлы негіз бар^[27]

${ displaystyle { frac { Diamond p land Diamond neg p} { bot}}.}$

• Виссер ережелері

${ displaystyle { frac { displaystyle { Bigl (} bigwedge _ {i = 1} ^ {n} (p_ {i} to q_ {i}) to p_ {n + 1} lor p_ { n + 2} { Bigr)} lor r} { displaystyle bigvee _ {j = 1} ^ {n + 2} { Bigl (} bigwedge _ {i = 1} ^ {n} (p_ { i} to q_ {i}) to p_ {j} { Bigr)} lor r}}, qquad n geq 1}$

ішіндегі рұқсат етілген ережелердің негізі болып табылады IPC немесе KC.^[28]

• Ережелер

${ displaystyle { frac { displaystyle Box { Bigl (} Box q to bigvee _ {i = 1} ^ {n} Box p_ {i} { Bigr)} lor Box r} { displaystyle bigvee _ {i = 1} ^ {n} Box (q land Box q to p_ {i}) lor r}}, qquad n geq 0}$

ережелерінің негізі болып табылады GL.^[29] (Бос дизъюнкция ретінде анықталғанын ескеріңіз ${ displaystyle bot}$.)

• Ережелер

${ displaystyle { frac { displaystyle Box { Bigl (} Box (q to Box q) to bigvee _ {i = 1} ^ {n} Box p_ {i} { Bigr) } lor Box r} { displaystyle bigvee _ {i = 1} ^ {n} Box ( Box q to p_ {i}) lor r}}, qquad n geq 0}$

ережелерінің негізі болып табылады S4 немесе Grz.^[30]

Рұқсат етілген ережелер семантикасы

Ереже Γ /B болып табылады жарамды модальды немесе интуитивті Kripke жақтауы ${ displaystyle F = langle W, R rangle}$, егер келесі бағалау әрбір бағалау үшін дұрыс болса ${ displaystyle Vdash}$ жылы F:

егер ${ displaystyle forall x in W , (x Vdash A)}$ барлығына ${ displaystyle A in Gamma}$, содан кейін ${ displaystyle forall x in W , (x Vdash B)}$.

(Анықтама оңай жалпылайды жалпы рамалар, қажет болса.)

Келіңіздер X ішкі бөлігі болуы керек W, және т нүкте W. Біз мұны айтамыз т болып табылады

• а рефлексиялық тығыз предшественник туралы X, егер әрқайсысы үшін болса ж жылы W: тырысу егер және егер болса т = ж немесе х = ж немесе x R y кейбіреулер үшін х жылы X,
• ан рефлексиялық қатаң предшественник туралы X, егер әрқайсысы үшін болса ж жылы W: тырысу егер және егер болса х = ж немесе x R y кейбіреулер үшін х жылы X.

Біз рамка деп айтамыз F рефлексивті (иррефлексивті) тығыз предшественниктері бар, егер әрқайсысы үшін болса ақырлы ішкі жиын X туралы W, рефлексивті (рефлексивті емес) тығыз предшественник бар X жылы W.

Бізде бар:^[31]

• ереже рұқсат етіледі IPC егер ол рефлексиялық қатаң предшественниктерге ие барлық интуитивті шеңберлерде жарамды болса ғана,
• ереже рұқсат етіледі Қ4 егер ол жалпыға бірдей жарамды болса ғана өтпелі рефлексиялық және рефлекторлы емес тығыз предшественниктер,
• ереже рұқсат етіледі S4 егер ол барлық өтпелі кезеңдерде жарамды болса ғана рефлексивті рефлексиялық тығыз предшественниктері бар кадрлар,
• ереже рұқсат етіледі GL егер ол тек барлық өтпелі жағдайда жарамды болса ғана негізделген рефлексиялық тығыз емес предшественники бар рамалар.

Біраз тривиальды жағдайлардан басқа, тығыз предшественники бар кадрлар шексіз болуы керек, сондықтан негізгі өтпелі логикада рұқсат етілген ережелер ақырғы модель қасиетіне ие болмайды.

Құрылымдық толықтығы

Құрылымдық тұрғыдан толық логиканың жалпы жіктелуі оңай мәселе болмаса да, біз кейбір ерекше жағдайларды жақсы түсінеміз.

Интуитивистік логиканың өзі құрылымдық жағынан толық емес, оның фрагменттер өзін басқаша ұстауы мүмкін. Атап айтқанда, суперинтуитивті логикада рұқсат етілген кез-келген дизьяксыз ереже немесе импликациясыз ереже туынды болып табылады.^[32] Екінші жағынан, Монеталар ережесі

${ displaystyle { frac {(p to q) to p lor r} {((p to q) to p) lor ((p to q) to r)}}}$

интуитивті логикада рұқсат етілген, бірақ туынды емес және тек салдарлары мен дизъюнкцияларын қамтиды.

Біз білеміз максималды құрылымдық жағынан толық емес өтпелі логика. Логика деп аталады тұқым қуалайтын құрылымдық жағынан толық, егер қандай да бір кеңейту құрылымдық жағынан аяқталған болса. Мысалы, классикалық логика, сонымен қатар логика LC және Grz.3 жоғарыда аталған, тұқым қуалайтын құрылымдық жағынан толық. Циткин мен Рыбаков тұқым қуалайтын құрылымдық жағынан толық суперинтуиционистік және өтпелі модальді логиканың толық сипаттамасын берді. Атап айтқанда, суперинтуициялық логика, егер ол Крипкенің бес фреймінің ешқайсысында жарамсыз болса ғана, тұқым қуалайтын түрде толық болады.^[9]

Сол сияқты, кеңейту Қ4 Крипкенің белгілі жиырма фреймінің кез-келгенінде жарамсыз болған жағдайда ғана (егер жоғарыдағы бес интуициялық фреймді қосқанда) тұқым қуалаушылық жағынан толық болып табылады.^[9]

Құрылымдық жағынан толық емес құрылымдық жағынан толық логика бар: мысалы, Медведевтің логикасы құрылымдық жағынан толық,^[33] бірақ ол құрылымдық жағынан толық емес логикаға енгізілген KC.

Нұсқалар

A параметрлері бар ереже форманың ережесі болып табылады

${ displaystyle { frac {A (p_ {1}, dots, p_ {n}, s_ {1}, dots, s_ {k})} {B (p_ {1}, dots, p_ {n }, s_ {1}, нүкте, s_ {k})}},}$

оның айнымалылары «тұрақты» айнымалыларға бөлінеді б_менжәне параметрлер с_мен. Ереже: L- егер әрқайсысы болса L-бөлгіш A осылай σс_мен = с_мен әрқайсысы үшін мен біріктіруші болып табылады B. Рұқсат етілетін ережелер бойынша шешімділіктің негізгі нәтижелері параметрлері бар ережелерге сәйкес келеді.^[34]

A көп қорытынды ережесі деп жазылған екі ақырлы формула жиынтығының жұбы (Γ, Δ) болып табылады

${ displaystyle { frac {A_ {1}, нүктелер, A_ {n}} {B_ {1}, нүктелер, B_ {m}}} qquad { text {or}} qquad A_ {1} , нүктелер, A_ {n} / B_ {1}, нүктелер, B_ {m}.}$

Егер Γ әрбір біріктіргіші Δ формуласын біріктіруші болса, мұндай ережеге жол беріледі.^[35] Мысалы, логика L болып табылады тұрақты егер ол ережені мойындайтын болса

${ displaystyle { frac {; bot ;} {}},}$

және суперинтуитивті логикада бар дизъюнкция қасиеті егер ол ережені мойындайтын болса

${ displaystyle { frac {p lor q} {p, q}}.}$

Тағы да, рұқсат етілген ережелер бойынша негізгі нәтижелер бірнеше тұжырымдамалық ережелерді біркелкі жалпылайды.^[36] Дизъюнкция қасиетінің нұсқасы бар логикада көп қорытынды ережелері бір қорытынды ережелер сияқты экспрессивтік күшке ие: мысалы, S4 жоғарыдағы ереже барабар

${ displaystyle { frac {A_ {1}, dots, A_ {n}} { Box B_ {1} lor dots lor Box B_ {m}}}.}$

Дәлелдерді жеңілдету үшін бірнеше тұжырым ережелерін жиі қолдануға болады.

Жылы дәлелдеу теориясы, рұқсат етілуі көбінесе контексте қарастырылады дәйекті кальций, мұндағы негізгі нысандар формулалардан гөрі секвенциялар. Мысалға, тілдің сөзін қайта өзгертуге болады элиминациялық теорема кескінсіз дәйекті есептеулер мойындайды деп айтқандай кесілген ереже

${ displaystyle { frac { Gamma vdash A, Delta qquad Pi, A vdash Lambda} { Gamma, Pi vdash Delta, Lambda}}.}$

(Тілді теріс пайдалану арқылы кейде (толық) дәйекті есептеу кесілген деп танылады, бұл оның кескінсіз нұсқасын білдіреді.) Алайда, тізбектелген калькуляциялардағы рұқсат, әдетте, сәйкес логикада рұқсаттың ескертілген нұсқасы болып табылады: кез келген (мысалы) интуитивтік логика үшін толық есептеу дәйекті ережені қабылдайды, егер ол қажет болса IPC әрбір тізбекті аудару арқылы алатын формула ережесін мойындайды ${ displaystyle Gamma vdash Delta}$ оның сипаттамалық формуласына ${ displaystyle bigwedge Gamma to bigvee Delta}$.

Ескертулер

Әдебиеттер тізімі

• В.Блок, Д.Пигозци, Алгебраланатын логика, Американдық математикалық қоғам туралы естеліктер 77 (1989), жоқ. 396, 1989 ж.
• А.Чагров және М. Захарящев, Модальды логика, Oxford Logic Guides т. 35, Оксфорд университетінің баспасы, 1997 ж. ISBN  0-19-853779-4
• П. Кинтула және Г. Меткалф, Бұлыңғыр логикадағы құрылымдық толықтығы, Notre Dame Journal of Formal Logic 50 (2009), жоқ. 2, 153-182 бб. дои:10.1215/00294527-2009-004
• Циткин А. Құрылымдық жағынан толық суперинтуициялық логика туралы, Кеңестік математика - Докладий, т. 19 (1978), 816–819 бб.
• С.Гиларди, Интуициялық логикадағы унификация, Symbolic Logic журналы 64 (1999), жоқ. 2, 859-880 бб. Евклид жобасы JSTOR
• С.Гиларди, Модальдық теңдеулерді жақсы шешу, Жылнамалар таза және қолданбалы логика 102 (2000), жоқ. 3, 183–198 бб. дои:10.1016 / S0168-0072 (99) 00032-9
• Р.Иемхоф, Интуициялық пропозициялық логиканың рұқсат етілген ережелері туралы, Symbolic Logic журналы 66 (2001), жоқ. 1, 281–294 б. Евклид жобасы JSTOR
• Р.Иемхоф, Аралық логика және Виссердің ережелері, Notre Dame Journal of Formal Logic 46 (2005), жоқ. 1, 65-81 б. дои:10.1305 / ndjfl / 1107220674
• Р.Иемхоф, Аралық логика ережелері туралы, Математикалық логикаға арналған мұрағат, 45 (2006), жоқ. 5, 581-599 бб. дои:10.1007 / s00153-006-0320-8
• Э. Джебек, Модальды логиканың рұқсат етілген ережелері, Логика және есептеу журналы 15 (2005), жоқ. 4, 411-431 бб. дои:10.1093 / logcom / exi029
• Э. Джебек, Рұқсат етілген ережелердің күрделілігі, Математикалық логикаға арналған мұрағат 46 (2007), жоқ. 2, 73-92 б. дои:10.1007 / s00153-006-0028-9
• Э. Джебек, Рұқсат етілген ережелердің тәуелсіз негіздері, IGPL 16 журналы (2008), жоқ. 3, 249-267 б. дои:10.1093 / jigpal / jzn004
• М. Крахт, Модальды салдарлық қатынастар, in: Modal Logic анықтамалығы (П.Блэкберн, Дж. ван Бентем және Ф. Волтер, ред.), Логика және практикалық пайымдауды зерттеу т. 3, Elsevier, 2007, 492-545 бб. ISBN  978-0-444-51690-9
• П.Лоренсен, «Logik und Mathematik» оперативті операциясында, Grundlehren der matemischen Wissenschaften т. 78, Спрингер-Верлаг, 1955.
• Г.Минц және А.Кожевников, Интуициялық Frege жүйелері көпмүшелік жағынан эквивалентті, Записки Научных Семинаров ПОМИ 316 (2004), 129–146 бб. gzipped PS
• Т. Прукнал, Медведевтің болжамдық есептеуінің құрылымдық толықтығы, Математикалық логика бойынша есептер 6 (1976), 103–105 бб.
• Т. Прукнал, Харви Фридманның екі мәселесі туралы, Studia Logica 38 (1979), жоқ. 3, 247–262 бет. дои:10.1007 / BF00405383
• Розьере, Rugles enquible propositionnel intuitionniste рұқсат етілген, Ph.D. тезис, Париж VII Университеті, 1992 ж. PDF
• В.В.Рыбаков, Логикалық қорытынды ережелерінің рұқсат етілуі, Логикадағы зерттеулер және математика негіздері т. 136, Эльзевье, 1997 ж. ISBN  0-444-89505-1
• Ф.Волтер, М. Захарящев, Модальды және сипаттама логикасы үшін біріздендіру және рұқсат ету проблемаларының шешілмеуі, ACM Transaction Computational Logic 9 (2008), жоқ. 4, мақала № 25. дои:10.1145/1380572.1380574 PDF