페아노 산술 (편집)

(불러오기) (편집 필터 규칙)

[[분류:가져온 문서/오메가]]
수학에서, 페아노 산술(Peano arithmetic)이란 [[자연수]] 체계를 묘사하는 1차 이론이다. 이론 전산학(theoretical computer science)에서 프로그램의 정당성 증명이나 계산 가능성 이론(computability theory)과 같은 분야에서 활용된다.

== 정의 ==
페아노 산술은 다음과 같은 요소들로 이루어져 있다 :
* 논리 기호들과 등호 ([math(=)])
* 상수 기호 [math(0)]
* 두 자리 관계 기호 [math(\le)]
* 한 자리 함수 기호 [math(S)]
* 두 자리 함수 기호 [math(+)], [math(\cdot)]

페아노 산술은 1차 이론으로, 1차 논리학의 논리 공리들과 추론 규칙들을 포함하고 있다. 또한 다음과 같은 공리들을 갖고 있다:
* [math(\forall x [S(x)\neq 0])]
* [math(\forall x\forall y [S(x)=S(y)\to x=y])]
* [math(\forall x \forall y (x\le S(y) \land x\neq y\to x\le y))]
* [math(\forall x\forall y (x\le y \lor y\le x))]
* [math(\forall x (x\le 0 \to x=0))]
* [math(\forall x (x+0=x))]
* [math(\forall x\forall y x+S(y)=S(x+y))]
* [math(\forall x (x\cdot 0=0))]
* [math(\forall x \forall y [x\cdot S(y)=x\cdot y+x])]
* 임의의 1차 문장 [math(\phi)]에 대해 [math(\phi(0) \land \forall x [\phi(x)\to \phi(S(x){{{)}}}{{{]}}}\to \forall x \phi(x))]

마지막 공리는 하나의 공리가 아니라 각 [math(\phi)]에 대해서 주어지는 공리꼴이다. 페아노 산술은 각 문헌마다 정의가 약간씩 다르게 나와 있다. 하지만 그 정의들은 모두 동치이다. 형식 이론은 공리들의 집합으로 정해지는 것이 아니라 공리들로부터 생성된 형식 이론임에 유의하라.

== 이론의 일관성 ==
[[괴델의 불완전성 정리]]에 의해, 페아노 산술의 일관성은 페아노 산술 내에서 증명될 수 없다. 하지만 겐첸에 의하면, [math(\varepsilon_0)]의 well-foundedness를 가정하면 페아노 산술의 일관성을 증명할 수 있다. 또한, ZF와 같은 강력한 이론들은 페아노 산술의 일관성을 증명할 수 있다.

[Include(틀:가져옴2,O=오메가, C=[[https://creativecommons.org/licenses/by-nc-sa/3.0/deed.ko|CC BY-NC-SA 3.0]])]

(임시 저장) (임시 저장 불러오기)

(↪️) (💎) (🛠️) (추가)

[Include(틀:가져옴2,O=오메가, C=[[https://creativecommons.org/licenses/by-nc-sa/3.0/deed.ko|CC BY-NC-SA 3.0]])]

비로그인 상태입니다. 편집한 내용을 저장하면 지금 접속한 IP가 기록됩니다.

편집을 전송하면 당신은 이 문서의 기여자로서 본인이 작성한 내용이 CC BY 4.0에 따라 배포되고, 기여한 문서의 하이퍼링크나 URL로 저작자 표시가 충분하다는 것에 동의하는 것입니다.