결정 가능성(논리)

Decidability (logic)

논리학에서는 정답을 도출하기 위한 효과적인 방법이 존재한다면 참/거짓 판정 문제를 판단할 수 있다.0차 논리(명제 논리)는 결정 가능하지만 1차 이상의 논리에서는 결정 불가능.논리 시스템은 논리적으로 유효한 공식(또는 이론) 집합의 멤버십을 효과적으로 결정할 수 있다면 결정될 수 있습니다.이론(논리적 결과에 따라 닫힌 문장의 집합)은 임의의 공식이 이론에 포함되는지 여부를 결정하는 효과적인 방법이 있다면 결정 가능하다.많은 중요한 문제들은 결정할 수 없다. 즉, 멤버쉽을 결정하기 위한 효과적인 방법(모든 경우에 매우 긴 시간이 걸릴 수 있지만 유한한 시간 후에 정답을 반환하는 것)이 그들에게 존재할 수 없다는 것이 증명되었다.

논리 시스템의 결정 가능성

각 논리 시스템은 무엇보다도 입증가능성의 개념을 결정하는 구문적 요소논리적 타당성의 개념을 결정하는 의미적 요소를 모두 가지고 있습니다.논리적으로 유효한 시스템의 공식은 때때로 시스템의 이론이라고 불리며, 특히 괴델의 완전성 정리가 의미론 및 통사론의 결과의 동등성을 확립하는 1차 논리의 맥락에서 그러하다.선형 로직과 같은 다른 설정에서는 구문적 결과(프로비빌리티) 관계를 사용하여 시스템의 이론을 정의할 수 있습니다.

논리시스템은 임의의 공식이 논리시스템의 정리인지 아닌지를 판단하는 효과적인 방법이 있으면 결정 가능하다.예를 들어, 명제논리는 결정가능하다. 왜냐하면 진실표법은 임의명제식이 논리적으로 유효한지 여부를 결정하기 위해 사용될 수 있기 때문이다.

일반적으로 1차 로직은 결정할 수 없습니다.특히, 등식을 포함한 시그니처의 논리 검증 세트나, 2개 이상의 인수를 가지는 적어도1개의 다른 술어는 결정할 [1]수 없습니다.2차 논리 및 유형 이론과 같이 1차 논리를 확장하는 논리 시스템도 결정할 수 없습니다.

그러나 동일성을 갖는 단항 술어 미적분의 타당성은 결정될 수 있다.이 시스템은 함수 기호가 없고 등호 이외의 관계 기호가 한 개 이상의 인수를 사용하지 않는 시그니처로 제한됩니다.

어떤 논리체계는 이론집합만으로 충분히 표현되지 않는다.(를 들어 클린의 논리에는 이론이 전혀 없다.)이러한 경우 논리 시스템의 결정 가능성에 대한 대체 정의가 자주 사용되며, 예를 들어 시퀀스의 유효성 또는 논리 결과 관계 {(г, A) г A}보다 더 일반적인 것을 결정하기 위한 효과적인 방법을 요구한다.

이론의 결정 가능성

이론은 논리적인 결과에서 닫힌 것으로 종종 가정되는 일련의 공식입니다.이론의 결정가능성은 이론의 서명에 임의의 공식이 주어졌을 때 공식이 이론의 구성원인지 아닌지를 결정하는 효과적인 절차가 있는지 여부에 관한 것이다.결정성 문제는 이론이 고정된 공리의 논리적 결과 집합으로 정의될 때 자연스럽게 발생한다.

이론의 결정 가능성에 대한 몇 가지 기본적인 결과가 있다.이론의 서명에 있는 모든 공식은 이론의 논리적 결과가 될 것이고 따라서 이론의 구성원이 될 것이기 때문에 모든 모순된 이론은 결정될 수 있다.모든 재귀적으로 열거할 수 있는 1차 이론은 결정 가능하다.결정 가능한 이론의 연장은 결정될 수 없을지도 모른다.예를 들어, 명제 논리에는 결정 불가능한 이론이 있지만, 타당성 집합(최소 이론)

