형식 체계
"오늘의AI위키"의 AI를 통해 더욱 풍부하고 폭넓은 지식 경험을 누리세요.
1. 개요
형식 체계는 형식 언어와 연역 시스템으로 구성되며, 형식 언어는 기호의 문자열인 잘 구성된 공식의 집합으로 정의된다. 연역 시스템은 공리와 추론 규칙을 통해 정리를 유도하며, 형식 체계는 재귀 집합 또는 재귀적으로 열거 가능할 수 있다. 형식 언어는 구문론과 의미론을 가지며, 형식 문법은 생성 문법과 분석 문법으로 분류된다. 형식 체계는 소프트웨어, 하드웨어 검증, 논리적 추론, 자연어 처리 등 다양한 분야에 응용된다. 연역 시스템은 공리와 추론 규칙으로 구성되며, 형식적 증명을 통해 정리(theorem)를 이끌어낸다. 형식적 증명은 일련의 잘 정의된 공식으로, 공리 또는 추론 규칙을 적용한 결과이며, 형식주의는 형식적 증명을 수학의 전부로 보는 관점이다. 형식 논리 체계는 고대부터 발전해 왔으며, 조지 불, 고틀로프 프레게 등의 기여로 근대 수리 논리가 발전했다. 힐베르트의 프로그램은 괴델의 불완전성 정리로 인해 제동이 걸렸다.
더 읽어볼만한 페이지
- 형식 체계 - 추론 규칙
추론 규칙은 전제가 참일 때 결론이 필연적으로 참임을 보이는 논리적 도출 과정을 형식적으로 표현한 규칙으로, 다양한 유형이 존재하며 명제 논리와 술어 논리에서 기본적인 추론을 수행하는 데 사용되고, 형식 체계의 핵심 요소이다. - 형식 체계 - 제일원리
제일원리는 철학, 형식 논리학, 자연과학 등에서 근본 원리 또는 가장 기본적인 법칙을 의미하며, 철학에서는 근본 원인에 대한 접근 방식, 형식 논리학에서는 다른 명제를 연역해낼 수 있는 공리, 자연과학에서는 확립된 물리 법칙으로부터 직접 계산하는 방식을 나타낸다. - 수학기초론 - 힐베르트 프로그램
힐베르트 프로그램은 20세기 초 수학의 기초를 형식 체계로 구축하고 무모순성과 완전성을 증명하려 했으나, 괴델의 불완전성 정리에 의해 원래 목표 달성이 불가능해졌고 수정된 형태로 연구가 지속되고 있다. - 수학기초론 - 폰 노이만-베르나이스-괴델 집합론
폰 노이만-베르나이스-괴델 집합론(NBG)은 집합과 모임 두 종류의 객체를 다루는 공리적 집합론으로, 모든 집합은 모임이 되며, 집합론적 역설을 피하고 모임을 다루면서 ZFC의 보존적 확장이자 유한 공리화 가능 이론이고 클래스 개념을 통해 ZFC보다 강력한 선택 공리를 허용한다. - 정형 기법 - 자동 정리 증명
자동 정리 증명은 논리적 진술의 타당성을 자동으로 확인하는 기술로서, 형식 논리 발전과 컴퓨터 등장 이후 다양한 논리를 지원하며 여러 분야에 응용되고, 관련 연구와 시스템 개발이 활발히 진행되고 있다. - 정형 기법 - 튜링 기계
튜링 기계는 앨런 튜링이 제시한 계산 모델로, 테이프 위에서 기계적으로 작동하며, 유한한 상태, 테이프, 헤드, 명령 표를 통해 작동하고, 계산 가능성과 알고리즘의 한계를 연구하는 데 사용된다.
| 형식 체계 | |
|---|---|
| 개요 | |
 | |
