정식 시스템

Formal system

형식 시스템은 일련의 규칙에 따라 공리로부터 이론들을 추론하는 데 사용되는 추상적인 구조이다.공리로부터 정리의 추론을 실시하기 위해서 사용되는 이러한 규칙들은 형식 시스템의 논리 미적분이다.공식 시스템은 본질적으로 "축체 시스템"[1]입니다.

1921년, 데이비드 힐버트는 수학 [2]지식을 위한 기초로서 그러한 시스템을 사용할 것을 제안했다.형식적인 시스템은 잘 정의된 추상적 사고의 체계를 나타낼 수 있다.

형식주의라는 용어는 때때로 형식 체계와 대략적인 동의어이지만, 폴 디락의 브라-케트 표기법과 같은 주어진 표기 스타일을 가리키기도 한다.

배경

각 형식 시스템은 원시 기호(집합적으로 알파벳을 형성하는 것)를 사용하여 일련의 공리로부터 유추적 형성 규칙을 통해 형식 언어를 완성합니다.

따라서 시스템은 명시된 [3]규칙에 따라 공리에서 형성되는 기본 기호의 유한한 조합을 통해 구축된 유효한 공식으로 구성됩니다.

더 공식적으로, 이것은 다음과 같이 표현될 수 있습니다.

  1. 알파벳으로 알려진 유한한 기호 집합. 수식을 연결하기 때문에 공식은 알파벳에서 가져온 유한한 기호 문자열일 뿐입니다.
  2. 단순한 공식에서 공식을 형성하는 규칙으로 구성된 문법입니다.공식은 형식 문법의 규칙을 이용하여 만들어질 수 있다면 잘 만들어진다고 한다.종종 공식이 잘 형성되었는지 여부를 결정하기 위한 결정 절차가 필요합니다.
  3. 올바른 공식으로 구성된 일련의 공리 또는 공리 스키마타입니다.
  4. 추론 규칙 세트입니다.공리로부터 추론할 수 있는 잘 형성된 공식을 형식 시스템의 정리라고 한다.

재귀적

공식 시스템은 공리 집합 및 추론 규칙 집합이 각각 결정 가능한 집합 또는 반결정 가능한 집합일 경우 재귀적(즉 유효) 또는 재귀적으로 열거할 수 있다고 한다.

추론 및 수반

논리적 기반에 의한 시스템의 수반은 추상적 모델에서 어느 정도 근거를 가질 수 있는 형식적 시스템과 다른 시스템을 구별하는 것입니다.종종 형식 시스템은 모델 [clarification needed]이론과 같은 현대 수학에서의 용도와 일치하는 더 큰 이론이나 분야(예: 유클리드 기하학)의 기초가 되거나 심지어 동일시 될 것이다.

격식어

주요 기사:형식 언어 및 형식 문법

공식 언어는 공식 시스템에 의해 정의된 언어입니다.언어학상의 언어와 마찬가지로 정식 언어에는 일반적으로 다음 두 가지 측면이 있습니다.

  • 언어의 구문은 그 언어가 어떻게 보이는가(좀 더 형식적으로: 그 언어에서 유효한 발언인 가능한 표현의 집합)이다.
  • 언어의 의미론은 언어의 발화가 의미하는 것이다(문제의 언어의 유형에 따라 다양한 방법으로 공식화된다).

컴퓨터 과학과 언어학에서는 보통 형식 문법의 개념을 통해 형식 언어의 구문만 고려됩니다.형식 문법은 형식 언어의 구문에 대한 정확한 설명입니다. 문자열 집합입니다.형식 문법의 두 가지 주요 범주는 언어의 문자열이 어떻게 생성될 수 있는지에 대한 규칙 집합인 생성 문법과 문자열이 언어의 구성원인지 결정하기 위해 어떻게 분석될 수 있는지에 대한 규칙 집합인 분석 문법의 [4][5]그것이다.간단히 말해, 분석 문법은 문자열이 집합의 멤버일 때 인식하는 방법을 기술하는 반면, 생성 문법은 집합의 문자열만 쓰는 방법을 기술합니다.

수학에서 정형언어는 보통 정형문법이 아니라 영어와 같은 자연어로 기술된다.논리 시스템은 연역 체계와 자연 언어 모두에 의해 정의됩니다.연역 시스템은 자연어로만 정의됩니다(아래 참조).

연역법

연역적 장치 또는 논리라고도 불리는 연역적 시스템은 시스템의 [6]이론을 도출하기 위해 사용될 수 있는 공리와 추론 규칙으로 구성됩니다.

이러한 연역적 시스템은 시스템에서 표현되는 공식에서 연역적 특성을 보존합니다.보통 우리가 걱정하는 품질은 거짓이 아니라 진실이다.그러나 정당성이나 신념과 같은 다른 양식은 대신 보존될 수 있습니다.

연역적 무결성을 유지하기 위해 연역적 장치는 언어의 어떠한 의도된 해석도 참조하지 않고 정의할 수 있어야 한다.그 목적은 파생된 각 행이 그 앞에 있는 행의 구문적 결과일 뿐이라는 것을 확인하는 것이다.시스템의 연역적 성격과 관련된 언어의 해석 요소는 없어야 합니다.

연역 시스템의 예는 1차 술어 논리이다.

논리 시스템

