인정규정

논리적으로, 추론 규칙은 시스템의 기존 규칙에 추가되었을 때 시스템의 정리 집합이 변경되지 않으면 공식 시스템에서 인정된다.즉, 그 규칙을 이용하여 도출할 수 있는 모든 공식은 이미 그 규칙 없이 파생될 수 있기 때문에, 어떤 의미에서는 중복되는 것이다.인정된 규칙의 개념은 폴 로렌젠(1955)에 의해 도입되었다.

정의들

아드미시블은 우리가 다음으로 설명할 명제 비분류적 논리학에서 구조 규칙의 경우에만 체계적으로 연구되어 왔다.

기본 명제 커넥티브 세트를 고정시키십시오(예를 들어 초인전주의 로직의 경우$$$${ → ,${\displaystyle ,}$ ,${\displaystyle ,}$ ,${\displaystyle \mathrm{},}$ $,\land ,\lor ,\bot \}},$ 또는 단일 로직의 경우$$${\displaystyle }${${\displaystyle }$→ ,${\displaystyle \mathrm{\perp }}$ ,${\displaystyle }$⊥ , ${\displaystyle ◻\}}$ ${\displaysty \{\to ,\bot ,\Box \}).$명제 변수 p₀, p₁, ....의 무한한 집합에서 이러한 결합체를 사용하여 잘 형성된 공식들이 자유롭게 구축된다.치환 σ은 공식에서 연결부와 통용되는 공식까지 함수다.

${\displaystyle \sigma f(A_{1},\dots ,A_{n})=f(\sigma A_{1},\dots,\sigma A_{n}}}}$

모든 결합 f와 공식 A, ..., A에_1n 대하여. (우리는 공식의 γ에 대체물을 적용하여 σγ = {σA: A ∈}을(를) 만들 수도 있다.) 타르스키식 결과관계는^[1] 공식 집합과 공식 사이의 관계$$ $⊢{\displaystyle }$ ${\displaysty \vdash }$이다.

모든 공식 A, B 및 공식 집합 γ, Δ. 다음과 같은 결과 관계

모든 대체품을 구조라고 부른다.(여기서 그리고 아래에 사용된 "구조적"이라는 용어는 연속적인 캘커리에서의 구조 규칙의 개념과 무관하다는 점에 유의한다.)구조적 결과 관계를 명제 논리라고 한다.공식 A는 논리 $⊢{\displaystyle }$ ${\displaystyle \vdash }$의 정리인데, 만일 ${\displaystyle \varnothing }$ ${\displaystyle A}$ {\$displaystyle \varnoth \vdash A}$이$($가) 있다면$.$

예를 들어, 우리는 표준 결과 관계 $\{{\displaystyle {}_{}}$ ${\displaystyle L_{}}$ ${\$를 모더스 폰과 공리로 공리화할$$ 수 있는 초직관적 논리 L을 식별하고, ${\displaystyle {글로벌}_{}}$ 결과 관계 $⊢{\displaystyle {}_{}}$ L ${\$모듈 폰, 필요성 및 액시오에 의해 공리모달$$ 논리를 식별한다.Ms.

구조 추론 규칙^[2](또는 간단히 말해서 규칙)은 보통 다음과 같이 쓰여진 쌍( (,B)에 의해 주어진다.

${\displaystyle {\frac {A_{1},\dots, A_{n}}}{B}}}\cext{or}}\text{or}}}\qquad A_{1},\dots,A_{n}/B,}$

여기서 γ = {A₁, ..., A_n}은 유한한 공식 집합이고, B는 공식이다.그 규칙의 예는 다음과 같다.

${\displaystyle \sigma A_{1},\dots,\sigma A_{n}/\sigma B}$

