메타패스

메타패스

개발자	노먼 메길
안정된 릴리스	2021년 8월 7일 / 0.198[1]; 11개월 전 (2021년 8월 7일)
저장소	github.com/metamath/metamath-exe
기입처	ANSI C
운영 체제	Linux, Windows, MacOS
유형	컴퓨터 지원 증명 검사
면허증.	GNU General Public License (데이터베이스용 Creative Commons 퍼블릭 도메인 전용)
웹 사이트	metamath.org

메타매스는 수학 증명을 ^[2]보관, 검증 및 연구하기 위한 공식 언어이자 관련 컴퓨터 프로그램(증명 검사기)입니다.논리, 집합론,^[3] 수론, 대수, 위상, 분석 등의 표준 결과를 포함하는 메타마스를 사용하여 증명된 이론의 여러 데이터베이스가 개발되었습니다.

2022년 2월^[update] 현재 메타마스를 사용한 증명된 이론 집합은 가장 큰 공식화된 수학 집합 중 하나로, "정식화 100개 이론"^[5] 도전의 100개 이론 중 74개의 증명을^[4] 포함하고 있으며, 홀 라이트, 이자벨, Coq에 이어 네 번째이지만 Mizar, ProofPower, Lean, Acl, nqm2 이전에는 네 번째이다.메타패스 ^[6]형식을 사용하는 데이터베이스에는 17개 이상의 증명 검증자가 있습니다.

이 프로젝트는 공식화된 정리 데이터베이스를 일반 ^[7]웹사이트 형태로 인터랙티브하게 브라우징할 수 있는 최초의 프로젝트입니다.

메타마스어

메타매스 언어는 다양한 공식 시스템을 개발하는 데 적합한 메타 언어입니다.메타매스 언어에는 특정한 논리가 포함되어 있지 않습니다.대신 추론 규칙(공리로서 주장되거나 나중에 증명됨)이 적용될 수 있다는 것을 증명하는 방법으로 간주될 수 있다.증명된 이론의 가장 큰 데이터베이스는 기존의 ZFC 집합론과 고전 논리를 따르지만, 다른 데이터베이스는 존재하고 다른 데이터베이스는 생성될 수 있다.

메타매스 언어 설계는 단순성에 초점이 맞춰져 있다; 정의, 공리, 추론 규칙 및 정리를 기술하기 위해 사용되는 언어는 소수의 키워드로만 구성되며, 모든 증명은 변수의 치환을 기반으로 하는 하나의 단순한 알고리즘을 사용하여 체크된다(어떤 변수가 나중에 구별되어야 하는지에 대한 옵션 제공).대체가 이루어지다).^[8]

언어의 기본

수식을 구성하는 데 사용할 수 있는 기호 집합은 다음을 사용하여 선언됩니다.$c(기호 표시) 및$v(기호) 문장은 다음과 같습니다.

$($c 0 + = -> ( ) 용어 wff - $. ($) $v t r s Q $.

공식의 문법은 다음 조합으로 지정됩니다.$f(가설(가설)) 및$a(자동 어설션) 스테이트먼트. 예를 들어 다음과 같습니다.

$( 메타 변수 $의 속성 지정) t $f term t $. tr $f term r $. ts $f term s $. wp $f wff P $. wq $f wff Q $. (파트 1) $) weq $a wff t = r $. (파트 2) wim $im $im

추론의 공리와 규칙은 다음과 같이 지정된다.$a와 함께 진술.${그리고.$}블록 범위 지정 및 옵션$e(필수 가설) 진술. 예:

