유한 이중 관계 프레임 속성을 갖는 S4 양상 논리

직관주의 양상 논리 S4의 두 주요 변형인 CS4와 IS4는 오랫동안 유한 모델 속성(finite model property) 보유 여부가 미해결 문제였습니다. 본 연구는 이 중 CS4가 유한 프레임 속성(finite frame property)을 가짐을 증명하여 첫 번째 문제를 해결합니다. 또한, IS4와 밀접하게 관련된 세 가지 논리(GS4, GS4c, S4I)를 탐구합니다. GS4는 IS4에 괴델-덤멧 공리(Gödel–Dummett axiom)를 추가한 것으로, 기존의 실수 값 의미론 외에 이중 관계 의미론(birelational semantics)을 제시하고 이에 대한 강한 완전성(strong completeness)을 증명합니다. GS4c는 GS4의 확장으로, 이중 관계 의미론에 추가적인 합류 조건(confluence condition)을 부여하여 강한 완전성을 증명합니다. 이 두 논리는 실수 값 의미론에서는 유한 모델 속성을 갖지 않지만, 이중 관계 의미론에서는 유한 프레임 속성을 가짐을 증명합니다. 이는 이전에 미해결이었던 이들 논리의 결정가능성(decidability)을 즉시 확립하며, CS4, GS4, GS4c에 대해 coNEXPTIME 상한을 제공합니다. S4I는 이중 관계 의미론에서 양상 관계와 직관주의 관계의 역할을 바꾼 논리로, S4I에 대해서도 유한 프레임 속성과 결정가능성을 증명합니다. 종합적으로, 본 연구는 CS4, GS4, GS4c, S4I 모두 유한 프레임 속성을 가짐을 입증합니다.