대체용 σ규칙 γ/B는 $⊢{\displaystyle }$ ${\displaystyle \vdash$ $\},$ ${\displaystyle \gamma }$ ${\displaystyle ⊢}$B {\$displaystyle \Gamma \vdash$ B$}$에서 파생될 수 있다. 규칙의 모든 예에 대해 formulasB는 σ의 모든 공식들이 정리일 때마다 인정된다$.$^[3]즉, 논리에 추가되었을 때 새로운 이론으로 이어지지 않는다면 규칙은 인정된다.^[4]또한${\displaystyle }write{\displaystyle \mathrm{}}$ ~ ${\displaystyle B}$ ${\displaystyle \감마$ \,$\!\!$라고 쓴다.$\!\sim B}$ if/B가 허용될 경우$$. (참고: ${\displaystyle ~}$ ${\displaystyle \!\!)$$\!\sim }$은(는) 그 자체로 구조적인 결과 관계다.)

모든 파생 가능한 규칙은 허용되지만, 일반적으로 그 반대는 아니다.허용되는 모든 규칙이 파생될 수 있는 경우, 즉 ${\displaystyle =}$ =${\displaystyle }$~$${\$displaystyle${\$vdash }={\,$\!\!) 로직은 구조적으로 완전하다.$\!\심$ $\}\}.$^[5]

In logics with a well-behaved conjunction connective (such as superintuitionistic or modal logics), a rule ${\displaystyle A_{1},\dots ,A_{n}/B}$ is equivalent to ${\displaystyle A_{1}\land \dots \land A_{n}/B}$ with respect to admissibility and derivability.따라서 단규 A/B만 다루는 것이 관례다.

예

• 고전 명제 미적분학(CPC)은 구조적으로 완전하다.^[6]Indeed, assume that A/B is non-derivable rule, and fix an assignment v such that v(A) = 1, and v(B) = 0. Define a substitution σ such that for every variable p, σp = ${\displaystyle \top }$ if v(p) = 1, and σp = ${\displaystyle \bot }$ if v(p) = 0. Then σA is a theorem, but σB is not (in fact, ¬σB is a theorem).따라서 규칙 A/B도 허용되지 않는다. (모든 요소가 L 언어로 이름을 갖는 논리 행렬에 관하여 완전한 다중값 논리 L에도 동일한 인수가 적용된다.)
• 더 크라이젤-푸트남 법칙(.K.A.하롭의 규칙 또는 전제 규칙의 독립성)

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

직관적 명제 미적분학(IPC)에서 인정된다.사실, 그것은 모든 초직관주의 논리에 허용된다.^[7]반면에 공식은

$(\neg p\to q\lor r)\to (\neg p\to q)\lor (\neg p\to r)}}$

KPR은 IPC에서 파생될 수 없는 직관적인 상호작용이 아니다.특히 IPC는 구조적으로 완전하지 않다.

• 규칙

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

K, D, K4, S4, GL과 같은 많은 모달 로직에서 허용된다(모달 로직 이름은 이 표 참조).S4에서는 파생할 수 있지만 K, D, K4, GL에서는 파생할 수 없다.

• 규칙

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

모든 일반적인 모달 논리에 허용된다.^[8]GL과 S4.1에서는 파생할 수 있지만 K, D, K4, S4, S5에서는 파생할 수 없다.

• 뢰브 법칙

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

기본 모달 논리 K에서는 허용되지만, GL에서는 허용된다.그러나 LR은 K4에서 인정되지 않는다.특히, 논리 L에서 인정될 수 있는 규칙이 그 연장선상에서 인정되어야 한다는 것은 일반적으로 사실이 아니다.

• 괴델-덤메트 논리(LC)와 모달 논리 Grz.3은 구조적으로 완전하다.^[9]제품 퍼지 논리도 구조적으로 완전하다.^[10]

결정성 및 규칙 감소