$( 상태 공리 a1 $) a1 $a - ( t = r -> ( t = s - > r = s ) $. $. ( 상태 공리 a2 $) a2 $a - ( t + 0 ) = t $. ${ min $e - P $e - ( P -> Q ) $ (추론 규칙 $a mponus mpens 정의) $.

하나의 구조를 사용하여$a구문 규칙, 공리 스키마 및 추론 규칙을 포착하는 것은 복잡한 유형 시스템에 의존하지 않고 고차 논리 프레임워크와 유사한 수준의 유연성을 제공하기 위한 것이다.

증명서

정리(및 도출된 추론 규칙)는 다음과 같이 작성된다.$p예를 들어 다음과 같습니다.

$(정리를 증명하라 $) th1 $p - t = t $= $(여기서 증명한다: $) tze tpl t weq tt a2 tze tt weq tt weq wim tt a2 tze tt tt tt weq tt weq weq tt a1 mp $.

증명서가 포함되어 있는 것에 주의해 주세요.$p진술.다음과 같은 상세한 증거를 요약합니다.

tt            $f 용어 t 움직이다           $a 용어 0 1,2 탭       $a 용어 ( t + 0 ) 3,1 동작하다       $a 꺼지다 ( t + 0 ) = t 1,1 동작하다       $a 꺼지다 t = t 1 a2          $a - ( t + 0 ) = t 1,2 탭       $a 용어 ( t + 0 ) 7,1 동작하다       $a 꺼지다 ( t + 0 ) = t 1,2 탭       $a 용어 ( t + 0 ) 9,1 동작하다       $a 꺼지다 ( t + 0 ) = t 1,1 동작하다       $a 꺼지다 t = t 10,11 wim     $a 꺼지다 ( ( t + 0 ) = t -> t = t ) 1 a2          $a - ( t + 0 ) = t 1,2 탭       $a 용어 ( t + 0 ) 14,1,1 a1     $a - ( ( t + 0 ) = t -> ( ( t + 0 ) = t -> t = t ) ) 8,12,13,15 mp $a - ( ( t + 0 ) = t -> t = t ) 4,5,6,16 mp   $a - t = t 

"필수" 형식의 증명은 구문적인 세부사항을 생략하고 보다 전통적인 프레젠테이션을 남깁니다.

a2             $a - ( t + 0 ) = t a2             $a - ( t + 0 ) = t a1             $a - ( ( t + 0 ) = t -> ( ( t + 0 ) = t -> t = t ) ) 2,3 mp         $a - ( ( t + 0 ) = t -> t = t ) 1,4 mp         $a - t = t 

대체

단계별 증명

모든 메타패스 증명 단계는 하나의 치환 규칙을 사용합니다.이것은 변수를 식에 의한 단순한 치환일 뿐 술어 미적분에 관한 작업에서 기술된 적절한 치환이 아닙니다.이를 지원하는 메타매스 데이터베이스에서 적절한 대체는 메타매스 언어 자체에 내장된 것이 아니라 파생된 구성입니다.

대체 규칙은 사용 중인 논리 시스템에 대한 가정을 하지 않으며 변수의 대체가 올바르게 수행되어야만 합니다.

이 알고리즘의 동작의 상세한 예를 다음에 나타냅니다.정리 1단계와 2단계2p2e4메타패스 프루프 탐색기(set.mm)의 왼쪽이 표시되어 있습니다.메타마스가 대체 알고리즘을 사용하여 2단계가 1단계의 논리적 결과인지 확인하는 방법을 설명하자.opreq2i. 스텝 2는 (2 + 2) = (2 + (1 + 1)을 나타냅니다.그것은 정리된 결론이다.opreq2i.정리opreq2iA = B이면 (C F A) = (C F B)임을 나타냅니다.이 정리는 교과서에서는 결코 이 수수께끼 같은 형태로 나타나지 않지만, 그것의 문맹스러운 공식은 진부하다: 두 양이 같을 때, 연산에서 하나는 다른 것으로 대체될 수 있다.Metamath가 (C F A) = (C F B)와 (2 + 2) = (2 + (1 + 1)의 통합을 시도하는 증명 확인.이를 위해서는 C를 2, F를 +, A를 2 및 B를 (1 + 1)로 통합하는 방법밖에 없습니다.그래서 메타마스는 다음과 같은 전제를 사용한다.opreq2i이 전제는 A = B라고 한다.이전 계산 결과 메타마스는 A를 2로, B를 (1 + 1)로 치환해야 한다는 것을 알고 있습니다.전제 A = B는 2=(1+1)가 되므로 스텝1이 생성됩니다.다음으로 스텝 1은 다음과 같이 통합됩니다.df-2.df-2번호의 정의입니다.2라고 기술하고 있습니다.2 = ( 1 + 1 )여기서 통일은 단순히 상수의 문제이고 간단하다(대체할 변수의 문제는 없다).이것으로 검증이 완료되어 다음 두 단계의 검증이 완료됩니다.2p2e4정답입니다.

메타마스가 (2 + 2)를 B와 통합하는 경우 구문 규칙이 존중되는지 확인해야 합니다.사실 B는 그런 타입을 가지고 있다.class따라서 Metamath는 (2 + 2)도 입력되었는지 확인해야 합니다.class.

메타패스 프루프 체커

메타매스 프로그램은 메타매스 언어를 사용하여 작성된 데이터베이스를 조작하기 위해 만들어진 원본 프로그램입니다.텍스트(명령줄) 인터페이스가 있으며 C로 기술되어 있습니다.Metamath 데이터베이스를 메모리에 읽고, 데이터베이스의 증명을 확인하고, 데이터베이스를 수정하고(특히 증빙을 추가하여), 스토리지에 다시 쓸 수 있습니다.

사용자가 증명을 입력할 수 있는 증명 명령과 기존 증명을 검색하는 메커니즘이 있습니다.

Metamath 프로그램은 문장을 HTML 또는 TeX 표기로 변환할 수 있습니다.예를 들어 다음과 같이 set.mm에서 modus ponens 공리를 출력할 수 있습니다.

$\displaystyle \vdash \vdash \&\quad \vdash (\varphi \rightarrow \psi )\quad \rightarrow \quad \vdash \psi }$

많은 다른 프로그램들이 메타매스 데이터베이스를 처리할 수 있으며, 특히 메타매스 ^[9]형식을 사용하는 데이터베이스에 대한 증명 검증자는 최소 17개입니다.

메타패스 데이터베이스

메타매스 웹사이트는 다양한 공리 시스템에서 파생된 정리들을 저장하는 여러 데이터베이스를 호스팅합니다.대부분의 데이터베이스(.mm 파일)에는 "익스플로러"라고 불리는 관련 인터페이스가 있으며, 이를 통해 웹 사이트에서 대화식으로 진술과 증거를 탐색할 수 있습니다.대부분의 데이터베이스는 힐베르트 형식 추리 시스템을 사용하지만, 이는 요건이 아닙니다.

메타패스 프루프 익스플로러

메타패스 프루프 익스플로러

메타매스 프루프 탐험가의 증거
사이트 유형	온라인 백과사전
본사	미국
주인	노먼 메길
작성자	노먼 메길
URL	us.metamath.org/mpeuni/mmset.html
상업의	아니요.
등록.	아니요.

메타매스 프루프 탐색기(set.mm에 수록)는 주요 데이터베이스이자 가장 큰 데이터베이스이며, 2019년 7월 현재 주요 부분에는 23,000개 이상의 프루프가 있다.이는 고전적인 1차 논리와 ZFC 집합론을 기반으로 한다(예: 범주 이론에서 필요할 때 Tarski-Grothendieck 집합론을 추가).데이터베이스는 20년 이상 유지되어 왔다(set.mm의 첫 번째 증거는 1993년 8월).데이터베이스는 다른 분야들 중에서 집합 이론의 발전(호수와 기수, 재귀, 선택 공리의 등가물, 연속체 가설 등가물, 순서 이론, 그래프 이론, 추상 대수, 선형 대수, 일반 위상, 실복소 해석, 힐베르트 공간)을 포함한다.s, 수 이론, 그리고 초등 기하학.이 데이터베이스는 Norman Megill에 의해 처음 작성되었지만, 2019-10-04년 현재 48명의 기여자(Norman Megill ^[10]포함)가 있다.

메타매스 프루프 탐색기는 메타매스와 ^[11]함께 사용할 수 있는 많은 교과서들을 참조합니다.따라서 수학 공부에 관심이 있는 사람들은 메타마스를 이 책들과 연계하여 사용할 수 있고 증명된 주장들이 문헌과 일치하는지 확인할 수 있다.

직관 논리 탐색기

이 데이터베이스는 직관적 논리의 공리로부터 시작하여 건설적 집합론의 공리 체계로 이어지는 건설적 관점에서 수학을 발전시킨다.

새 기초 탐색기

이 데이터베이스는 Quine의 New Foundations 집합 이론에서 수학을 발전시킵니다.

고차 논리 탐색기

이 데이터베이스는 고차 로직에서 시작하여 1차 로직 및 ZFC 집합론의 공리와 동등한 값을 도출합니다.

탐색기 없는 데이터베이스

메타매스 웹사이트는 탐험가와 관련이 없지만 주목할 만한 몇 가지 다른 데이터베이스를 제공합니다.Robert Solovay가 작성한 데이터베이스 peano.mm는 Peano 산술을 공식화합니다.데이터베이스 nat^[12].mm은 자연 연산을 공식화합니다.데이터베이스 miu.mm는 Gödel, Escher, Bach에서 제시된 공식 시스템 MIU를 기반으로 MU 퍼즐을 공식화합니다.

나이 든 탐험가

메타매스 홈페이지에는 현재 메타매스 프루프 탐색기에 병합된 힐베르트 우주 이론과 관련된 이론을 제시하는 힐베르트 우주 탐색기와 직교 이론에서 출발하는 양자 논리 탐색기 등 더 이상 유지되지 않는 몇 가지 오래된 데이터베이스도 있다.격자

자연공제

메타마스는 증명(즉 추론 규칙에 의해 연결된 공식의 나무)에 대한 매우 일반적인 개념을 가지고 있고 소프트웨어에 특정한 논리가 포함되어 있지 않기 때문에 메타마스는 힐버트 스타일의 논리학이나 시퀀트 기반 논리학처럼 다른 종류의 논리학이나 람다 미적분학에도 사용될 수 있습니다.

그러나 메타마스는 자연감점 시스템을 직접 지원하지 않습니다.앞서 기술한 바와 같이 데이터베이스 nat.mm은 자연감소를 공식화하고 있습니다.Metamath Proof Explorer(데이터베이스 set.mm)는 대신 Hilbert 스타일의 논리 내에서 자연스러운 추론 접근법을 사용할 수 있는 일련의 규약을 사용합니다.

메타매스와 관련된 기타 작품

프루프 체커

Metamath에서 구현된 디자인 아이디어를 사용하여 Raph Levien은 Python 코드 500줄에 매우 작은 프루프 체커(mmverify.py)를 구현했습니다.

길버트(Ghilbert)^[13]는 mmverify.py에 기반한 유사하지만 보다 정교한 언어입니다.Levien은 여러 사람이 협업할 수 있는 시스템을 구현하고 싶어 하며, 그의 작업은 모듈화와 작은 이론 간의 연결을 강조하고 있다.

Levien의 주요 작품을 사용하여 메타매스 설계 원리의 많은 다른 구현이 다양한 언어에 대해 구현되어 왔다.Juha Arpiainen은 Common Lisp에 Bourbaki라고 불리는^[14] 자신의 교정기를 구현했고 Marnix Kloster는 Haskell에 교정기를 코드화했다.^[15]

이들은 모두 공식적인 시스템 체커 코딩에 전반적인 메타패스 접근법을 사용하지만, 그들만의 새로운 개념도 구현합니다.

에디터

Mel O'Cat은 ^[16]입증을 위한 그래픽 사용자 인터페이스를 제공하는 Mmj2라고 불리는 시스템을 설계했다.Mel O'Cat의 초기 목표는 사용자가 단순히 공식을 입력하고 Mmj2가 그것들을 연결하기 위한 적절한 추론 규칙을 찾도록 함으로써 증거를 입력할 수 있도록 하는 것이었다.반대로 메타패스에서는 정리명만 입력할 수 있습니다.수식을 직접 입력할 수 없습니다.Mmj2에는 프루프를 앞으로 또는 뒤로 입력할 수도 있습니다(메타매스는 프루프를 뒤로만 입력할 수 있습니다).게다가 Mmj2는 (메타매스와는 달리) 진짜 문법 파서를 가지고 있다.이러한 기술적 차이는 사용자에게 더 편안함을 가져다 줍니다.특히 메타마스는 분석되는 여러 공식(대부분 무의미함) 사이에서 망설이며 사용자에게 선택을 요구한다.Mmj2에서는 이 제한이 더 이상 존재하지 않습니다.

Mmide라고 불리는 메타매스에 그래픽 사용자 인터페이스를 추가하는 William ^[17]Hale의 프로젝트도 있다.Paul Chapman은 치환 전후에 참조된 정리를 볼 수 있는 강조 표시가 있는 새로운 증명 브라우저를 개발하고 있습니다.

Milpgame은 Filip Cernatescu가 작성한 Metamath 언어(set.mm)용 그래픽 사용자 인터페이스를 갖춘 증명 도우미 및 검사기이며, 오픈 소스(MIT 라이센스) Java 애플리케이션(크로스 플랫폼 애플리케이션:Window, Linux, Mac OS).시연(증명)을 2가지 모드로 입력할 수 있습니다.증명할 스테이트먼트에 상대적인 순방향 모드와 역방향 모드입니다.Milpgame은 문장의 형식이 올바른지 확인합니다(통사적 검증자가 있음).더미링크 정리를 사용하지 않고도 완료되지 않은 증거를 저장할 수 있습니다.시연은 트리로 표시되고 문장은 html 정의(조형 장에서 정의)를 사용하여 표시됩니다.Milpgame은 Java .jar(NetBeans IDE로 작성된 JRE 버전6 업데이트 24)로 배포됩니다.

「 」를 참조해 주세요.

• 자동화된 증명 확인
• 프루프 어시스턴트

레퍼런스

외부 링크

• 메타매스: 공식 웹사이트.
• 수학자들은 메타매스에 대해 어떻게 생각하는가: 메타매스에 대한 의견.