2025-11-21T13:49:15.584467

Twist Sequent Calculi for S4 and its Neighbors

Kamide

Two Gentzen-style twist sequent calculi for the normal modal logic S4 are introduced and investigated. The proposed calculi, which do not employ the standard logical inference rules for the negation connective, are characterized by several twist logical inference rules for negated logical connectives. Using these calculi, short proofs can be generated for provable negated modal formulas that contain numerous negation connectives. The cut-elimination theorems for the calculi are proved, and the subformula properties for the calculi are also obtained. Additionally, Gentzen-style twist (hyper)sequent calculi for other normal modal logics including S5 are considered.

academic

S4 및 관련 논리를 위한 트위스트 시퀀트 계산법

기본 정보

논문 ID: 2501.00483
제목: Twist Sequent Calculi for S4 and its Neighbors
저자: Norihiro Kamide (나고야시립대학교 데이터과학부, 일본 아이치현)
분류: cs.LO (컴퓨터과학의 논리)
발표 학회: Non-Classical Logics: Theory and Applications (NCL'24), EPTCS 415, 2024
논문 링크: https://arxiv.org/abs/2501.00483

초록

본 논문은 정규 양상 논리 S4를 위한 겐첸 스타일의 트위스트 시퀀트 계산법(twist sequent calculi) 두 가지를 제안하고 연구한다. 제안된 계산 체계는 부정 연결사에 대한 표준 논리 추론 규칙을 사용하지 않으며, 대신 부정 논리 연결사에 대한 트위스트 논리 추론 규칙을 채택한다. 이러한 계산 체계를 사용하면 많은 부정 연결사를 포함하는 증명 가능한 부정 양상 공식에 대해 간단한 증명을 생성할 수 있다. 본 논문은 이러한 계산법의 절 제거 정리를 증명하고 부분공식 성질을 얻었다. 또한 S5를 포함한 다른 정규 양상 논리에 대한 겐첸 스타일의 트위스트 (초)시퀀트 계산법을 고려했다.

연구 배경 및 동기

문제 정의

본 연구가 해결하고자 하는 핵심 문제는 다음과 같다: 많은 부정 연결사를 포함하는 양상 공식에 대해 효과적이고 간결한 증명 체계를 어떻게 제공할 것인가? 전통적인 겐첸 스타일 시퀀트 계산법은 여러 부정을 포함하는 양상 공식을 처리할 때 장황한 증명을 생성한다.

연구의 중요성

철학 논리의 의의: 부정 정보 또는 지식의 추론, 특히 부정과 양상을 포함하는 추론은 철학 논리 분야에서 중요한 의미를 가지며, 피치 역설의 분석 등에 적용된다.
컴퓨터과학 응용: 논리 프로그래밍과 지식 표현에서 양상과 부정을 포함하는 추론이 필수적이다.
증명 효율성: 실제 세계에서 참인 부정 정보는 일반적으로 양상 연산자와 여러 부정 연결사를 포함하는 증명 가능한 부정 양상 공식으로 표현되며, 증거로서 간결한 증명이 필요하다.

기존 방법의 한계

오니시-마츠모토 체계: 절 제거 가능하고 분석적이지만, 많은 부정 연결사를 포함하는 부정 양상 공식의 증명에서 비효율적이다.
크립키의 GS4 체계: 마찬가지로 장황한 증명의 문제가 있다.
기타 확장 체계(NS4, DS4, SS4, GS41-GS43): 특정 추론 유형에 적용 가능하지만 분석성이 부족하거나 부정 양상 공식 처리 시 효율이 낮다.

핵심 기여

두 가지 트위스트 시퀀트 계산법 제안: lTS4(국소 트위스트)와 gTS4(전역 트위스트)는 모두 절 제거 가능하고 분석적이다.
증명 이론 결과: 절 제거 정리와 부분공식 성질을 확립했다.
효율성 향상: 많은 부정 연결사를 포함하는 양상 공식에 대해 현저히 짧은 증명을 제공한다.
다른 양상 논리로의 확장: K, KT, S5 등 다른 정규 양상 논리에 대한 해당 트위스트 계산법을 구성했다.
이론적 동치성: lTS4, gTS4와 표준 GS4 체계의 정리 동치성을 증명했다.

방법론 상세 설명

작업 정의

정규 양상 논리 S4에서 많은 부정 연결사를 포함하는 공식에 대해 간결한 증명을 제공할 수 있는 겐첸 스타일의 시퀀트 계산 체계를 구축한다. 입력은 양상 공식이고, 출력은 해당 공식의 증명(증명 가능한 경우)이다.

모델 구조

lTS4 (국소 트위스트 시퀀트 계산법)

초기 시퀀트:

표준: p ⇒ p (모든 명제 변수 p에 대해)
부정: ¬p ⇒ ¬p, ¬p, p ⇒, ⇒ ¬p, p

구조 추론 규칙:

절 규칙: (Γ ⇒ α)(α, Γ ⇒ Δ) / (Γ ⇒ Δ)
약화 규칙: 좌측 약화 및 우측 약화

비트위스트 논리 추론 규칙:

표준 ∧, ∨, → 규칙
양상 규칙: (□left), (□right), (◊left), (◊right)

트위스트 논리 추론 규칙: 핵심 혁신은 트위스트 규칙에 있으며, 예를 들어:

(¬□leftₜ): (Γ₁, ¬◊Γ₂ ⇒ ◊Δ₁, ¬□Δ₂, α) / (¬□α, Γ₁, ¬◊Γ₂ ⇒ ◊Δ₁, ¬□Δ₂)

gTS4 (전역 트위스트 시퀀트 계산법)

gTS4는 lTS4의 특정 규칙을 전역 트위스트 규칙으로 대체하여 얻어진다:

(¬□leftₜ): (Γ₁, Δ₂ ⇒ ◊Δ₁, ◊Γ₂, α) / (¬□α, Γ₁, ¬◊Γ₂ ⇒ ◊Δ₁, ¬□Δ₂)

기술적 혁신점

트위스트 규칙 설계: 표준 부정 규칙을 다른 논리 연결사의 규칙과 통합하여 "단축" 규칙을 형성한다.
국소 대 전역 처리: lTS4는 부정을 국소적으로 처리하고(주요하지 않은 문맥에서 부정 유지), gTS4는 전역적으로 처리한다(모든 문맥에서 부정 삭제).
표준 부정 규칙 제거: 겐첸 LK 체계의 표준 부정 규칙 (¬left)와 (¬right) 사용을 완전히 회피한다.

실험 설정

이론 검증 방법

본 논문은 수학적 증명 방법을 사용하여 이론 결과를 검증하며, 주로 다음을 포함한다:

귀납적 증명: 기본 성질과 동치성 증명에 사용
구성적 증명: 구체적인 증명 변환 제시
사례 분석: 구체적인 예시를 통해 다양한 체계의 증명 길이 비교

평가 지표

증명 길이: 다양한 체계가 생성하는 증명 단계 수 비교
부분공식 성질: 증명에 나타나는 모든 공식이 결론 공식의 부분공식임을 보장
절 제거성: 체계의 절 제거 가능성

실험 결과

주요 결과

정리 동치성 (정리 3.3)

lTS4, gTS4와 표준 GS4 체계의 정리 동치성을 증명했다: {S | lTS4 ⊢ S} = {S | gTS4 ⊢ S} = {S | GS4 ⊢ S}

절 제거 정리 (정리 4.4)

lTS4와 gTS4의 경우, 절 규칙은 절 제거 체계에서 허용 가능하다.

부분공식 성질 (정리 4.5)

lTS4와 gTS4 모두 부분공식 성질을 가지며, 체계의 분석성을 보장한다.

사례 분석

예 3.5: 증명 가능한 시퀀트 ¬¬¬◊¬p ⇒ ¬◊¬¬□¬¬¬p 고려

lTS4 증명(7단계):

¬p ⇒ ¬p
¬p, ¬◊¬p ⇒ (¬◊leftₜ)
¬¬¬p, ¬◊¬p ⇒ (¬¬leftₜ)
◊¬¬¬p, ¬◊¬p ⇒ (◊left)
¬¬□¬¬¬p, ¬◊¬p ⇒ (¬¬leftₜ)
¬◊¬p ⇒ ¬◊¬¬□¬¬¬p (¬◊rightₜ)
¬¬¬◊¬p ⇒ ¬◊¬¬□¬¬¬p (¬¬leftₜ)

gTS4 증명(7단계): 유사한 간결한 증명

GS4 증명(14단계): 표준 부정 규칙을 사용한 장황한 증명