논리 시스템 또는 언어(위에서 설명한 "형식 언어"의 종류와 혼동되지 않음)는 추가적인 (논리적이지 않은) 공리와 의미론과[disputed – discuss] 함께 연역 시스템(위의 섹션 참조; 가장 일반적으로 1차 술어 논리)이다.모델 이론 해석에 따르면 논리 시스템의 의미론은 주어진 구조에 의해 잘 형성된 공식이 충족되는지 여부를 기술한다.형식 시스템의 모든 공리를 만족시키는 구조를 논리 시스템의 모델이라고 합니다.논리시스템은 논리시스템의 모든 모델에 의해 공리로부터 추론할 수 있는 각각의 잘 형성된 공식이 충족된다면 건전하다.반대로 논리 시스템의 모든 모델에 의해 충족되는 각각의 잘 형성된 공식이 공리로부터 추론될 수 있다면 논리 시스템은 완전하다.

논리 시스템의 예로는 페아노 산술이 있습니다.

역사

초기 논리체계는 파니니의 인도 논리, 아리스토텔레스의 삼단논리, 스토이즘의 명제 논리, 공순롱(기원전 325년 경-250년)의 중국 논리학을 포함한다.좀 더 최근에는 조지 불, 아우구스투스 드 모건, 고틀롭 프레게 등이 있다.수학 논리는 19세기 유럽에서 발달했다.

형식주의

주요 기사:정식 논리 시스템

힐베르트 프로그램

주요 기사:힐베르트 프로그램

다비드 힐베르는 형식주의 운동을 선동했고 결국 괴델의 불완전성 이론으로 완화되었다.

QED 매니페스토

주요 기사: QED 매니페스토

QED 선언은 알려진 수학의 공식화에 대한 후속적인 노력을 나타내지만 아직 성공하지 못했다.

예

주요 기사:공식 시스템 목록

정식 시스템의 예는 다음과 같습니다.

변종

다음 시스템은 정식 시스템의[clarification needed] 변형입니다.

증명 시스템

주요 기사: 시스템 증명 및 공식 증명

형식 증명은 올바른 공식(또는 줄여서 wff)의 시퀀스입니다.wff가 증명의 일부로 인정되기 위해, 그것은 공리일 수도 있고 증명 시퀀스의 이전 wffs에 추론 규칙을 적용한 결과일 수도 있다.수열의 마지막 wff는 정리로 인식된다.

수학에 있어서 형식적인 증명을 만드는 것이 전부라는 관점은 종종 형식주의라고 불린다.David Hilbert는 형식적인 체계를 논하기 위한 학문으로 메타수학을 창시했다.형식적인 시스템에 대해 말할 때 사용하는 모든 언어를 메타언어라고 합니다.메타언어는 자연어일 수도 있고 부분적으로 형식화되어 있을 수도 있지만, 일반적으로 대상 언어, 즉 문제의 논의 대상으로 불리는 조사 대상 시스템의 형식 언어 구성 요소보다 덜 형식화되어 있습니다.

일단 정식 시스템이 주어지면, 정식 시스템 내에서 증명될 수 있는 일련의 정리를 정의할 수 있다.이 세트는 증거가 있는 모든 wffs로 구성됩니다.그러므로 모든 공리는 이론으로 간주된다.wffs의 문법과 달리, 주어진 wff가 정리인지 아닌지를 결정하는 절차가 있다는 보장은 없다.방금 정의된 정리의 개념은 혼동을 피하기 위해 보통 메타옴이라고 불리는 공식 시스템에 대한 이론과 혼동되어서는 안 된다.

「 」를 참조해 주세요.

레퍼런스

  1. ^ "Formal system, ENCYCLOPÆDIA BRITANNICA".
  2. ^ Zach, Richard (31 July 2003). "Hilbert's Program, Stanford Encyclopedia of Philosophy".
  3. ^ 브리태니커 백과사전, 공식 시스템 정의, 2007.
  4. ^ 환원문법: (컴퓨터 과학) 문자열이 언어 내에 존재하는지 여부를 판단하기 위한 일련의 구문 규칙."Sci-Tech Dictionary McGraw-Hill Dictionary of Scientific and Technical Terms" (6th ed.). McGraw-Hill.[unreliable source?] McGrow-Hill Encyclopedia of Science & Technology(뉴욕, 뉴욕) 편집자에 의해 편집된 저자에 대하여.이 문서는 과학 출판 분야의 최첨단 기술, 지식 및 혁신을 대표하는 사내 직원입니다.[1]
  5. ^ "포멀 언어 정의 컴파일러 쓰기 방식에는 두 가지 클래스가 있습니다.생산적인 문법 접근법이 가장 일반적이다.생산적인 문법은 언어의 가능한 모든 문자열을 생성하는 방법을 설명하는 일련의 규칙으로 구성됩니다.환원적 또는 분석적 문법 기법은 문자열을 분석하고 문자열이 언어에 있는지 여부를 결정하는 방법을 설명하는 일련의 규칙을 나타냅니다." "The TREE-META Compiler-Compiler System: A Meta Compiler System for the Univac 1108 and General Electric 645, University of Utah Technical Report RADC-TR-69-83. C. Stephen Carr, David A. Luther, Sherian Erdmann" (PDF). Retrieved 5 January 2015.
  6. ^ 헌터, 제프리, 메탈로직:캘리포니아 대학교 프레스의 1차 논리 표준 메타토리 소개, 1971년

추가 정보

외부 링크

무료 사전인 Wiktionary에서 형식화를 찾아보십시오.