피치 표기법

Fitch notation

피치 표기법은 피치 도표(Frederic Fitch의 이름을 따서 명명)로도 알려져 있으며, 보초적 로직과 술어 로직에서 사용되는 공식적인 증명들을 구성하기 위한 공칭 시스템이다. 피치식 교정쇄는 교정쇄를 구성하는 문장의 순서를 줄지어 배열한다. 피치 표기법의 독특한 특징은 각 행의 들여쓰기 정도가 해당 단계에 대해 어떤 가정이 활성화되어 있는지를 전달한다는 것이다.

예

피치 스타일 교정에서 각 행은 다음과 같다.

  • 가정 또는 입증되지 않은 가정
  • (1) 추론 규칙과 (2) 해당 규칙을 면허하는 증명의 이전 행 또는 행의 인용에 의해 정당화된 문장.

새로운 가정을 도입하면 들여쓰기 수준이 높아지고, 가정이 이행될 때까지 후속 라인을 계속 들여쓰는 새로운 수직 "스코프" 막대가 시작된다. 이 메커니즘은 모든 라인에서 다시 작성할 필요가 없는 가정(순서형 증빙과 같이) 없이 교정에서 주어진 라인에 대해 어떤 가정이 활성화되어 있는지를 즉시 전달한다.

다음 예는 피치 표기법의 주요 특징을 나타낸다. 

0 __ [추측, P가 아니라면 P를 원함] 1 __ P [추측, 원함] 2 __가 아닌 [P] 2 __가 아닌 [P] 2 __가 아닌 [논란 소개: 1, 2] 4가 아닌 [부정 소개: 2] 5 _가 아닌 [원함, 원함 P를 원함] 6 P [부정 제거: 5] 7 P가 아니라면 [Bicondition 소개: 1 - 4, 5 - 6]

0. 무효 가정, 즉 우리는 상호작용을 증명하고 있다.
1. 우리의 첫 번째 부차적 증거: 우리는 l.h.s가 r.h.s.를 다음에 보여준다고 가정한다.
2. 부차적: 우리가 원하는 것을 자유롭게 가정할 수 있다. 여기서 우리는 환원작용을 목표로 한다.
3. 우리는 지금 모순을 가지고 있다.
4. 모순을 '원인'했다는 진술에 '사유'하지 않는 것으로 접두사를 붙일 수 있도록 한다.
5. 우리의 두 번째 부차적 방증: 우리는 l.h.s.를 보여주기 위해 r.h.s.를 가정한다.
6. 문 접두사에서 짝수 수의 nots를 제거할 수 있는 규칙을 호출한다.
7. 1부터 4까지 P가 P가 아닌 경우 P를, 5부터 6까지 P가 아닌 경우 P를 보여 주었으므로, 쌍동설을 도입할 수 있다.

참고 항목

참조

외부 링크