주어진 논리의 허용 규칙에 대한 기본적인 질문은 허용 가능한 모든 규칙 집합을 해독할 수 있는가 하는 것이다.논리 자체(즉, 그것의 이론 집합)가 결정 가능하더라도 문제는 중요하지 않다는 점에 유의하십시오. 규칙 A/B의 자격의 정의는 모든 명제적 대체에 대해 무한 범용 계량자를 포함하므로, 그 이전부터 우리는 결정 가능 논리에서의 규칙 능력이 ${\displaystyle {\mathrm{}}_{}^{}}$ 1 0 ${\$이라는 것만 알고 있다.$}}^{0}}($즉, 그 보완이 재귀적으로 열거됨).예를 들어, 2모달 로직_u K와 K4_u(범용 모달리티를 가진 K 또는 K4의 확장자)에서는 불가해한 것으로 알려져 있다.^[11]주목할 만한 것은 기본적인 모달로직 K에서 기능성의 결정성이 중요한 개방성 문제라는 점이다.

그럼에도 불구하고, 규칙의 능력은 많은 모달과 초직관적 논리학에서 해독할 수 있는 것으로 알려져 있다.기본 전이적 모달 로직에서 허용 가능한 규칙에 대한 첫 번째 결정 절차는 Rybakov에 의해 축소된 규칙 형식을 사용하여 구성되었다.^[12]변수 p₀, ..., p의_k 모달 규칙을 형태가 있으면 축소라고 한다.

${\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}}},}$

여기서 각 $\neg {\displaystyle {\mathrm{}}_{}^{}}$ ${\displaystyle i_{}^{}}$, ${\displaystyle j_{}^{}}$ ${\displaystyle {}_{}^{}}$ ${\$ $\$$neg _{i,j}^{u}}}$은(는) 공백이거나 부정$display$ {\displaystyle \$neg}$이다$.$ 각 규칙 r에 대해, 모든 논리가 모든 s를 승인(또는 파생)하는 경우에만 r을 허용(또는 파생)하도록 축소된 규칙 s를 효과적으로 구성할 수 있다.ubformula를 A로 하고 그 결과를 완전한 분리 정상 형태로 표현한다.따라서 축소된 규칙의 수용성을 위한 의사결정 알고리즘을 구축하는 것으로 충분하다.

$\bigvee {\displaystyle \underset{}{\overset{}{}}}$ ${\displaystyle \underset{}{\overset{}{i}}}$= ${\displaystyle \underset{}{\overset{}{0}}}$ n ${\displaystyle {\phi }_{}}$ i${\displaystyle {}_{}}$/ ${\displaystyle {p\mathrm{}}_{}}$ ${\displaystyle 0{}_{}}$ ${\$을(를) 위와 같이 축소된 규칙이 되도록$$ 한다.We identify every conjunction ${\displaystyle \varphi _{i}}$ with the set ${\displaystyle \{\neg _{i,j}^{0}p_{j},\neg _{i,j}^{1}\Box p_{j}\mid j\leq k\}}$ of its conjuncts.For any subset W of the set ${\displaystyle \{\varphi _{i}\mid i\leq n\}}$ of all conjunctions, let us define a Kripke model ${\displaystyle M=\langle W,R,{\Vdash }\rangle }$ by

$\displaystyle \varphi _{i}\vdash p_{j}\iff p_{j}\in \varphi _{i}}}$

