실현 가능성

수학적 논리학에서 실현가능성은 건설적인 증거를 연구하고 그것들로부터 추가 정보를 추출하는 데 사용되는 증명 이론의 방법들의 집합이다.^[1]형식 이론의 공식은 실재자에 대한 지식이 공식의 진실에 대한 지식을 제공하는 방식으로 "실현자"로 알려진 사물에 의해 "실현"된다.실현성에는 많은 변화가 있다; 정확히 어떤 공식의 등급이 연구되고 어떤 개체가 실현자인지에 따라 다르다.

실현가능성은 직관적 논리의 BHK 해석을 공식화한 것으로 볼 수 있다. 실현가능성에서는 "증명"(BHK 해석에서 정의되지 않은 채 방치된) 개념이 "실현자"라는 형식적 개념으로 대체된다.대부분의 실현가능성의 변형은 연구되고 있는 공식적인 시스템에서 증명할 수 있는 어떤 진술도 실현가능하다는 정리로 시작한다.그러나 실재자는 공식 증명서가 직접 제공하는 것보다 공식에 대한 더 많은 정보를 제공한다.

직관적 실현 가능성에 대한 통찰력을 주는 것을 넘어, 실현 가능성을 적용하여 직관적 이론에 대한 분리 및 존재 특성을 증명하고 증명 채굴에서처럼 교정으로부터 프로그램을 추출할 수 있다.실현성 토포스를 통한 토포스 이론과도 관련이 있다.

예제: 숫자에 의한 실현 가능성

클린의 실재능력은 헤잉 산술에서 수식에 자연수를 실재자로 사용한다.헤잉 산술의 언어에서 자연수 n과 공식 A 사이의 관계 "n realize A"를 정의하기 위해 다음과 같은 절을 사용한다.몇 가지 표기법이 필요하다. 첫째, 순서 쌍(n,m)을 고정 유효 쌍 함수를 사용하여 단일 숫자로 처리한다. 둘째, 각 자연수 n에 대해 φ은_n 지수 n을 가진 계산 가능한 함수다.

n은 s=t가 참일 경우에만 원자 공식 s=t를 실현한다.따라서 모든 숫자는 참 방정식을 실현하고, 어떤 숫자도 거짓 방정식을 실현하지 못한다.
한 쌍(n,m)은 n이 A를 깨닫고 m이 B를 깨닫는 경우에만 공식 AbB를 실현한다.따라서 접속사용 실라이저는 결막용 실라이저 쌍이다.
한 쌍(n,m)은 다음과 같은 hold가 0 또는 1인 경우에만 공식 AbB를 실현하며, n이 0이면 m이 A를 실현하고, n이 1이면 m이 B를 실현한다.따라서 절연에 대한 실연자는 명시적으로 불연속(n 포함) 중 하나를 선택하고 그에 대한 실연자를 제공한다(m 포함.
숫자 n은 A를 실현하는 모든 m에 대해 φ_n(m)이 B를 실현하는 경우에만 공식 A→B를 실현한다.따라서 암시에 대한 실현자는 가설에 대한 실현자를 취하고 결론에 대한 실현자를 생성하는 계산 가능한 함수다.
a쌍(n,m)은 m이 a(n)에 대한 실재제일 경우에만 공식(∃∃ x)A(x)를 실현한다.따라서 실존적 공식에 대한 실존적 공식에 대한 실존적 공식은 그 증인과 함께 실존적 공식에 대한 명시적 증인을 생성한다.
숫자 n은 모든 m에 대해 φ_n(m)을 정의하고 A(m)를 실현하는 경우에만 공식(∀ x)A(x)를 실현한다.따라서 범용문을 위한 실현자는 m으로 인스턴스화된 공식에 대한 실현자를 각 m에 대해 생성하는 계산 가능한 함수다.

이 정의로 다음과 같은 정리를 얻는다.^[2]

A를 헤이팅 산술(HA)의 문장으로 하자.만약 HA가 A를 증명한다면 n은 A를 실현하는 n이 있다.

한편, 실현되지만 HA에서는 증명할 수 없는 공식들이 있는데, 로즈가 처음 확립한 사실이다.^[3]

이 방법에 대한 추가 분석을 통해 HA가 "분리 및 존재 특성"^[4]을 가지고 있음을 증명할 수 있다.

HA가 문장(문장 x)A(x)를 증명하는 경우, HA가 A(n)를 증명하는 n이 있다.
만약 HA가 AbB를 증명한다면, HA는 A를 증명하거나 HA가 B를 증명한다.

후기 개발

크라이셀은 활자화된 람다 미적분을 현실자의 언어로 사용하는 변형현실성을 도입했다.변형된 실현가능성은 마르코프의 원리가 직관적 논리에서 파생될 수 없다는 것을 보여주는 한 방법이다.반대로 다음과 같은 전제 독립성의 원칙을 건설적으로 정당화할 수 있도록 한다.

(A\rightarrow \exists x\;P(x))\rightarrow \exists x\;(A\rightarrow P(x))

→

(A\rightarrow \exists x\;P(x))\rightarrow \exists x\;(A\rightarrow P(x))

(A\rightarrow \exists x\;P(x))\rightarrow \exists x\;(A\rightarrow P(x))

(A\rightarrow \exists x\;P(x))\rightarrow \exists x\;(A\rightarrow P(x))

(

(A\rightarrow \exists x\;P(x))\rightarrow \exists x\;(A\rightarrow P(x))

)

(A\rightarrow \exists x\;P(x))\rightarrow \exists x\;(A\rightarrow P(x))

→

(A\rightarrow \exists x\;P(x))\rightarrow \exists x\;(A\rightarrow P(x))

(A\rightarrow \exists x\;P(x))\rightarrow \exists x\;(A\rightarrow P(x))

( ) → ∃ x

(A\rightarrow \exists x\;P(x))\rightarrow \exists x\;(A\rightarrow P(x))

(

(A\rightarrow \exists x\;P(x))\rightarrow \exists x\;(A\rightarrow P(x))

)

}

