나는 Russell ‘s Principia Mathematica (PM)와 논리적 실증주의에서 영감을 얻은 책을 소유하고있다. 공리를 결정하고 그것들로부터 이론을 추론함으로써 특정 영역을 공식화하려고 시도한다. 요컨대, PM이 수학을 위해 시도한 것을 그 영역을 위해 시도합니다. PM과 마찬가지로 자동 정리 증명 (ATP)이 가능하기 전에 작성되었습니다.

나는 현대의 ATP 시스템에서 이러한 공리를 표현하려고 노력하고 있으며, 처음에는 저자가 직접 추론 한 이론을 추론하려고 시도한다. 나는 이전에 ATP 시스템을 사용하지 않았으며 각각의 강점, 약점 및 의도 된 응용 프로그램과 함께 다양한 옵션 (HOL, Coq, Isabelle 등)을 감안할 때 내 특정에 적합한 것을 결정하는 것이 어렵다는 것을 증명합니다 목적.

저자의 형식주의는 PM을 반영한다. 클래스 (세트?), 클래스 클래스 등 최대 6 단계의 계층 구조가 있습니다. 1 차, 아마도 더 높은 차수가 있습니다. PM과의 관계를 고려할 때, PM에 대한 몇 가지 이론이 다른 사람들에 의해 MetaMath에서 입증 되었기 때문에 Metamath를 처음 조사했습니다. 그러나 Metamath는 물론 ATP 시스템이 아닌 증명 검증기입니다.

다양한 ATP 시스템에 대한 설명을 통해 교회 유형 이론, 건설적 유형 이론, 직관 론적 유형 이론, 유형 / 비 유형 집합 이론, 자연적 추론, 람다 미적분학 유형, 다형성, 재귀 함수 이론, 평등의 존재. 요컨대, 각 시스템은 매우 다른 언어를 구현하는 것으로 보이며 다른 것을 공식화하는 데 적합해야합니다. 수학 공식화를위한 기존 라이브러리는 내 목적과 관련이 없다고 가정합니다.

ATP를 선택할 때 고려해야 할 특성이 나이 질문을 읽은 후에 할 수있는 다른 조언에 대한 조언은 대단히 감사하겠습니다. 참고로 여기 책의 샘플 페이지가 있습니다. 불행히도 PM과 마찬가지로 Peano-Russell 표기법입니다.

그 책 –

“생물학의 공리 학적 방법”(1937), JH Woodger, A. Tarski, WF Floyd

공리는 단순한 것으로 시작합니다. 예를 들어

x

x

α

α

α

α

x

x

y

y

x

x

z

z

α

α

y

y

S=Dfx^α^{α⊂P‘→x:.(y):yPx.⊃.(∃z).z∈α.P‘→y∩P‘→z≠Λ} S=Dfx^α^{α⊂P‘→x:.(y):yPx.⊃.(∃z).z∈α.P‘→y∩P‘→z≠Λ}

다시, 이것은 Peano-Russell 표기법 (Principia의 표기법)입니다.

나중에 공리에는 생물학적 내용이 있습니다.

7.4.2 멘델 리안 클래스의 두 멤버의 게임이 쌍으로 결합하여 접합자를 형성 할 때, 주어진 쌍 결합의 확률은 다른 쌍의 확률과 동일합니다.

이것은 내가 이해 한 바에 따르면 멘델의 유전학에 대한 가정이었습니다.

3 줄 길이이고 이전에 정의 된 내용을 기반으로하기 때문에이 표기법을 생략합니다.

정리의 예-

이것은 멘델의 유전학에서 의미있는 해석을하는 것으로 보인다. 생물학의 역사학자는 아니지만 나는 이해할 수 없다. 이 책에서는 손으로 추론했습니다.

감사!

답변