전제의 독립성

증명 이론과 구성 수학에서 전제의 독립성의 원리는 만약 φ와 ∃x가 형식 이론의 문장이고 φ → ∃x가 증명 가능하다면 φx (θ → θ)는 증명 가능하다고 말합니다.여기서 x는 φ의 자유 변수가 될 수 없지만, θ는 그에 따라 술어가 될 수 있습니다.

원리의 주요 적용은 직관주의 논리학 연구에 있으며, 원리는 일반적으로 유효하지 않습니다.그 원리는 고전 논리학에서 유효합니다.

논의

일반적으로, 담론의 영역은 사람이 거주하는 것으로 가정됩니다.즉, 이론의 일부는 최소한 어떤 용어입니다.토론을 위해 우리는 a와 같은 하나의 용어를 구별합니다.자연수 이론에서, 이 역할은 숫자 7에 의해 수행될 수 있습니다.아래에서 φ와 ψ는 x에 의존하지 않는 명제를 나타내며, θ는 에서 의존할 수 있는 술어입니다.

다음은 쉽게 설정할 수 있습니다.

• 첫째, φ가 참으로 설정되면 φ → ∃x θ가 증명 가능하다고 가정하면 φ → θ를 만족하는 x가 있습니다.
• 두 번째로, 만약 φ가 거짓으로 밝혀지면, 폭발에 의해 φ → ψ 형태의 어떤 명제도 성립합니다.그러면, 임의의 x는 공식적으로 φ → θ (그리고 실제로 이 형태의 모든 술어)를 만족시킵니다.

첫 번째 시나리오에서는 전제에 포함된 일부 x 바인딩이 결론에서 재사용되며, 일반적으로 이를 검증하는 전제 조건은 아닙니다.두 번째 시나리오에서, 특히 a 값은 원칙의 결론을 검증합니다.따라서 이 두 가지 경우 모두에서 일부 x는 결론을 검증합니다.

셋째, 이제 위의 두 가지 점과는 대조적으로 ①을 증명하거나 기각하는 방법을 알 수 없는 경우를 생각해 보십시오.핵심적인 경우는 φ이 공식 ∃z θ(z)일 때인데, 이 경우 선행 φ → ∃x θ는 사소한 것이 됩니다: "만약 θ이 만족스럽다면 θ은 만족할 수 있습니다."설명을 위해, π가 산술에서 결정 가능한 술어라는 것을 인정합니다. 즉, 주어진 숫자 b에 대해 명제 π(b)가 참 값을 검사하기 쉽다는 것을 의미합니다.좀 더 구체적으로, θ는 x가 증명 가능성이 알려지지 않은 수학적 추측의 공식적인 증명의 색인이라는 것을 표현해야 합니다.확실히 여기서, ∃x(θ → θ)를 설정하는 한 가지 방법은 θ를 진정으로 만족시키는 것으로 나타낼 수 있는 특정 지수 x를 제공하는 것입니다(일부 값 z가 θ를 만족한다고 가정하면 도움이 됩니다).그러나 그러한 x를 설명하는 것은 아직 증명되지 않았거나 거부된 추측의 증거를 정확하게 암호화하기 때문에 가능하지 않습니다(아직은 아닐 수도 있고 절대 아닐 수도 있습니다).

직관주의 논리학에서

위의 산술 예제는 약한 카운터 예제라고 하는 것을 제공합니다.존재 주장 δx (δ → δ)는 직관적인 방법으로 증명할 수 없습니다.φ → θ를 검증하는 x를 검사할 수 있으면 추측이 해결됩니다.

예를 들어, 다음과 같은 고전적인 인수를 생각해 보십시오.골드바흐 추측에는 증거가 있거나 없습니다.만약 그것이 증거를 가지고 있지 않다면, 그것이 증거를 가지고 있다고 가정하는 것은 터무니없고 무엇이든 뒤따릅니다 - 특히, 그것은 증거를 가지고 있습니다.따라서 골드바흐 추측에 증거가 있다고 가정하면 x가 그러한 증거의 색인인 자연수 지수 x가 있습니다.

