Formal proof

논리학(logic)과 수학(mathematics)에서, 형식적 증명(formal proof) 또는 유도(derivation)는 유한한 문장(sentences)의 열(sequence, 형식적 언어의 경우에서 잘-형성된 공식이라고 불림)이며, 각 문장은 공리, 가정이거나 열에서 추론의 규칙에 의해 앞 문장을 따릅니다. 그것은 엄격한, 모호하지 않고 기계적으로 검증할 수 있다는 점에서 자연어 논증과 다릅니다.^[1] 만약 가정의 집합이 빈 것이면, 형식적 증명에서 마지막 문장은 형식적 시스템(formal system)의 정리(theorem)라고 불립니다. 정리의 개념은 일반적으로 유효하지 않고, 따라서 항상 주어진 문장의 증명을 찾거나 어떤 것도 존재하지 않는다고 결정할 수 있는 방법이 없을 수 있습니다. 피치-스타일 증명(Fitch-style proof), 시퀀트 계산법(sequent calculus) 및 자연 연역(natural deduction)의 개념은 증명 개념의 일반화입니다.^[2]^[3]

정리는 증명에서 선행하는 모든 잘-형성된 공식의 구문적 결과입니다. 잘-형성된 공식이 증명의 일부로 자격이 되려면, 그것은 증명 열에서 이전의 잘-형성된 공식에 (일부 형식적 시스템의) 연역적 장치(deductive apparatus)의 규칙을 적용한 결과여야 합니다.

형식적 증명은 종종 (예를 들어, 증명 검사기와 자동화된 정리 증명기의 사용을 통해) 대화형 정리 증명(interactive theorem proving)에서 컴퓨터의 도움으로 구성됩니다.^[4] 중요하게도, 이들 증명은 컴퓨터에서도 자동으로 확인될 수 있습니다. 형식적 증명을 확인하는 것은 보통 간단하지만, 증명을 찾는 문제 (자동화된 정리 증명)는 보통 사용 중인 형식적 시스템에 따라 계산적으로 다루기 어렵고/또는 오직 반-결정가능(semi-decidable)입니다.

Background

Formal language

형식적 언어는 기호의 유한한 수열의 집합입니다. 그러한 언어는 표현의 어떤 것의 임의의 의미를 참조 없이 정의될 수 있습니다; 그것은 임의의 해석이 부여되기 전에 – 즉, 그것이 임의의 의미를 가지기 전에 존재할 수 있습니다. 형식적 증명은 일부 공식 언어에서 표현됩니다.

Formal grammar

형식적 문법 (형성 규칙이라고도 불림)은 형식적 언어의 잘-형성된 공식(well-formed formulas)의 정확한 설명입니다. 그것은 잘-형성된 공식을 구성하는 형식적 언어의 알파벳에 걸쳐 일련의 문자열과 동의어입니다. 어쨌든, 그것은 의미론 (즉, 그들이 의미하는 것)을 설명하지는 않습니다.

Formal systems

형식적 시스템 (논리적 계산, 또는 논리적 시스템이라고도 불림)은 연역적 장치 (연역적 시스템이라고도 불림)와 함께 형식적 언어로 구성됩니다. 연역적 장치는 일련의 변환 규칙 (추론 규칙이라고도 불림) 또는 일련의 공리로 구성되거나, 둘 다를 가질 수 있습니다. 형식적 시스템은 하나 이상의 다른 표현에서 하나의 표현을 유도하기 위해 사용됩니다.

Interpretations

형식적 시스템의 해석은 기호에 의미를 부여하고, 형식적 시스템의 문장에 진리 값을 부여하는 것입니다. 해석의 연구는 형식적 의미론(formal semantics)이라고 불립니다. 해석을 제공하는 것은 모델(model)을 구성하는 것과 동의어입니다.

References

^ Kassios, Yannis (February 20, 2009). "Formal Proof" (PDF). cs.utoronto.ca. Retrieved 2019-12-12.
^ The Cambridge Dictionary of Philosophy, deduction
^ Barwise, Jon; Etchemendy, John Etchemendy (1999). Language, Proof and Logic (1st ed.). Seven Bridges Press and CSLI.
^ Harrison, John (December 2008). "Formal Proof—Theory and Practice" (PDF). ams.org. Retrieved 2019-12-12.

External links

"A Special Issue on Formal Proof". Notices of the American Mathematical Society. December 2008.
2πix.com: Logic Part of a series of articles covering mathematics and logic.
Archive of Formal Proofs
Mizar Home Page

[1] Kassios, Yannis (February 20, 2009). "Formal Proof" (PDF). cs.utoronto.ca. Retrieved 2019-12-12.

[2] The Cambridge Dictionary of Philosophy, deduction

[3] Barwise, Jon; Etchemendy, John Etchemendy (1999). Language, Proof and Logic (1st ed.). Seven Bridges Press and CSLI.

[4] Harrison, John (December 2008). "Formal Proof—Theory and Practice" (PDF). ams.org. Retrieved 2019-12-12.

[1]

[2]

[3]

[4]