{\

displaystyle

(

A\rightarrow \exists x\;P(

x)\

rightarrow \exists x\;(A\rightarrow

P

(x

상대적 실현가능성은^[5] 디지털 컴퓨터 시스템에서 실물을 근사치만 할 수 있을 때 모든 실제 숫자에 대한 계산 가능한 연산처럼 반드시 계산할 수 없는 데이터 구조의 재귀적 또는 재귀적으로 열거된 요소들의 직관적 분석이다.

적용들

실현가능성은 겉으로 보기에 비건설적인 수학적 증명으로부터 콘크리트 "프로그램"을 추출하기 위해 증명 채굴에 사용되는 방법 중 하나이다.실현가능성을 이용한 프로그램 추출은 Coq와 같은 일부 증명 보조자에게 구현된다.

참고 항목

메모들

^ 판 우스틴 2000
^ 반 우스틴 2000, 페이지 7
^ 로즈 1953년
^ 판 우스틴 2000, 페이지 6
^ 버키달 2000

참조

Birkedal, Lars; Jaap van Oosten (2000). Relative and modified relative realizability.
크라이셀 G. (1959년)."유한유형의 건설적 함수에 의한 해석", in: 수학의 구성성, A에 의해 편집된.헤이팅, 노스홀랜드 101-128쪽
Kleene, S. C. (1945). "On the interpretation of intuitionistic number theory". Journal of Symbolic Logic. 10 (4): 109–124. doi:10.2307/2269016. JSTOR 2269016.
클레인, S. C. (1973), 페이지 95–112의 "실현 가능성: 소급 조사".
van Oosten, Jaap (2000). Realizability: An Historical Essay.
Rose, G. F. (1953). "Propositional calculus and realizability". Transactions of the American Mathematical Society. 75 (1): 1–19. doi:10.2307/1990776. JSTOR 1990776.

외부 링크

실현 가능성 실현 가능성 및 관련 주제에 대한 최신 논문에 대한 링크 모음입니다.

[1] 판 우스틴 2000

[2] 반 우스틴 2000, 페이지 7

[3] 로즈 1953년

[4] 판 우스틴 2000, 페이지 6

[5] 버키달 2000

[1]

[2]

[3]

[4]

[5]

Search

실현 가능성

네임스페이스

더

목차

예제: 숫자에 의한 실현 가능성

후기 개발

적용들

참고 항목

메모들

참조

외부 링크