Q0(수학 로직)

Q는₀ 단순 형식 람다 미적분의 피터 앤드류스의 공식으로, 1차 논리 + 집합론에 필적하는 수학의 기초를 제공합니다.이것은 고차 로직의 한 형태이며 HOL 정리 프로버 패밀리의 로직과 밀접하게 관련되어 있습니다.

정리 증명 시스템 TPS와 ETPS는 Q에 기초하고₀ 있습니다.2009년 8월, TPS는 사상 최초의 고차 정리 증명 ^[1]시스템 경쟁에서 우승했다.

Q의₀ 공리

이 시스템에는 5개의 공리만 있으며, 이는 다음과 같이 기술할 수 있습니다.

${\displaystyle (1)}$ ${\displaystyle g_{oo}T\land g_{oo}F=\forall x_{o}\centerdot g_{oo}x_{o}$

$(\displaystyle (2^{\alpha })}$ $\displaystyle [x_{\alpha }=y_{\alpha}\supset \centerdot \,h_{o\alpha}x_{\alpha}=h_{o\alpha}y_{\alpha}}}$

$(\displaystyle (3^{\alpha \alpha })}$ $\displaystyle f_{\alpha \display}=g_{\alpha \display}=\forall x_{\alpha \display}x_{\display}=g_{\alpha \display}x_{\display}$

${\displaystyle(4)}$ ${\displaystyle [\displayda \mathbf {x_{\alpha }} \mathbf {A} _{\alpha } =\mathbf {S} _{A_{\alpha }} } ^{\mathbf {B} } } _{\mathbf {B} } } } } } } } }$

${\displaystyle (}$ ${\displaystyle 5}$)$${ $displaystyle$($5$)${\displaystyle {}_{}}$℩$$ ${\displaystyle i_{}}$ (${\displaystyle {}_{}{}_{}}$ i ${\displaystyle {}_{}}$ [ ${\displaystyle {}_{}}$ ${\displaystyle {}_{}{}_{}}$ ${\displaystyle {yi}_{}]=}$ ${\displaystyle {yi}_{}}$ ${\displaystyle ({}_{}}$ $displaystyle _$ i ($$$oi$ )$}[{\$$text{\text}$$Q}_{oi}y_{i}=y_{i},}$

(축 2, 3, 4는 유사한 공리의 패밀리인 공리 스키마입니다.Axiom 2와 Axiom 3의 인스턴스는 변수와 상수의 유형에 따라 다를 뿐이지만 Axiom 4의 인스턴스는 A와 B를 대체하는 식을 가질 수 있습니다.)

첨자 "o"는 부울 값의 유형 기호이고 첨자 "i"는 개별(비부울) 값의 유형 기호입니다.이러한 순서는 함수 유형을 나타내며, 서로 다른 함수 유형을 구별하기 위한 괄호를 포함할 수 있습니다.α 및 β와 같은 첨자가 있는 그리스 문자는 유형 기호의 구문 변수입니다.A, B, C 등의 굵은 대문자는 WFF의 구문 변수이며 x, y 등의 굵은 소문자는 변수의 구문 변수입니다.S는 모든 자유 발생 시 구문 치환을 나타냅니다.

유일한 원시 상수는 각 유형 α의 구성원의 동일성을 나타내는 Q와 정확히 한 개인을 포함하는 집합의 고유한 요소인 개인을 위한 설명 연산자를 나타내는 _(i(oi))θ이다_((oα)α).기호 and와 대괄호("[" 및 "]")는 언어의 구문입니다.다른 모든 기호는 수량자 and 및 ∃를 포함하여 이러한 기호가 포함된 용어의 약어입니다.

Axiom 4에서 x는 B에서 A에 대해 자유로워야 하며, 이는 치환으로 인해 A의 자유 변수가 결합되는 일이 없음을 의미한다.

공리에 대해서

• Axiom 1은 T와 F가 유일한 부울 값이라는 생각을 나타냅니다.
• Axiom 스키마^α 2와^αβ 3은 함수의 기본 특성을 나타냅니다.
• Axiom 스키마 4는 defines 표기법의 성질을 정의한다.
• Axiom 5는 선택 연산자가 개인에 대한 등식 함수의 역함수라고 말한다. (하나의 인수가 주어지면 Q는 개인을 개인을 포함하는 집합/프리디케이트에 매핑한다.Q에서₀ x = y는 Qxy의 약자로, (Qx)y의 약자입니다.

Andrews 2002에서 Axiom 4는 대체 과정을 세분화하는 5개의 하위 파트로 개발되었습니다.여기서 제시된 공리는 대안으로 논의되고 하위 부분에서 증명된다.

Q에서의₀ 추론

Q에는₀ 하나의 추론 규칙이 있습니다.

규칙 R. C와 A_α = B에서_α C에서 A의_α 발생을 B의_α 발생으로 치환한 결과를 추론한다. 단, C에서 A의_α 발생이 (변수의 발생) 바로 앞에 있지 않은 경우.

추론 Rθ의 파생 규칙은 가설 집합 H로부터 추론을 가능하게 한다.

규칙 R'A의_α 1회 발생을 B의 발생으로_α 치환하여 C에서 H a_α A = B_α, H c C, D를 구하면 다음과 같은 조건이 충족된다.

• C에서 A의 발생은_α immedi 바로 앞에 있는 변수의 발생이 아닙니다.
• A = B에_α 자유_α 변수가 없으며 A가_α 치환될 때 H의 구성원은 C에 결합된다.

참고: C에서 A를_α B로_α 치환하는 제한은 가설과 A_α = B에서_α 모두 자유로운 변수를 치환한 후에도 동일한 값을 가지도록 계속 구속합니다.

Q에 대한₀ 추론 정리는 규칙 R can를 사용하여 가설에서 얻은 증명은 가설 없이 규칙 R을 사용하여 증명으로 변환될 수 있음을 보여준다.

일부 유사한 시스템과 달리, Q에서의₀ 추론은 WFF 내의 모든 깊이에 있는 하위 표현식을 동등한 표현으로 대체합니다.예를 들어 다음과 같은 공리를 들 수 있습니다.

1. µxPx
2. Px q Qx

그리고 A b B （ A b A ), B ）라는 사실은 정량자를 제거하지 않고 진행할 수 있습니다.

3. A 및 B의 인스턴스화 Px ( (Px q Qx )
4. 3행에서 1행으로 치환되는 µx(Px µ Qx) 규칙 R.

메모들

레퍼런스

• Andrews, Peter B. (2002). An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof (2nd ed.). Dordrecht, The Netherlands: Kluwer Academic Publishers. ISBN 1-4020-0763-9. '1'도 참조해 주세요.
• Church, Alonzo (1940). "A Formulation of the Simple Theory of Types" (PDF). Journal of Symbolic Logic. 5: 56–58. doi:10.2307/2266170. Archived from the original (PDF) on 2019-01-12.

추가 정보

• Q에 대한₀ 좀 더 자세한 설명; 스탠포드 철학 백과사전에 실린 처치의 유형 이론에 대한 기사의 일부.
• 수학 로직의 개요(Q의₀ 다양한 후계자 포함):수학의 기초. 계보 및 개요 doi: 10.4444/100.111.