전지전능의 제한된 원리
Limited principle of omniscience건설 수학에서 전지전능(LPO)의 제한된 원리와 전지전능(LLPO)의 덜 제한된 원리는 비건설적이지만 배제된 중간(Bridge & Richman 1987)의 전체 법칙보다 약한 공리들이다.LPO와 LLPO 공리는 건설적인 역수학에서와 같이 논쟁에 필요한 비구성성의 양을 측정하는 데 사용된다.브루워의 의미에서도 약한 백작과 관련이 있다.
정의들
전지전능 주의 제한된 원리(Bridge & Richman 1987, 페이지 3):
- LPO: 각 a가i 0 또는 1인1 시퀀스 a0, a, a, ...의 경우, 다음은 유지된다: 모든 i에 대해i a = 0 또는 ak = 1인 k가 있다.[1]
전지전능의 덜 제한적인 원칙은 다음과 같다.
- LLPO: 모든 시퀀스 a0, a1, ... 각 a가i 0 또는 1이고, 최대 1 a가i 0이 아닌 경우, a와2i a가2i+1 각각 짝수 및 홀수 인덱스를 가진 항목인 모든 i에 대해2i a = 0 또는 모든2i+1 i에 대해 a = 0을 유지한다.
배제된 중간의 법칙이 LPO를, LPO가 LLPO를 내포한다는 것은 건설적으로 증명할 수 있다.그러나 이러한 함축적 의미는 건설 수학의 전형적인 시스템에서는 되돌릴 수 없다.
"전지적 참견"이라는 용어는 수학자가 LPO의 결론에 있는 두 가지 사례 중 어떤 경우를 주어진 순서 (ai)에 대해 보유하는지를 어떻게 구별할 수 있는지에 관한 사고 실험에서 유래한다.'k가k a = 1인가'라는 질문에 부정적으로 답하는 것은 음성으로 가정해 전체 시퀀스를 조사해야 할 것으로 보인다.이를 위해서는 무한히 많은 용어들을 검토해야 하기 때문에, 이러한 결정을 내릴 수 있다는 공리는 비숍(1967년)에 의해 "전지적 참견 원리"라고 불렸다.
참조
- ^ Mines, Ray (1988). A course in constructive algebra. Richman, Fred and Ruitenburg, Wim. New York: Springer-Verlag. pp. 4–5. ISBN 0387966404. OCLC 16832703.
- Bishop, Errett (1967). Foundations of Constructive Analysis. ISBN 4-87187-714-0.
- Bridges, Douglas; Richman, Fred (1987). Varieties of Constructive Mathematics. ISBN 0-521-31802-5.