$\\displaystyle \varphi _{i}\,R\,\varphi _\forall j\leq k\,(\Box p_{j}\in \varphi \{p_{j},\Box p_{j}\subsete \varpi _{varphi_{varphi_}}$

그 다음 사항은 K4의 수용성에 대한 알고리즘 기준을 제공한다.^[13]

정리.The rule ${\displaystyle \textstyle \bigvee _{i=0}^{n}\varphi _{i}/p_{0}}$ is not admissible in K4 if and only if there exists a set ${\displaystyle W\subseteq \{\varphi _{i}\mid i\leq n\}}$ such that

1. ${\displaystyle {\phi }_{}}$ ${\displaystyle i_{}}$ ${\displaystyle {}_{}}$ ${\displaystyle {}_{}}$ ${\displaystyle {0\mathrm{}}_{}}$ ${\$ 일부$$ $i{\displaystyle }$ ${\displaystyle \le n,}$ ${\displaysty$ i\$leq n,}$
2. ${\displaystyle {\phi }_{}}$ ${\displaystyle i_{}}$ ${\displaystyle {}_{}}$ ${\displaystyle i_{}}$ ${\$ 매$$ $i{\displaystyle }$ ${\displaystyle \le n,}$ ${\displaystyle i\leq n,}$
3. W의 모든 부분 집합 D에 $대해{\displaystyle }$ α ,${\displaystyle \beta }$ ${\displaystyle \in }$ W ${\displaystyle \alpha ,\beta \in W}$ 등가성분들이 존재한다$$.

${\displaystyle \alpha }$ ${\displaystyle ⊩}$ p ${\displaystyle j_{}}$ ${\$만 $if{\displaystyle }$${\displaystyle p_{}}$ ${\$인 경우에만 ${\displaystyle d}$D$${\$displaystysty \varphi \in$D}

${\displaystyle \alpha \Vdash \Box p_{j}}$ if and only if ${\displaystyle \alpha \Vdash p_{j}}$ and ${\displaystyle \varphi \Vdash p_{j}\land \Box p_{j}}$ for every ${\displaystyle \varphi \in D}$

모든 J를 지지하다

로직 S4, GL 및 Grz에 대해서도 유사한 기준을 찾을 수 있다.^[14]또한 Gödel-McKinsey-Tarski 번역기를 사용하여 Grz에서 직관 논리의 능력을 수용성으로 줄일 수 있다.^[15]

${\displaystyle$$\!\sim _{IPC}$$B$가$$T (${\displaystyle A}$)${\displaystyle {}_{}}$~ ${\displaystyle G_{}}$ ${\displaystyle r_{}}$ ${\displaystyle {}_{}}$( ${\displaystyle B}$ )${\displaystyle }$.${\displaystyle$ T$(A)\, \!\!$$\!\sim _{Grz}T(B).$$}$

Rybakov (1997) developed much more sophisticated techniques for showing decidability of admissibility, which apply to a robust (infinite) class of transitive (i.e., extending K4 or IPC) modal and superintuitionistic logics, including e.g. S4.1, S4.2, S4.3, KC, T_k (as well as the above-mentioned logics IPC, K4, S4, GL, Grz).^[16]

디커피블이 가능함에도 불구하고, 능력 문제는 단순한 로직에서도 계산 복잡성이 상대적으로 높다: 기본 전이 로직 IPC, K4, S4, GL, Grz는 cNExP-완전이다.^[17]이는 PSPACE-완전한 로직의 유도성 문제(규칙이나 공식의 경우)와 대조되어야 한다.^[18]

프로젝트성과 통일성

명제 로직의 능력은 모달 또는 헤이팅 알헤브라의 등가 이론에서 통일과 밀접한 관련이 있다.그 연결은 길라르디(1999, 2000)에 의해 개발되었다.In the logical setup, a unifier of a formula A in a logic L (an L-unifier for short) is a substitution σ such that σA is a theorem of L. (Using this notion, we can rephrase admissibility of a rule A/B in L as "every L-unifier of A is an L-unifier of B".) An L-unifier σ is less general than an L-unifier τ, written as σ ≤ τ, if there exists a substi그런 식으로 말하다.

$\displaystyle \vdash _{L}\sigma p\왼쪽 오른쪽 화살표 \upsilon \tau p}$

모든 변수 p에 대해공식 A의 전체 고유자 집합은 A의 모든 L-유니퍼가 S의 일부 고유자보다 덜 일반적이도록 A의 L-유니어의 집합 S이다.A의 가장 일반적인 단일자(mgu)는 단일자 σ이며, {σ}은(는) A의 완전한 단일자 집합이다.S가 A의 완전한 단일자 집합인 경우, 규칙 A/B는 S의 모든 σ이 B의 L-unifier인 경우에만 허용된다.따라서 우리가 예의 바르게 행동한 완전한 단수들을 찾을 수 있다면 허용 가능한 규칙들을 특징 지을 수 있다.

가장 일반적인 단일자를 갖는 중요한 종류의 공식은 투영식이다: 이것들은 A의 단일자 σ이 존재하는 공식이다.

${\displaystyle A\vdash _{L}B\왼쪽 오른쪽 화살표 \sigma B}$

모든 공식 B에 대해σ은 A의 mgu라는 점에 유의한다.타동사의 조동사와의 한정된 모델 속성(fmp)과superintuitionistic 논리에서 의미론적으로 근 플레이어와 한정되어 L-models의 집합을 확장 속성을로:사영 공식의 특성을 보여 줄 수 있[19]만약 M가 유한한 Kripke L-model의 클러스터는 singleton이 뿌리 r과 함께 했으며, 공식 A의 Mr을 제외하고 모든 점에서, 그리고 보유하고 있다.우리가r에서 변수의 가치평가를 변경하여 a를 r에서도 진실되게 할 수 있다.더욱이, 그 증거는 주어진 투영 공식 A에 대한 mgu의 명시적인 구성을 제공한다.

기본 전이 로직 IPC, K4, S4, GL, Grz(그리고 더 일반적으로 유한 프레임 세트가 다른 종류의 확장 특성을 만족하는 fmp를 가진 어떤 전이적 논리에서도, 우리는 A 공식의 투사적 근사치 ((A):^[20] 다음과 같은 유한한 투사 공식 집합을 효과적으로 구성할 수 있다.

1. ${\displaystyle P}$ ${\displaystyle {}_{}}$ L ${\displaystyle {}_{}}$ ${\displaystyle P\vdash _{L}모든$ $P{\displaystyle }$ ${\displaystyle \in }$ ${\displaystyle \pi }$( A${\displaystyle }$)${\displaystyle }$, ${\displaystyle$ P$\in \Pi (A),}$
2. A의 모든 단수는 π(A)의 공식을 단일한 것이다.

π(A) 원소의 mgus 집합이 A의 완전한 단수 집합이라는 것에 따른다.더욱이 P가 투영식이라면, 그 다음이다.

${\displaystyle$$\!\sim _{L}$$B$가 P ${\displaystyle {}_{}}$ ${\displaystyle {}_{}}$ B ${\displaystyle P\vdash _{L}B$인 경우에만$$ 해당됨

모든 공식 B에 대해.따라서 허용 가능한 규칙의 다음과 같은 효과적인 특성을 얻는다.^[21]

${\displaystyle$$\backslash !\backslash {\displaystyle \mathrm{}}$$sim _{L}B$가 ${\displaystyle \mathrm{if}}$ ${\displaystyle \in }$ ( ${\displaystyle \mathrm{A}}$) ($($ ${\displaystyle L{}_B}$ ) .${\displaystyle }${\$displaystyle \forall P\in \Pi (A)\,$ (P$\vdash _{L}B)$인 경우에만 해당.$}$

인정된 규칙

L을 논리로 삼자.허용되는 모든 규칙 Ⅱ/B가 R과 L의 파생 가능한 규칙에서 도출될 수 있다면 대체, 구성 및 약화를 사용하여 L-admit 규칙의 집합 R을 허용 가능한 규칙의^[22] 기초로 부른다.${\displaystyle {즉}_{},{}_{}}$ R은 ~ L ${\$의 경우에만 기초가 된다.$\!\sim _{L}$은(는) $⊢{\displaystyle {}_{}}$ ${\displaystyle L_{}}$ ${\$과(와) R을 포함하는 가장 작은 구조적 결과 관계다$$.

결정 가능한 논리의 허용 가능한 규칙의 결정성은 재귀적(또는 재귀적으로 열거된) 근거의 존재와 동등하다는 점에 유의하십시오. 한편으로, 허용 가능한 모든 규칙의 집합은 수용가능성이 결정 가능한 경우 재귀적 기준이다.반면, 허용 가능한 규칙의 집합은 항상 동일하며, 만약 우리가 더 많은 기준(re.e.based)을 가지고 있다면, 그것 또한 r. 즉, decificable이 가능하다.(다시 말해, A/B의 능력을 다음 알고리즘에 의해 결정할 수 있다: A를 통합하지만 B는 아닌 대체 σ에 대해, 그리고 R과 $⊢ L에서 A/$를 도출하는 것에 대해 두 가지 알고리즘을 병행하여 시작할 수 있다$.$ 한 가지 검색은 결국 답을 도출해야 한다.)결정성 외에도, 허용 가능한 규칙의 명시적 근거는 예를 들어 입증 복잡성 등에 있어 일부 적용에 유용하다.^[23]

주어진 논리에 대해서는 그것이 허용 가능한 규칙의 재귀적 또는 유한적 근거를 가지고 있는지 묻고, 명시적 근거를 제시할 수 있다.어떤 논리에 유한한 기초가 없다면, 그럼에도 불구하고 그것은 독립적인 기초 즉, R의 적절한 부분집합이 기초가 되지 않는 기초 R을 가질 수 있다.

일반적으로 바람직한 성질을 가진 기지의 존재에 대해서는 거의 말할 수 없다.예를 들어, 표 로직은 일반적으로 잘 행동하며 항상 정밀하게 공리화할 수 있는 반면, 규칙의 유한하거나 독립적인 기초가 없는 표 형식 로직은 것이다.^[24]유한 베이스는 상대적으로 드물다. 기본 전이 로직 IPC, K4, S4, GL, Grz도 독립 베이스를 가지고 ^[25]있지만 허용 가능한 규칙의 유한 기반을 가지고 있지 않다.^[26]

베이스의 예

• 빈 집합은 L이 구조적으로 완전한 경우에만 L-admacle 규칙의 기초가 된다.
• 모달 논리 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}{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]참고: 빈 구분은 $\perp {\displaystyle \mathrm{}}$ ${\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는 F의 모든 평가 $⊩{\displaystyle }$ ${\displaystyle \Vdash }$에 대해 다음이 참인 경우 모달 ${\displaystyle \mathrm{또는}}$ 직관적인 Kripke $프레임{\displaystyle }$ F${\displaystyle }$= ${\displaystyle ⟨}$ W${\displaystyle }$, ${\displaystyle R}$ ${\displaystyle ⟩}$ ${\displaystyle F=\langle W,R\randle$ $\}$에서 유효하다.

if ${\displaystyle \forall x\in W\,(x\Vdash A)}$ for all ${\displaystyle A\in \Gamma }$, then ${\displaystyle \forall x\in W\,(x\Vdash B)}$.

(이 정의는 필요한 경우 일반 프레임으로 쉽게 일반화된다.)

X를 W의 하위 집합으로 하고, T를 W의 점으로 한다.우리는 t라고 말한다.

• X의 반사적으로 엄격한 전신, 만약 모든 Y에 대해 W: t R y의 경우 t = y 또는 x = y 또는 X의 일부 X의 경우 x R y인 경우에만,
• X의 일부 X에 대해 x = y 또는 x R y인 경우에만 W: t R y의 모든 y에 대해 X의 회복 불가능할 정도로 엄격한 이전 버전

우리는 프레임 F가 반사성(비유연성) 엄격한 선행자를 가지고 있다고 말한다. 만약 W의 모든 유한 부분 집합 X에 대해, W에 X의 반사성(비유연성) 엄격한 선행자가 존재한다면.

다음이 있음:^[31]

• IPC에서 규칙은 반사적으로 엄격한 전임자를 가진 모든 직감적 틀에서 유효할 경우에만 허용된다.
• K4에서 규칙은 반사적이고 회복 불가능한 엄격한 전임자를 가진 모든 전이적 프레임에서 유효한 경우에만 허용된다.
• 규칙은 반사적으로 빡빡한 전임자를 가진 모든 전이적 반사 프레임에서 유효하다면 S4에서 허용된다.
• GL에서는 회복할 수 없는 엄격한 이전 버전을 가진 모든 타동성 컨버스 근거가 충분한 프레임에서 유효한 경우에만 규칙이 허용된다.

사소한 몇 가지 경우를 제외하고, 엄격한 선행 조건이 있는 프레임은 무한해야 하므로 기본 전이 로직에서 허용 가능한 규칙은 유한 모델 특성을 누리지 못한다.

구조완전성

구조적으로 완전한 논리학의 일반적인 분류는 쉬운 일은 아니지만, 우리는 몇몇 특별한 경우를 잘 이해하고 있다.

직관적 논리 자체는 구조적으로 완전하지는 않지만, 그 단편들은 다르게 행동할 수도 있다.즉, 초인체적 논리에서 허용될 수 있는 모든 분리-자유 규칙 또는 함축-자유 규칙은 파생될 수 있다.^[32]반면에 민츠가 통치한다.

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

직관적 논리에서는 인정되지만 파생될 수 없으며, 함축적 의미와 분리만을 포함한다.

우리는 구조적으로 불완전한 전이 로직의 최대치를 알고 있다.어떤 연장이 구조적으로 완전하다면 어떤 논리는 유전적으로 완전하다고 불린다.예를 들어 위에서 언급한 로직 LC와 Grz.3은 물론 고전적 논리도 유전적으로 구조적으로 완전하다.구조적으로 완전한 초직전주의와 전이적 모달 로직의 완전한 설명은 씨트킨과 라이바코프에 의해 각각 주어졌다.즉 초인체적 논리는 다섯 개의 크립케 틀^[9] 중 어느 하나에도 유효하지 않은 경우에만 유전적으로 완전하다.

마찬가지로 K4의 연장은 특정한 20개의 Kripke 프레임 중 하나(위의 다섯 개의 직관적 프레임을 포함)에서 유효하지 않은 경우에만 유전적으로 완전하다.^[9]

유전적으로 완전하지 않은 구조적으로 완전한 로직들이 존재한다. 예를 들어 메드베데프의 논리는 구조적으로 완전하지만 ^[33]구조적으로 불완전한 논리 KC에 포함된다.

변형

매개변수가 있는 규칙은 양식의 규칙이다.

${\displaystyle {\frac {A(p_{1},\dots ,p_{n},\dots,s_{k}}}{B(p_{1},\dots,p_{n},s_{1},}},},},}$

이 변수들은 "정규_i" 변수 p와_i 매개변수 s로 나뉜다.각 i에 대해 uns_i = s가_i 또한 B의 단수일 경우 A의 모든 L-unifier σ가 L-admit이면 규칙은 L-admit이 허용된다.허용 가능한 규칙에 대한 기본 결정성 결과는 매개변수가 있는 규칙에도 적용된다.^[34]

다중 결합 규칙은 두 개의 유한한 공식 집합의 쌍(Δ, Δ)으로, 다음과 같이 기록된다.

${\displaystyle {\frac {A_{1},\dots,A_{n}}{B_{1},\dots,B_{m}},\dots,B_{n},\dots,B_{n}/{m},\dots,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 \lor \Box B_{m}}}.}$

그럼에도 불구하고 다중 컨버전스 규칙은 종종 논쟁을 단순화하기 위해 채택될 수 있다.

증명 이론에서 수용성은 종종 수식이 아닌 염기서열인 석회암이라는 맥락에서 고려된다.예를 들어, 절삭-제거 정리는 절삭-절삭-절삭 미적분학이 절삭규칙을 인정한다는 말로 바꾸어 말할 수 있다.

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

(언어의 남용에 의해서, 때로는 (완전한) 속편 미적분학이 절단을 인정한다고도 하는데, 이는 절단이 없는 버전이 절단을 인정하는 것을 의미한다.)그러나, 시퀀스 미적분학의 능력은 해당 논리에서의 능력을 위한 공칭적 변종일 뿐이다: (예:) 직관적 논리에 대한 완전한 미적분학은 IPC가 각 시퀀스 $\delta {\displaystyle \mathrm{}\mathrm{\Delta }}$ ${\displaystyle \감마 \vdash \Delta }$을(으)로$$ 변환하여 얻은 공식 규칙을 승인하는 경우에만 시퀀스 규칙을 인정한다.${\displaystyle \mathrm{racteristic}}$ 공식 $\bigwedge {\displaystyle }$ ${\displaystyle \bigvee }$→$$ {\$displaystyle \bigwedge \Gamma \to \bigvee \Delta$ $\}.$

메모들

참조

• W. Blok, D.피고찌, 대수학 가능 논리학, 미국 수학 학회 77호(1989), 제396호, 1989.
• A. Chagrov와 M. Zakaryaschev, Modal Logic, Oxford Logic Guides vol. 35, Oxford University Press, 1997. ISBN0-19-853779-4
• P. Cintula와 G.Metcalfe, 퍼지 로직에서의 구조적 완전성, 노틀담 저널 of Formal Logic 50 (2009), 2, 페이지 153–182. doi:10.1215/00294527-2009-004
• A. I. Citkin, 구조적으로 완전한 초직관주의 논리학에서, 소련 수학 - Doklady, 제 19권 (1978), 페이지 816–819.
• S. 길라르디, 직관논리의 통일, 기호논리의 저널 64 (1999), 제 2, 페이지 859–880.프로젝트 유클리드 JSTOR
• S. 길라르디, 최고의 해결 방법 방정식, 순수와 응용 논리 102(2000), 3, 페이지 183–198. doi:10.1016/S0168-0072(99)00032-9
• R. Iemhoff, 직관론적 명제논리의 인정된 규칙에 대하여, Journal of Symbolic Logic 66(2001), 제1호, 페이지 281–294.프로젝트 유클리드 JSTOR
• R. Iemhoff, 중간 로직 및 비서의 규칙, 형식 논리 46의 노트르담 저널(2005), 1번 페이지 65–81. doi:10.1305/ndjfl/1107220674
• R. Iemhoff, 중간 로직의 규칙에 대하여, 수학 논리 아카이브 45 (2006), 5, 페이지 581–599. doi:10.1007/s00153-006-0320-8
• E. 제아벡, 모달 로직의 허용 규칙, 로직 및 계산 저널 15(2005), 4, 페이지 411–431. doi:10.1093/logcom/exi029
• E. 제아벡, 인정된 규칙의 복잡성, 수학 논리 46(2007), 제 2, 페이지 73–92. doi:10.1007/s00153-006-0028-9
• E. 제아벡, 인정된 규칙에 대한 독립적 근거, IGPL 16(2008), 3, 페이지 249–267. doi:10.1093/jigpal/jzn004
• M. Kracht, Modal Rescue Relations in: Modal Logic의 핸드북(P. Blackburn, J. van Benthem, F)Wolter, eds.), 논리 및 실제 추론에 관한 연구 vol. 3, Exvier, 2007, 페이지 492–545.ISBN 978-0-444-51690-9
• P. 로렌젠, Einführung in die operative Logik und Mathik, Grundlehren deramatischen Wissenschaften vol. 78, Springer–Verlag, 1955.
• G. 민츠와 A.Kojevnikov, 직관적 Frege 시스템은 다항적으로 동등하며, Zapiski Nauchnyh Seminaov POMI 316(2004), 페이지 129–146. gziped PS.
• T. 프루크날, 메드베데프의 명제 미적분의 구조적 완전성, 수학 논리 6(1976), 페이지 103–105.
• T. Prucnal, 하비 프리드먼의 두 가지 문제, Studia Logica 38 (1979), 3, 페이지 247–262. doi:10.1007/BF00405383
• P. Roziér, Régles addicles in calcul propositionniste, 박사 논문, Université de Paris VII, 1992.PDF
• V. V. Rybakov, 논리적 추론 규칙의 수용성, 논리와 수학의 기초에 관한 연구 vol. 136, 엘스비에, 1997.ISBN 0-444-89505-1
• F. Wolter, M. Zakaryaschev, 모달 및 설명 로직의 통일 불해독성 및 능력 문제, ACM Transactions on Computing Logic 9(2008), 제4호, 제25조 doi:10.1145/1380572.1380574 PDF