실수에 대한 1차 이론의 결정성

Decidability of first-order theories of the real numbers

수학 논리학에서, 실수의 1차 언어란, 보편적·실존적 정량자와 실제 변수에 대한 표현의 평등과 불평등의 논리적 결합을 포함하는 1차 논리학의 모든 잘 형성된 문장들의 집합이다.대응하는 1차 이론은 실제 숫자에 맞는 문장 집합이다.표현에 사용할 수 있도록 허용된 원시적 연산에 따라 표현력이 다른 몇 가지 이론이 있다.이러한 이론의 연구에 있어서 근본적인 질문은 그것들이 결정 가능한가 하는 것이다: 즉, 문장을 입력으로 받아들이고 그 이론에 그 문장이 사실인가에 대한 질문에 "예" 또는 "아니오"의 답을 산출할 수 있는 알고리즘이 있는가.

실제 폐쇄장 이론은 원시 연산이 곱셈과 덧셈이라는 이론이다. 이는 이 이론에서 정의될 수 있는 유일한 숫자가 실제 대수적 숫자임을 암시한다.타르스키에 의해 증명된 바와 같이, 이 이론은 해독할 수 있다. 타르스키-세이덴버그 정리 및 퀀티퍼 제거를 참조하라.실제 폐쇄장 이론에 대한 의사결정 절차의 현재 구현은 종종 원통형 대수분해에 의한 정량화 제거에 기초한다.

타르스키의 지수함수 문제는 이 이론이 또 다른 원시 연산인 지수함수로 확장되는 것과 관련이 있다.이 이론이 해독할 수 있는 것인지 아닌지는 공공연한 문제지만, 샤누엘의 추측이 뒷받침된다면 이 이론의 결정성은 뒤따를 것이다.[1][2]이와는 대조적으로, 사인함수와 함께 실제 폐쇄장 이론의 확장은 불변의 정수의 인코딩이 가능하기 때문에 불변의 해석은 불가능하다(리차드슨의 정리 참조).

그래도 반드시 항상 종료되지 않는 알고리즘을 사용함으로써 사인 등의 기능으로 미해결 사례를 처리할 수 있다.특히 공식이 약간 혼란스러워도 만족도가 변하지 않는 입력식, 즉 공식이 강한 입력식에 대해서만 종료를 요구하는 알고리즘을 설계할 수 있다.[3]그 대신에 순수하게 휴리스틱한 접근법을 사용하는 것도 가능하다.[4]

참조

  1. ^ Macintyre, A.J.; Wilkie, A.J. (1995), "On the decidability of the real exponential field", in Odifreddi, P.G. (ed.), Kreisel 70th Birthday Volume, CLSI
  2. ^ Kuhlmann, S. (2001) [1994], "Model theory of the real exponential function", Encyclopedia of Mathematics, EMS Press
  3. ^ Ratschan, Stefan (2006). "Efficient Solving of Quantified Inequality Constraints over the Real Numbers". ACM Transactions on Computational Logic. 7 (4).
  4. ^ Akbarpour, Behzad; Paulson, Lawrence Charles (2010). "MetiTarski: An Automatic Theorem Prover for Real-Valued Special Functions". Journal of Automated Reasoning. 44.


Stub icon

이 대수 기하학 관련 기사는 단조롭다.위키피디아를 확장하여 도울 수 있다.