페아노 산술

(+)분류 : 가져온 문서/오메가

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

목차

1. 정의
2. 이론의 일관성

1. 정의 _{✎ ⊖}

페아노 산술은 다음과 같은 요소들로 이루어져 있다 :

논리 기호들과 등호 (=)
상수 기호 0
두 자리 관계 기호 \\le
한 자리 함수 기호 S
두 자리 함수 기호 +, \\cdot

페아노 산술은 1차 이론으로, 1차 논리학의 논리 공리들과 추론 규칙들을 포함하고 있다. 또한 다음과 같은 공리들을 갖고 있다:

\\forall x [S(x)\\neq 0]
\\forall x\\forall y [S(x)=S(y)\\to x=y]
\\forall x \\forall y (x\\le S(y) \\land x\\neq y\\to x\\le y)
\\forall x\\forall y (x\\le y \\lor y\\le x)
\\forall x (x\\le 0 \\to x=0)
\\forall x (x+0=x)
\\forall x\\forall y x+S(y)=S(x+y)
\\forall x (x\\cdot 0=0)
\\forall x \\forall y [x\\cdot S(y)=x\\cdot y+x]
임의의 1차 문장 \\phi에 대해 \\phi(0) \\land \\forall x [\\phi(x)\\to \\phi(S(x){{{)}}}{{{]}}}\\to \\forall x \\phi(x)

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

2. 이론의 일관성 _{✎ ⊖}

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

이 문서의 내용 중 전체 또는 일부는 오메가에서 가져왔으며 CC BY-NC-SA 3.0에 따라 이용할 수 있습니다.

1. 정의 ✎ ⊖

2. 이론의 일관성 ✎ ⊖

1. 정의 _{✎ ⊖}

2. 이론의 일관성 _{✎ ⊖}