경계 정량기
Bounded quantifier수학적 논리학의 형식 이론 연구에서는 경계 정량자가 표준 정량자 "∀"와 "∃"에 덧붙여 형식 언어에 포함되는 경우가 많다.경계 정량자는 그 경계 정량자에서 "정량화" 및 "정량화"와 다르다.경계가 있는 정량자 연구는 경계가 있는 정량자만 있는 문장이 참인지 아닌지를 판단하는 것이 종종 임의의 문장이 참인지를 판단하는 것만큼 어렵지 않다는 사실에 의욕을 갖는다.null
예
실제 분석의 맥락에서 경계 정량자의 예는 다음과 같다.
- > - 모든 x의 경우 x가 0보다 큼
- < - y가 0보다 작은 y가 있음
- - 모든 x에 대해 x는 실제 숫자임
- > y< ( = ) y<2}) - 모든 양의 숫자는 음수의 제곱이다.
산술의 경계 정량자
L이 페아노 산술의 언어라고 가정하자(모든 유한형에서 2차 산술이나 산술의 언어도 통할 것이다).경계 정량자에는 < {\ n과() <t {\의 두 가지 유형이 있다.이러한 정량자는 숫자 변수 n을 바인딩하며 n을 언급하지 않을 수 있지만 다른 자유 변수를 가질 수 있는 숫자 용어 t를 포함한다. ("여기서 숫자 용어"는 "1 + 1", "2", "2 x 3", "m + 3" 등과 같은 용어를 의미한다.)null
정량자는 다음 규칙에 의해 정의된다는 공식을 의미한다).null
이 정량자에는 몇 가지 동기가 있다.null
- 산술적 계층 구조와 같이 재귀 이론을 위한 언어의 적용에서 경계 정량자는 복잡성을 추가하지 않는다. }이가) 결정 가능한 술어인 경우 ∃n < { n 및 {\도 마찬가지로 결정 가능해진다.
- Peano 산술 연구에 대한 적용에서, 특정 집합이 한정된 정량자로만 정의될 수 있다는 사실은 집합의 계산성에 영향을 미칠 수 있다.예를 들어, 한정된 정량자만을 사용하는 프라이머리티의 정의가 있다: n은 제품이 n인 n보다 엄격히 적은 두 개의 숫자가 없는 경우에만 프라이머리다.그러나 language ,+ ,×,, ,, , , ={\\langle \} 언어에는 양자 자유 정의가 없다원시성을 정의하는 경계 정량화 공식이 있다는 사실은 각 숫자의 원시성이 계산적으로 결정될 수 있음을 보여준다.
일반적으로 자연수에 대한 관계는 다항식 계층 구조와 유사하게 정의되지만 다항식 대신 선형 시간 한계로 정의된 선형 시간 계층 구조에서 계산할 수 있는 경우에만 한정식을 통해 정의된다.결과적으로, 한정된 공식에 의해 정의될 수 있는 모든 술어는 Kalmar 초급, 상황에 민감한, 원시적인 재귀성이다.null
산술 계층 구조에서 경계 정량자만 포함하는 산술 공식을 0 0}^{0}}}}}}}}}}}}}{0라고 한다위첨자 0은 생략되기도 한다.null
집합 이론의 경계 정량자
L이 Zermelo-Fraenkel 세트 이론의 언어language,… = 이라고 가정해 보십시오. 여기서 줄임표는 파워셋 작동 기호 등의 용어 형성 연산으로 대체될 수 있다.경계 정량자는 t t과(와) {\ t 두 가지가 있다이러한 정량자는 설정된 변수 x를 결합하고 x를 언급하지 않을 수 있지만 다른 자유 변수를 가질 수 있는 t 항을 포함한다.null
이러한 정량자의 의미론은 다음 규칙에 의해 결정된다.
경계 정량자만 포함하는 ZF 공식을 0 0 라고 한다이것은 산술적 계층 구조와 유사하게 정의되는 레비 계층 구조의 기초를 형성한다.null
경계 정량자는 Δ0 분리만 포함된 Kripke-Platek 집합 이론과 건설적인 집합 이론에서 중요하다.즉, 한정된 정량자만 있는 공식에 대해서는 분리를 포함하지만 다른 공식에 대해서는 분리를 포함하지 않는다.KP에서 동기 부여는 set x가 경계 정량화 공식을 만족하는지가 x에 가까운 집합의 집합에만 의존한다는 사실이다(파워셋 연산은 용어를 형성하기 위해 여러 번 정밀하게 적용할 수 있기 때문이다).건설적인 집합론에서 그것은 서술적 근거에서 동기를 부여한다.null
참고 항목
- Subtyping - 유형 이론의 경계 수량화
- 시스템 F<: — 경계가 있는 다형식 람다 미적분
참조
- Hinman, P. (2005). Fundamentals of Mathematical Logic. A K Peters. ISBN 1-56881-262-0.
- Kunen, K. (1980). Set theory: An introduction to independence proofs. Elsevier. ISBN 0-444-86839-9.