교회논문(건설수학)

건설 수학에서 Church의 논문(CT)은 모든 전체 기능이 계산 가능하다는 공리론이다.이 공리는 Church-Turing 논문에서 그 이름을 따온 것인데,^{[citation needed]} 이 논문은 모든 계산 가능한 함수는 계산 가능한 함수지만, 구성주의 버전은 모든 함수가 계산 가능하다고 주장하면서 훨씬 더 강하다는 것이다.

공리 CT는 충분히 강한 시스템에서는 고전적 논리와 양립할 수 없다.예를 들어 CT를 추가 공리로 하는 헤이팅 산술(HA)은 제외된 중간 법칙의 일부 예를 반증할 수 있다.그러나 헤이팅 산술은 페이노 산술(PA)뿐 아니라 헤이팅 산술 플러스 처치의 논문과도 동일하다.즉, 배제된 중간의 법칙이나 교회의 논제를 추가하는 것은 헤잉 산수를 일관성이 없게 만드는 것이 아니라, 두 가지 모두를 추가하는 것이다.

형식명세서

함수에 대해 직접 정량화할 수 없는 HA와 같은 1차 이론에서 CT는 클렌의 T 술어를 사용하여 계산가능성을 정의함으로써 어떤 정의 가능한 함수가 계산가능하다는 공리 스키마로 명시되어 있다.두 변수의 각 공식 x(x,y)에 대해 스키마는 공리를 포함한다.

${\displaystyle(\forall x\;\exists y\;\varphi(x,y))\to(\exist e\;\fourall x\;\exists y,u\mathbf {T}(e, y)\wedge \varphi(x,y)}$

이 공리는 만약 모든 x에 대해 만족 satisfying이 있다면, 실제로 e는 공식을 만족시키는 Gödel의 일반 재귀 함수의 Gödel 번호로, 어떤 u는 사실 y가 func의 값이라는 사실을 증명하는 검증 가능한 계산 인코딩이 된다.x에서 tion at x

함수에 대해 직접 정량화할 수 있는 고차 계통에서 CT는 자연수에서 자연수까지 모든 함수를 계산할 수 있다는 단일 공리로 명시할 수 있다.

고전적 논리와의 관계

위에 나타낸 CT의 스키마 형태는 HA와 같은 건설적인 시스템에 추가되었을 때 제외된 중간계의 법칙의 부정을 내포하고 있다.예를 들어, 모든 튜링 기계는 주어진 입력에서 정지하거나 정지하지 않는 것이 고전적인 태토학이다.이러한 tautology를 가정하면, HA와 같이 충분히 강력한 시스템에서는 튜링 기계의 코드를 받아 기계가 정지하면 1을 반환하고 정지하지 않으면 0을 반환하는 함수 h를 형성할 수 있다.그러면 교회의 논문에서 이 기능 자체가 계산가능하다고 결론을 내리겠지만, 이는 잘못된 것으로 알려져 있는데, 이는 Halting 문제가 계산적으로 해결될 수 없기 때문이다.따라서 HA와 CT는 배제된 중간 법칙의 일부 결과를 반증한다.

위에 언급된 CT의 "단일 공리" 형태,

${\displaystyle(\forall f)(\exists e)(\forall n)(\exists u)[\mathbf {T}(e,n,f(n),u),}$

함수에 대해 정량화하고 모든 함수 f는 계산 가능하다고 말한다(지수 e로).이 공리는 전항의 함수 f와 같은 기능을 형성할 힘이 없는 일부 약한 고전적 시스템과 일치한다.${\displaystyle {예}_{}}$를 들어 약한 고전적 시스템 $R{\displaystyle {\mathsf{}}_{}}$ ${\displaystyle {\mathsf{C}}_{}}$ ${\displaystyle A_{\mathrm{}}}$ ${\displaystyle {\mathsf{0}}_{}}$ ${\$$displaystyle$ ${\$$mathsf$$${$RCA}_{0}}$은(는) ${\displaystyle {\mathsf{모든}}_{}}$ 기능이 계산 가능한 모델을 가지고$$ 있기 때문에 이 단일 공리와 일치한다$$.그러나 단축 형식은 전항의 함수 h와 같은 기능을 구성하기에 충분한 공리가 있는 시스템에서 제외된 중간 법칙과 일관되지 않게 된다.

확장교회논문

확장교회의 논문(ECT)은 특정 유형의 영역에 걸쳐 완전히 정의된 기능에 대한 주장을 확장한다.안드레이 마르코프 주니어가 설립한 건설 수학 학교에서 사용한다.스키마에 의해 공식적으로 다음과 같이 명시될 수 있다.

$\displaystyle(\forall x\;\psi (x)\exists y\;\varphi(x,y)\exists f(f,x,y,u)\exists y,u\mathbf {T}\wedge \varphi(x,y)}$

위의 $\psi {\displaystyle }$ ${\displaystyle \psi }$은(는) 거의 음성으로 제한된다$$.1차 산술(스키마가 E $C{\displaystyle }$ ${\displaystyle {T\mathrm{}}_{}}$ ${\displaystyle {}_{}}$ ${\$으로 지정된 경우)$$의 경우, 이는 $\psi {\displaystyle }$ ${\displaystyle \psi }}$이(가) 분리를 포함할 수 없으며$$, 실존 정량자는 $\Delta {\displaystyle {\mathrm{}}_{}^{}}$ ${\displaystyle {0\mathrm{}}_{}^{}}$ ${\displaystyle {\mathrm{}}_{}^{}}${\$displaystyle \Delta_{0}^{0}}}}}}}}}}}}}}}}}}{$0}}}}}}}}}}}}}}}}}}}}}}}}}($$decifiable 공식 앞에만

이 논문은 문장이 계산적으로 실현 가능한 경우에만 참이라는 특징을 가질 수 있다.사실 이는 다음과 같은 메타이론적 동등성에 의해 포착된다.^[1]

${\displaystyle HA+ECT_{0}\vdash(\varphi \좌우 이동)(\exists n\;n\Vdash \vdash \varphi )}$

${\displaystyle(HA+ECT_{0}\vdash \varphi )\좌우 이동(HA\vdash \exists n\;(n\Vdash \varphi )}}$

Here, ${\displaystyle n\Vdash \varphi }$ stands for "${\displaystyle n{\text{ realises }}\varphi }$". So, it is provable in ${\displaystyle HA}$ with ${\displaystyle ECT_{0}}$ that a sentence is true iff it is realisable.But also, ${\displaystyle \varphi }$ is provably true in ${\displaystyle HA}$ with ${\displaystyle ECT_{0}}$ iff ${\displaystyle \varphi }$ is provably realisable in ${\displaystyle HA}$ without ${\displaystyle ECT_{0}}$.

두 번째 등가성은 다음과 같이 마르코프의 원리(M)로 확장할 수 있다.

${\displaystyle(HA+ECT_{0}+M\vdash \varphi )\좌우 이동(\exists n\;;PA\vdash({\bar{n}\Vdash \varphi )}$

So, ${\displaystyle \varphi }$ is provably true in ${\displaystyle HA}$ with ${\displaystyle ECT_{0}}$ and ${\displaystyle M}$ iff there is a number n which provably realises ${\displaystyle \varphi }$ in ${\displaystyle PA}$. The existential quantifier has to be outside ${\disp$이 경우$$ PA는 비건설적이며 존재 속성이 결여되어 있기 때문에 $레이스타일 PA}.$

참조

• 엘리엇 멘델슨(1990) "교회의 논문과 수학적 증명에 대한 두 번째 생각", Journal of Physical 87(5) : 225–233.