모든 일관된 확장은 결정할 수 없다는 특성을 가진 일관된 이론은 근본적으로 결정할 수 없다고 한다.사실, 모든 일관된 확장은 근본적으로 결정할 수 없습니다.장 이론은 결정할 수 없지만 본질적으로 결정할 수 있는 것은 아니다.로빈슨 산수는 본질적으로 결정할 수 없는 것으로 알려져 있고, 따라서 로빈슨 산수를 포함하거나 해석하는 모든 일관된 이론도 결정할 수 없다.

결정 가능한 1차 이론의 예로는 실제 닫힌이론프레스버거 산술이 있는 반면, 군 이론과 로빈슨 산술은 결정 불가능한 이론의 예들이다.

몇 가지 결정 가능한 이론들

결정 가능한 이론은 다음과 같습니다(Monk 1976, 페이지 234).[2]

결정성을 확립하기 위해 사용되는 방법에는 정량화 제거, 모델 완전성łł-Vaught 테스트가 포함된다.

결정할 수 없는 몇 가지 이론들

다음과 같은 결론을 내릴 수 없는 이론이 있다(Monk 1976, 페이지 279).[2]

  • 동등성을 갖는 모든 1차 서명의 논리적 타당성 집합. 1953년 Trakhtenbrot에 의해 확립된 2개 이상의 단항 함수 기호 또는 2개 이상의 아리티 함수 기호 중 하나.
  • 1949년 타르스키와 안제이 모스토프스키에 의해 확립된 덧셈, 곱셈, 등식을 수반하는 자연수의 1차 이론.
  • 1949년 줄리아 로빈슨에 의해 확립된 덧셈, 곱셈, 등식을 포함한 유리수의 1차 이론.
  • 1953년 [3]알프레드 타르스키에 의해 확립된 1차 군 이론.놀랍게도, 집단의 일반 이론은 결정할 수 없을 뿐만 아니라, 예를 들어 (Mal'cev 1961에 의해 확립된) 유한 집단의 이론과 같은 몇 가지 더 구체적인 이론도 있다.말체프는 또한 반군의 이론과 고리의 이론은 결정할 수 없다는 것을 증명했다.로빈슨은 1949년에 장 이론이 결정 불가능하다는 것을 확립했다.
  • 1950년 라파엘 로빈슨에 의해 확립된 로빈슨 산술(따라서 페아노 산술과 같은 일관된 확장)은 본질적으로 결정할 수 없다.
  • 등식과 두 개의 함수[4] 기호가 있는 1차 이론

해석 가능성 방법은 이론의 결정 불가능성을 확립하기 위해 종종 사용된다.만약 근본적으로 결정할 수 없는 이론 T가 일관된 이론 S에서 해석될 수 있다면, S 또한 본질적으로 결정할 수 없다.이것은 계산가능성 이론의 다대1 감소 개념과 밀접하게 관련되어 있다.

반신뢰성

결정성보다 약한 이론이나 논리체계의 속성은 반결정성입니다.이론에는 임의의 공식이 주어졌을 때 항상 그 공식이 이론 안에 있을 때 정확하게 말할 수 있지만, 그 공식이 이론 안에 없을 때 부정적인 답을 주거나 아예 답을 주지 않는 효과적인 방법이 있다면 반신반의할 수 있다.논리 시스템은 모든 정리가 최종적으로 생성되도록 정리(및 정리만)를 생성하는 효과적인 방법이 있다면 반신반의할 수 있다.이것은 결정 가능성과는 다릅니다. 왜냐하면 반감정 가능한 시스템에서는 공식이 정리가 아니라는 것을 확인하는 효과적인 절차가 없을 수 있기 때문입니다.

모든 결정 가능한 이론이나 논리 시스템은 반감정이 가능하지만, 일반적으로 그 반대는 사실이 아니다; 이론은 이론과 그 보완이 반감정이 가능해야 결정 가능하다.예를 들어 1차 논리의 논리유효성 집합 V는 반결정 가능하지만 결정 불가능하지는 않다.이 경우 A가 V에 속하지 않는지 여부를 임의의 공식 A에 대해 판단하는 효과적인 방법이 없기 때문입니다.마찬가지로, 재귀적으로 열거할 수 있는 1차 공리 집합의 논리적 결과 집합은 반감각적이다.위에 제시된 결정 불가능한 1차 이론의 많은 예는 이 형태이다.

완전성과의 관계

결정성은 완전성과 혼동해서는 안 된다.예를 들어, 대수적으로 닫힌 필드의 이론은 결정 가능하지만 불완전하지만, +와 ×를 가진 언어의 음이 아닌 정수에 대한 모든 진실된 1차 진술의 집합은 완전하지만 결정할 수 없다.불행하게도, 용어적 모호성으로서, "undecoverable statement"라는 용어는 종종 독립 스테이트먼트의 동의어로 사용된다.

계산 가능성과의 관계

결정 가능한 집합의 개념과 마찬가지로 결정 가능한 이론 또는 논리 시스템의 정의는 효과적인 방법 또는 계산 가능한 함수의 관점에서 제공될 수 있다.이것들은 일반적으로 교회의 논문에 따르면 동등하다고 여겨진다.실제로, 논리 시스템이나 이론이 결정 불가능하다는 증거는 적절한 집합이 결정 가능 집합이 아님을 보여주기 위해 계산 가능성의 공식 정의를 사용하고, 그 이론이나 논리 시스템이 어떤 효과적인 방법으로도 결정 불가능하다는 것을 보여주기 위해 처치의 논문을 인용할 것이다(Enderton 2001, 페이지 206ff).

게임의 맥락에서

일부 게임은 결정 가능성에 대해 분류되어 있습니다.

  • 체스는 쉽게 [5][6]이길 수 있다.완벽한 정보를 가진 다른 유한한 2인용 게임도 마찬가지입니다.
  • 무한 체스(규칙과 게임피스에 제한이 있음)에서 n의 짝은 결정 가능합니다.[7][8]단, (최종적으로 많은 조각이 있는) 위치가 강제적으로 승리하지만 유한[9]n에 대해 n의 짝이 되지 않습니다.
  • 한정된 보드 상에 불완전한 정보가 있는 팀 게임(단, 시간이 무제한)은 판별할 [10]수 없습니다.

「 」를 참조해 주세요.

레퍼런스

메모들

  1. ^ 1953년, Trahtenbrot.
  2. ^ a b Monk, Donald (1976). Mathematical Logic. Springer. ISBN 9780387901701.
  3. ^ Tarski, A.; Mostovski, A.; Robinson, R. (1953), Undecidable Theories, Studies in Logic and the Foundation of Mathematics, North-Holland, Amsterdam, ISBN 9780444533784
  4. ^ Gurevich, Yuri (1976). "The Decision Problem for Standard Classes". J. Symb. Log. 41 (2): 460–464. CiteSeerX 10.1.1.360.1517. doi:10.1017/S0022481200051513. S2CID 798307. Retrieved 5 August 2014.
  5. ^ 스택 Exchange 컴퓨터 사이언스체스 게임 무브먼트 TM은 결정 가능합니까?
  6. ^ 결정할 수 없는 체스 문제?
  7. ^ Mathoverflow.net/Decidability-of-chess-on-an-infinite-board 무한보드 체스의 결정성
  8. ^ Brumleve, Dan; Hamkins, Joel David; Schlicht, Philipp (2012). "The Mate-in-n Problem of Infinite Chess Is Decidable". Conference on Computability in Europe. Lecture Notes in Computer Science. Vol. 7318. Springer. pp. 78–88. arXiv:1201.5597. doi:10.1007/978-3-642-30870-3_9. ISBN 978-3-642-30870-3. S2CID 8998263.
  9. ^ "Lo.logic – Checkmate in $\omega$ moves?".
  10. ^ Poonen, Bjorn (2014). "10. Undecidable Problems: A Sampler: §14.1 Abstract Games". In Kennedy, Juliette (ed.). Interpreting Gödel: Critical Essays. Cambridge University Press. pp. 211–241 See p. 239. arXiv:1204.0299. CiteSeerX 10.1.1.679.3322. ISBN 9781107002661.}

참고 문헌