이 문제는 또한 직관적 증명을 위해 BHK 해석을 사용하여 접근할 수 있으며, 이는 고전적 증명 미적분과 비교되어야 합니다.BHK는 φ → ∃ x θ의 증명은 φ의 증명을 취하고 ∃ x θ의 증명을 반환하는 함수로 구성된다고 말합니다.여기서 증명 자체는 함수에 대한 입력으로 작용할 수 있으며, 가능하면 x를 구성하는 데 사용될 수 있습니다. 그러면 ∃x의 증명(φ → θ)은 특정 x를 증명해야 하며, φ의 증명을 x가 그 값을 갖는 θ의 증명으로 변환하는 함수와 함께 표시해야 합니다.증명 미적분에서는 - 약한 반례에서와 마찬가지로 - 적합한 x는 수정 가능한 φ에 연결된 더 많은 입력을 사용해야만 제공될 수 있습니다.

실제로, 위반 모델을 사용하여, 전제 φ → ∃ x θ는 원칙에 의해 부여된 일반적인 존재 증명에 충분하지 않다는 것이 확인되었습니다.

규칙.

선행 조건이 약화될 수 있을 때 의미가 강화됩니다.여기서 관심을 끄는 것은 부정문 형태의 전제인 φ : = η입니다.

메타 이론적으로 δ → δ x δ가 산술적으로 증명을 가지고 있으면 δ x (δ → δ)도 증명을 가지고 있다는 것이 밝혀졌습니다.

이것이 익숙한 집합 ^[1]이론에도 적용되는지 여부는 알려지지 않았습니다.

실존적 정량자가 없는 π의 경우 직관주의 논리에 대한 이론은 이러한 성질의 규칙과 관련하여 잘 수행되는 경향이 있습니다.

크라이젤-푸트남 논리

직관적 명제 미적분은 다음과 같은 관련 원리가 공리로 채택될 때 여전히 분리 특성을 가집니다.

$표시({style \big (}\neg \eta \to (\alpha \lor \lor \lor ){\big )}\to \big (}(\neg \eta \to \alpha )\lor (\neg \eta \to \la ){\big )}}$

해당 규칙은 허용되는 규칙입니다.

고전 논리학에서

언급한 바와 같이, 고정 φ과 임의의 θ에 대한 전제 원칙의 독립성은 φ의 증명뿐만 아니라 거부로부터도 따릅니다.따라서, 배제된 중간 분해의 법칙을 공리적으로 가정하면, 원리는 유효합니다.

예를 들어, 여기서 ∃x (("y θ) → θ)는 항상 유지됩니다.보다 구체적으로, 다음과 같은 제안을 고려합니다.

"만약 골드바흐 추측에 대한 증명 지수가 존재한다면, 그 숫자 x는 골드바흐 추측에 대한 증명 지수는 골드바흐 추측의 증명 지수입니다.

이는 다음과 같이 고전적으로 입증할 수 있습니다.골드바흐 추측의 증명을 위한 지수가 존재하거나 그러한 지수가 존재하지 않습니다.한편, 만약 하나가 존재한다면, 그 인덱스가 무엇이든 위의 명제에서 유효한 x로 기능합니다.반면에, 만약 그러한 지수가 존재하지 않는다면, 그러한 지수도 존재하는 것은 모순되고, 폭발에 의해 모든 것이 뒤따릅니다 - 특히 x=7은 골드바흐 추측의 증거의 지수입니다.두 경우 모두 제안을 검증하는 일부 인덱스가 존재합니다.

구성적으로, 사람은 x를 제공할 필요가 있습니다. (그러면 φ가 유효하다고 가정하고 일부 y에 대해서도 y도 ∃). 고전적으로, φ에 대한 두 개의 가설에서 시작할 때 동일한 관심 결론을 도출하는 것으로 충분합니다.후자의 프레임워크에서, 일부 x는 어느 쪽이든 존재한다고 주장되며, 논리는 그것을 설명할 것을 요구하지 않습니다.

레퍼런스

• Jeremy Avigad and Solomon Feferman (1999). Gödel's functional ("Dialectica") interpretation (PDF). in S. Buss ed., The Handbook of Proof Theory, North-Holland. pp. 337–405.