| 유형 | 형식 체계 |
| 연구 분야 | 논리학 수학 컴퓨터 과학 |
| 구성 요소 | |
| 알파벳 | 유한한 기호 집합 |
| 형식 언어 | 알파벳 기호에서 구성된 문자열 집합 |
| 추론 규칙 | 형식 언어의 문자열을 변환하는 규칙 집합 |
| 공리 | 초기점으로 제공되는 형식 언어의 문자열 집합 |
| 응용 | |
| 수학적 기초 | 수학적 주장을 공식화하고 증명 |
| 컴퓨터 과학 | 프로그래밍 언어 의미론 정의 |
| 관련 개념 | |
| 형식 문법 | 문자열 집합을 생성하기 위한 규칙 |
| 형식 증명 | 공리에서 결론까지의 추론 규칙의 적용 순서 |
| 해석 | 형식 체계의 기호와 문장에 의미를 부여 |
2. 개념
형식 체계는 형식 언어와 연역 시스템으로 구성된다.[3][4][5]
- 형식 언어: 알파벳에서 온 기호의 문자열인 잘 구성된 공식의 집합으로, 형식 문법(생성 규칙 또는 형성 규칙으로 구성됨)에 의해 형성된다.
- 연역 시스템: 추론 규칙이 있어 공리를 가져와 정리를 추론하며, 이 둘 다 형식 언어의 일부인 증명 시스템이다.
형식 체계는 공리 집합과 추론 규칙 집합이 각각 결정 가능 집합 또는 반결정 가능 집합인 경우 재귀 집합 (즉, 효과적) 또는 재귀적으로 열거 가능하다고 한다.
2. 1. 형식 언어
형식 언어는 형식 체계에 의해 정의되는 언어이다. 언어학의 언어와 마찬가지로 형식 언어는 일반적으로 구문론과 의미론 두 가지 측면을 갖는다.- 구문론: 언어가 어떻게 보이는지에 대한 것으로, 언어에서 유효한 발화가 될 수 있는 가능한 표현의 집합이다.
- 의미론: 언어의 발화가 의미하는 바를 나타내며, 문제의 언어 유형에 따라 다양한 방식으로 형식화된다.
일반적으로 형식 언어의 구문론은 형식 문법의 개념을 통해 고려된다. 형식 문법의 두 가지 주요 범주는 언어의 문자열이 작성될 수 있는 규칙 집합인 생성 문법과 문자열이 언어의 구성원인지 여부를 결정하기 위해 분석될 수 있는 규칙 집합인 분석 문법이다.[6][7]
2. 1. 1. 핵심 개념
형식 체계는 다음을 갖는다:[3][4][5]
- 형식 언어: 알파벳에서 온 기호의 문자열인 잘 구성된 공식의 집합으로, 형식 문법(생성 규칙 또는 형성 규칙으로 구성됨)에 의해 형성된다.
- 연역 시스템: 추론 규칙이 있어 공리를 가져와 정리를 추론하며, 이 둘 다 형식 언어의 일부인 증명 시스템이다.
형식 체계는 공리 집합과 추론 규칙 집합이 각각 결정 가능 집합 또는 반결정 가능 집합인 경우 재귀 집합 (즉, 효과적) 또는 재귀적으로 열거 가능하다고 한다.
형식 언어는 형식 체계에 의해 정의되는 언어이다. 언어학의 언어와 마찬가지로 형식 언어는 일반적으로 두 가지 측면을 갖는다.
- 구문론: 언어가 어떻게 보이는지 (더 형식적으로는, 언어에서 유효한 발화가 될 수 있는 가능한 표현의 집합)이다.
- 의미론: 언어의 발화가 의미하는 바를 나타낸다 (이는 문제의 언어 유형에 따라 다양한 방식으로 형식화된다).
일반적으로 형식 언어의 구문론만 형식 문법의 개념을 통해 고려된다. 형식 문법의 두 가지 주요 범주는 언어의 문자열이 작성될 수 있는 규칙 집합인 생성 문법과 문자열이 언어의 구성원인지 여부를 결정하기 위해 분석될 수 있는 규칙 집합인 분석 문법이다.[6][7]
2. 1. 2. 응용 분야
2. 2. 연역 시스템
'''연역 시스템'''은 '''연역적 장치'''라고도 하며, 공리 (또는 공리 체계)와 형식적 증명을 통해 정리를 유도하는 데 사용되는 추론 규칙으로 구성된다.[8]이러한 연역 시스템은 시스템에서 표현되는 수식에서 연역적 추론의 성질을 보존한다. 일반적으로 보존되는 성질은 진실이며, 정당성이나 신념과 같은 다른 양상이 대신 보존될 수도 있다.
연역적 완전성을 유지하기 위해, ''연역적 장치''는 언어의 의도된 해석에 대한 참조 없이 정의되어야 한다. 이는 유도의 각 줄이 그 앞에 있는 줄의 논리적 결과일 뿐임을 보장하기 위해서이다.
시스템의 논리적 기초에 의한 논리적 결과 (또는 함의)는 추상적 모델에 기초를 둔 다른 형식 시스템과 구별되는 특징이다. 종종 형식 시스템은 더 큰 이론이나 분야 (예: 유클리드 기하학)의 기반이 되거나, 현대 수학 (예: 모형 이론)에서 사용되는 것과 일치하는 것으로 간주된다.
연역 시스템의 예로는 1차 논리에서 사용되는 추론 규칙과 동등성에 관한 공리가 있다.
2. 2. 1. 증명 시스템
형식적 증명은 잘 정의된 공식 (WFF)의 나열이다. 증명을 구성하는 정식은 공리이거나, 증명 내 앞선 정식에 추론 규칙을 적용하여 도출된 것이다. 나열된 정식 중 마지막 정식이 정리로 인식된다.형식 체계가 주어지면, 형식 체계 내에서 증명할 수 있는 정리 집합을 정의할 수 있다. 이 집합은 증명이 있는 모든 WFF로 구성된다. 따라서 모든 공리는 정리로 간주된다. WFF의 문법과 달리, 주어진 WFF가 정리인지 여부를 결정하는 결정 절차가 있을 것이라는 보장은 없다.
형식적 증명을 생성하는 것이 수학의 전부라는 관점을 흔히 ''형식주의''라고 한다. 다비트 힐베르트는 형식 체계를 논의하기 위한 학문으로서 메타수학을 창시했다. 형식 체계에 대해 이야기하는 데 사용하는 모든 언어를 ''메타언어''라고 한다. 메타언어는 자연어일 수도 있고 부분적으로 형식화될 수도 있지만, 일반적으로 검토 중인 형식 체계의 형식 언어 구성 요소보다 덜 완전히 형식화되어 있으며, 이를 ''객체 언어'', 즉 문제에 대한 논의의 대상이라고 한다. 방금 정의한 ''정리''의 개념은 혼동을 피하기 위해 일반적으로 메타정리라고 하는 ''형식 체계에 대한 정리''와 혼동해서는 안 된다.
2. 2. 2. 논리 체계의 형식적 의미론
모형 이론에 따르면, 논리 체계는 주어진 구조가 잘 구성된 공식을 만족하는지 여부를 설명하는 해석이 주어질 수 있다. 형식 체계의 모든 공리를 만족하는 구조는 논리 체계의 모형으로 알려져 있다.논리 체계는 다음과 같은 특성을 가질 수 있다.
- 건전성: 공리로부터 추론될 수 있는 각 잘 구성된 공식이 논리 체계의 모든 모형에 의해 만족되는 경우를 말한다.
- 의미적 완전성: 논리 체계의 모든 모형에 의해 만족되는 각 잘 구성된 공식이 공리로부터 추론될 수 있는 경우를 말한다.
논리 체계의 예로는 페아노 산술이 있다. 산술의 표준 모형은 담화 영역을 음이 아닌 정수로 설정하고 기호에 일반적인 의미를 부여한다.[10] 또한 비표준 산술 모형도 존재한다.
논리 체계는 일종의 의미론(통상, 모형 이론적 해석의 형태)을 동반한 형식 체계로, 자유 변수를 포함하지 않는 논리식(문)에 진리값을 할당한다. 어떤 논리가 건전하다는 것은, 도출되는 모든 문이 참으로 해석된다는 것을 의미하며, 어떤 논리가 완전하다는 것은, 반대로 모든 참인 문을 도출할 수 있다는 것을 의미한다.
3. 관련 주제
논리 체계는 추론 체계와 비논리적 공리를 묶은 것이며, 모형 이론에 따라 해석이 주어질 수 있다. 페아노 산술은 논리 체계의 한 예시이며, 음이 아닌 정수를 담화 영역으로 하는 표준 모형과 비표준 산술 모형이 존재한다. 논리는 형식 체계에 진리값을 할당하는 의미론을 동반하며, 건전성과 완전성을 갖는다.
형식적 증명은 잘 정의된 공식(WFF)들의 나열이며, 마지막 공식은 정리로 간주된다. 다비트 힐베르트는 형식 체계를 연구하는 메타수학을 창시했으며, 형식 체계에 대해 논할 때 사용되는 언어를 ''메타언어''라고 한다.
3. 1. 논리 체계
논리 체계는 추론 체계 (가장 흔하게는 일계 논리)와 추가적인 비논리적 공리를 함께 묶은 것이다.[9] 모형 이론에 따르면, 논리 체계는 주어진 구조 (특정 의미로의 공식 매핑)가 잘 구성된 공식을 만족하는지 여부를 설명하는 해석이 주어질 수 있다. 형식 체계의 모든 공리를 만족하는 구조는 논리 체계의 모형으로 알려져 있다.논리 체계는 다음과 같은 특성을 가질 수 있다.
| 특성 | 설명 |
|---|---|
| 건전성 | 공리로부터 추론될 수 있는 각 잘 구성된 공식이 논리 체계의 모든 모형에 의해 만족되는 경우 |
| 의미적 완전성 | 논리 체계의 모든 모형에 의해 만족되는 각 잘 구성된 공식이 공리로부터 추론될 수 있는 경우 |
페아노 산술은 논리 체계의 한 예이다. 산술의 표준 모형은 담화 영역을 음이 아닌 정수로 설정하고 기호에 일반적인 의미를 부여한다.[10] 비표준 산술 모형도 존재한다.
논리 체계 또는 논리는 일종의 의미론 (통상, 모형 이론적 해석의 형태)을 동반한 형식 체계로, 형식 언어의 문 (자유 변수를 포함하지 않는 논리식)에 진리값을 할당한다. 어떤 논리가 건전하다는 것은 도출되는 모든 문이 참으로 해석된다는 것을 의미하며, 어떤 논리가 완전하다는 것은 반대로 모든 참인 문을 도출할 수 있다는 것을 의미한다.
3. 2. 형식적 증명
형식적 증명은 일련의 잘 정의된 공식(WFF)으로, 공리이거나 증명 시퀀스에서 이전 WFF에 추론 규칙을 적용한 결과일 수 있다.[3][4][5] 시퀀스의 마지막 WFF는 정리로 인식된다.
형식 체계가 주어지면 형식 체계 내에서 증명할 수 있는 정리 집합을 정의할 수 있다. 이 집합은 증명이 있는 모든 WFF로 구성된다. 따라서 모든 공리는 정리로 간주된다. WFF의 문법과 달리, 주어진 WFF가 정리인지 여부를 결정하는 결정 절차가 있을 것이라는 보장은 없다.
형식적 증명을 생성하는 것이 수학의 전부라는 관점을 흔히 ''형식주의''라고 한다. 다비트 힐베르트는 형식 체계를 논의하기 위한 학문으로서 메타수학을 창시했다. 형식 체계에 대해 이야기하는 데 사용하는 모든 언어를 ''메타언어''라고 한다. 메타언어는 자연어일 수도 있고 부분적으로 형식화될 수도 있지만, 일반적으로 검토 중인 형식 체계의 형식 언어 구성 요소보다 덜 완전히 형식화되어 있으며, 이를 ''객체 언어'', 즉 문제에 대한 논의의 대상이라고 한다. 방금 정의한 ''정리''의 개념은 혼동을 피하기 위해 일반적으로 ''메타정리''라고 하는 ''형식 체계에 대한 정리''와 혼동해서는 안 된다.
4. 역사
파니니의 인도 논리, 아리스토텔레스의 삼단 논리, 스토아 철학의 명제 논리, 공손룡(기원전 325–250년경)의 중국 논리가 초기 논리 체계에 해당한다. 더 최근에는 조지 불, 오거스터스 드 모르간, 고틀로프 프레게가 형식 논리 체계 발전에 기여했다. 수리 논리는 19세기 유럽에서 발전했다.
다비트 힐베르트는 힐베르트의 프로그램이라고 불리는 형식주의 운동을 주도했는데, 이는 수학 기초의 위기에 대한 해결책으로 제안되었으나 괴델의 불완전성 정리에 의해 완화되었다.[2] QED 선언은 알려진 수학의 형식화를 위한 후속 노력이었으나 아직 성공하지 못했다.
참조
[1]
백과사전
Formal system
https://www.britanni[...]
2012-01-06
[2]
서적
Hilbert's Program, Stanford Encyclopedia of Philosophy
Metaphysics Research Lab, Stanford University
2003-07-31
[3]
PlanetMath
Formal System
[4]
웹사이트
Syntax & Semantics of Formal Systems
https://cse.buffalo.[...]
2010-03-25
[5]
ProofWiki
[6]
사전
Reductive grammar
http://encyclopedia2[...]
McGraw-Hill
[7]
웹사이트
A Tree Meta for the XDS 940
http://bitsavers.inf[...]
Augmentation Research Center
2024-11-30
[8]
ProofWiki
Deductive Apparatus
2024-11-30
[9]
서적
Formal Semantics and Logic
https://www.princeto[...]
Nousoul Digital Publishers
[10]
서적
Models of Peano arithmetic
Clarendon Press
1991
[11]
뉴스
Formal system definition
http://www.britannic[...]
Encyclopædia Britannica
2007
본 사이트는 AI가 위키백과와 뉴스 기사,정부 간행물,학술 논문등을 바탕으로 정보를 가공하여 제공하는 백과사전형 서비스입니다.
모든 문서는 AI에 의해 자동 생성되며, CC BY-SA 4.0 라이선스에 따라 이용할 수 있습니다.
하지만, 위키백과나 뉴스 기사 자체에 오류, 부정확한 정보, 또는 가짜 뉴스가 포함될 수 있으며, AI는 이러한 내용을 완벽하게 걸러내지 못할 수 있습니다.
따라서 제공되는 정보에 일부 오류나 편향이 있을 수 있으므로, 중요한 정보는 반드시 다른 출처를 통해 교차 검증하시기 바랍니다.
문의하기 : help@durumis.com