일반 틀

General frame

논리학에서 일반 프레임(또는 단순 프레임)은 추가 구조를 가진 Kripke 프레임으로, 모달중간 로직의 모델링에 사용된다.일반적인 프레임 의미론들은 크립케 의미론대수적 의미론들의 주요 덕목을 결합한다: 그것은 전자의 투명한 기하학적 통찰과 후자의 견고한 완성도를 공유한다.

정의

A modal general frame is a triple , where is a Kripke frame (i.e., R is a binary relation on the set F), and V is a set of subsets of F that is closed under the following:

  • (이진) 교차로, 유니언보어의 부울 연산
  • ={ x ( x y→ y A ( y로 정의된 작업

따라서 그들은 추가적인 구조를 가진 집합의 특별한 경우다.V의 목적은 프레임에 허용되는 평가를 제한하는 것이다: 프레임 , , \ \ \ \ , { { \ \) 일반 프레임 F에서 허용된다.

명제 변수 p{ x x F

그런 다음 V의 폐쇄 조건은 모든 공식 A(변수뿐만 아니라에 대해 V에 확인하십시오 이(가) V에 속하는지 확인하십시오.

A formula A is valid in F, if for all admissible valuations , and all points . A normal modal logic L is valid in the frame F, if all axioms (or equivalently, all theorems) of L are valid in F.이 경우에 우리는 F를 L-프레임이라고 부른다.

A Kripke frame may be identified with a general frame in which all valuations are admissible: i.e., , where denotes the power set of F.

프레임의 종류

일반적으로 일반 프레임은 Kripke 모델의 화려한 이름 이상일 수 없으며, 특히 접근성 관계에 대한 속성에 대한 모달 공리의 일치성은 상실된다.이는 허용 가능한 평가 집합에 추가 조건을 부과함으로써 해결할 수 있다.

프레임 = , , 을(를) 호출한다.

  • 구별되는 , A A y ) {\ VA y에서 = x
  • 타이트, A ( A y ) A V \A\ A이() xR {\\,y}을 의미하며은 다음과 같다.
  • 압축, 유한 교차 특성을 가진 V의 모든 부분 집합이 비어 있지 않은 교차점을 갖는 경우,
  • 원자, V가 단골격을 모두 포함하면
  • 정제, 차별화, 조여진다면
  • 정교하고 압축된 경우 기술적으로 설명해야 한다.

크립크 틀은 정제되고 원자적이다.그러나 무한의 크립키 프레임은 결코 소형화되지 않는다.모든 유한한 차별화 또는 원자 프레임은 크립케 프레임이다.

서술형 프레임은 이중성 이론 때문에 프레임의 가장 중요한 등급이다(아래 참조).정제된 프레임은 서술형 프레임과 크립키 프레임의 일반적인 일반화로 유용하다.

프레임의 작동 및 형태

Kripke 모델 , R , \ \ F은(는) 프레임 F, R 유도하며, 여기서 V는 V로 정의된다

생성된 서브프레임, p-모르픽 영상 및 Kripke 프레임의 불연속 조합의 기본적인 진실 보존 운영은 일반 프레임에서 유사하다.A frame is a generated subframe of a frame , if the Kripke frame is a generated subframe of the Kripke frame 즉, 는) 에서 위쪽으로 의 하위 집합이며, S = R × 이다.)

A p-morphism (or bounded morphism) is a function from F to G that is a p-morphism of the Kripke frames and , and satisfies the additional constraint

- [ f V 모든 W

The disjoint union of an indexed set of frames , , is the frame , where F is the disjoint union of I R{ 의 조합이며

The refinement of a frame is a refined frame defined as follows.우리는 동등성 관계를 고려한다.

G= /~ 를) ~ 의 동등성 클래스의 집합으로 한다 그런 다음,

완성도

Kripke 프레임과는 달리, 모든 정상적인 모달 논리 L은 일반 프레임의 클래스에 관하여 완전하다.This is a consequence of the fact that L is complete with respect to a class of Kripke models : as L is closed under substitution, the general frame induced by is an L-frame.더욱이 모든 논리 L은 하나의 서술적 틀에 관해서 완전하다.실제로 L은 그 규범적 모델에 관해서 완전하며, 규범적 모델(L규범적 프레임이라고 함)에 의해 유도된 일반적 프레임은 서술적이다.

욘손-타르스키 이중성

리거-니시무라 사다리는 1범용 직감론적 크립케 틀이다.
이중 헤이팅 대수학인 리거-니시무라 격자.그것은 1개의 발전기에 대한 자유 헤잉 대수학이다.

일반 프레임은 모달 알헤브라와 밀접한 관련이 있다. = F, , 은(는) 일반적인 프레임이다.The set V is closed under Boolean operations, therefore it is a subalgebra of the power set Boolean algebra . It also carries an additional unary operation, . The combined structure }}은는) 모달 대수학으로 F의 이중 대수라고 하며 + {로 표시된다

In the opposite direction, it is possible to construct the dual frame to any modal algebra . The Boolean algebra 에는 스톤 공간이 있으며, 그 기본 집합 FA의 모든 초여광 필터의 집합이다.+ 에 허용되는 가치의 V 집합은 F열린 하위 집합으로 구성되며, 접근성 관계 R은 다음과 같이 정의된다.

모든 울트라필터용 x와 y.

프레임과 프레임의 이중은 동일한 공식을 검증하므로 일반적인 프레임 의미론과 대수적 의미론은 어떤 의미에서 동등하다.모든 모달 대수의 이중 이중+)+ A {\ \에 이형적이다.모든 대수의 이중은 서술적이기 때문에 프레임의 이중의 경우 일반적으로 이것은 사실이 아니다.실제로 F{\은(는 이중F+ ) + {\(\ {F}에 대해 이형인 경우에만 설명된다

p-모형성의 이중성을 한 편으로는 정의할 수 있고, 다른 한편에서는 모달 대수 동형성의 이중성을 정의할 수도 있다.이렇게 하여 연산자)+ )+ 일반 프레임의 범주, 모달 알헤브라의 범주 사이에 한 쌍의 상반된 펑커가 된다.이러한 functors는 서술형 프레임과 모달 알헤브라의 범주 사이에 이중성(Bjarni JonssonAlfred Tarski이름을 따서 Jonsson-Tarski라고 함)을 제공한다.이것은 복잡한 알헤브라와 관계 구조물의 세트장 사이에 더 일반적인 이중성의 특별한 경우다.

직감 프레임

직관적 및 중간 로직의 프레임 의미론은 모달 로직의 의미론과 병렬로 개발될 수 있다.직관적인 일반 프레임은 3중 , , F이며 여기서 F부분적인 주문이며, V는 빈 세트를 포함하는 F상부 서브셋() 집합이며, 아래에서 닫힌다.

  • 교차로와 조합,
  • 작업 =(- B) B

타당성 및 기타 개념은 모달 프레임과 유사하게 도입되며, 허용 가능한 평가 집합의 취약한 폐쇄 특성을 수용하기 위해 몇 가지 변경이 필요하다.특히 직감 프레임 = , , (를) 부른다.

  • A ) 에 대해 \\for \ y A)}이) y 의미한다면
  • 콤팩트, 유한 교차로 속성이 있는 - V V의 모든 부분 집합이 비어 있지 않은 교차점을 갖는 경우.

촘촘한 직감 프레임은 자동으로 차별화돼 정교해진다.

The dual of an intuitionistic frame is the Heyting algebra . The dual of a Heyting algebra is the intuitionistic frame , where F is the set of all prime filters of A, the ordering is inclusion, and V consists of all subsets of F of the form

A 모달 케이스에서처럼 )+ + 반투명 펑커의 한 쌍으로, 헤이팅알헤이스트레이브라의 범주를 기술직주의 프레임의 범주와 사실상 동일하다.

전이적 반사적 모달 프레임에서 직관적 일반 프레임을 구성할 수 있으며, 그 반대의 경우도 모달 동반자를 참조한다.

참조

  • 알렉산더 차그로프와 마이클 자카리아셰프, 모달 로직, 옥스퍼드 대학 출판부, 1997년 옥스퍼드 로직 가이드 35권.
  • 2001년 캠브리지 대학 출판부의 이론 컴퓨터 과학의 패트릭 블랙번, 마아텐리케, 그리고 모달 로직 이데 베네마, 모달 로직, 케임브리지 대학 출판부의 이론 컴퓨터 과학의 53권.