논리 시스템에서 진술을 증명할 때 직관적 인 "메타"논리를 사용합니까, 아니면 시스템의 추론 규칙을 사용합니까?
나는 주제에 익숙하지 않지만 현재 명제 및 술어 논리에 대한 강의 노트를 읽고 있습니다. 저는 특히 논리와 언어의 경계에 관심이 있습니다. 여기에 언급 한 내용 중 일부가 잘못된 경우 수정하십시오.
사람은 상상할 수있는 세상의 모든 것에 대한 진술을 할 수 있으며,이 진술 (어떤 언어로 된 진술이든)은 참이거나 거짓 일 수 있습니다 (또는 그 사이에 가능한 어떤 것). 다른 진술이 이미 사실이라면 우리는 언어로 할 수있는 일부 진술의 타당성에 대해 직관적으로 이해하고 있습니다.
All cats live on earth.
Simon is a cat.
THEREFOR Simon lives on earth.
나는 문장의 타당성을 결정하는이 과정을 공식화하는 논리 시스템을 이해합니다 (고양이 또는 여러 가지를 설명하는 것과 상관없이). 여기에서 내가 틀렸다면 저를 바로 잡으십시오.
AFAIK는 논리 시스템을 "발명"할 때 몇 가지 정의를 기록합니다 (예를 들어 논리 기호, 술어 또는 공식과 같은 특정 객체가 어떻게 호출되는지 또는 그 구조가 무엇인지). 정의는 무언가를 부르는 방법에 대한 합의 일 뿐이 기 때문에 이것은 나에게 좋습니다. 내 뇌는 내가 인식하는 사물을 내가 부르고 싶은 방식으로 부르는 세상에서 살기에 충분히 강력합니다.)
다음으로, 이전 문장에서 진실과 거짓이 어떻게 뒤 따르는 지 적습니다 . 나의 현재 이해는 또한 이러한 규칙을 가정해야한다는 것입니다. 그것들은 어떤 메타 언어 나 원칙에서도 추론 될 수 없습니다. 하나는 단순히 어딘가에서 시작해야합니다. 맞습니까?
이 시점에서 내가 만난 대부분의 강의 노트는 건전성, 완전성 또는 일관성과 같은 것, 구문론과 의미 론적 진실의 동등성에 대해 이야기하기 시작합니다. 그리고 그들은 논리 시스템에 대한 결론을 내리기 시작합니다.
내 질문은 다음과 같습니다. 논리 시스템의 정의 나 추론 규칙 중 하나가 아닌 논리 시스템의 진술에 대해 논리 시스템의 추론 규칙 만 사용하여 증명해야합니까? 그것을 증명하기 위해 어떤 종류의 직관적 인 메타 로직 (제가 처음에 이야기했던 것)을 사용합니까?
답변
나는 문장의 타당성을 결정하는이 과정을 공식화하는 논리 시스템을 이해합니다 (고양이 또는 여러 가지를 설명하는 것과 상관없이). 여기에서 내가 틀렸다면 저를 바로 잡으십시오.
당신이 올바른지. 특히 공식 시스템은 추론 할 수있는 문장을 규정 할뿐입니다. 시스템은 기호 나 문장에 어떤 의미도 부여하지 않습니다. 추론 할 수있는 것을 알려줍니다. 그들에게 어떤 의미를 부여하고 싶다면 물론 그 시스템 내부에서 그렇게 할 수는 없지만 외부에서해야합니다. 힐베르트 스타일 시스템에서 추론 할 수있는 문장은 modus-ponens 규칙과 공리를 사용하여 규정됩니다. 다른 형식 시스템 (예 : Fitch 스타일 시스템)에는 다른 종류의 추론 규칙이 있습니다.
AFAIK는 논리 시스템을 "발명"할 때 몇 가지 정의를 기록합니다 (예를 들어 논리 기호, 술어 또는 공식과 같은 특정 객체가 어떻게 호출되는지 또는 그 구조가 무엇인지).
"논리 시스템"이 정확히 무엇을 의미하는지에 따라 다릅니다. "기초 시스템"을 의미하는 경우 중요한 것은 증명이 계산 가능하게 검증 될 수 있다는 것입니다. 즉, 시스템에서 증명할 수있는 모든 문장에는 증명이라고하는 (유한) 문자열로 증명할 수있는 증인이 있으며 입력 된 문자열 쌍을 제공하는 단일 증명 검증 프로그램이 있습니다.$(p,x)$ 항상 중지되고 출력은 "예"입니다. $p$ 문장 체계에 대한 유효한 증거 $x$. 이것은 인간이 사용할 수있는 가장 일반적인 기초 시스템 개념입니다 (우리가 아는 한).
비 고전적 이론과 유형 이론을 포함하여 수학적 역사에서 제안 된 다른 모든 기본 시스템과 마찬가지로 계산 가능하게 결정 가능한 일련의 공리와 적절한 연역 시스템을 가진 FOL 이론은 모두 위의 개념에 포함됩니다.
그러나 일반 FOL 이론 (아마도 계산할 수 없거나 계산할 수없는 언어 또는 공리가있을 수 있음)과 같은 "추상 형식 시스템"을 의미하는 경우 반드시 메타 시스템 내에서 작업해야합니다 (지금부터 MS라고 부를 것입니다). ), 공식적으로하지 않더라도. MS는 위의 개념에 따라 변함없이 그 자체가 기본 시스템입니다.
다음으로, 이전 문장에서 진실과 거짓 진술이 어떻게 뒤 따르는 지 적습니다. 나의 현재 이해는 또한 이러한 규칙을 가정해야한다는 것입니다. 그것들은 어떤 메타 언어 나 원칙에서도 추론 될 수 없습니다. 하나는 단순히 어딘가에서 시작해야합니다. 맞습니까?
예, 이것은 앞서 언급 한 추론 규칙입니다. 그러나 "[...]에서 진실과 거짓 진술이 어떻게 나오는지"라고 말하는 것은 정확하지 않습니다. 형식 시스템은 단지 구문 규칙을 규정 할 뿐이며 "참"또는 "거짓"이라는 개념은 없습니다. 이러한 종류의 의미 론적 의미는 MS 내에서든 현실 세계의 자연어 내에서든 외부 에서만 할당 할 수 있습니다 .
또한 예, 규칙과 공리는 의미있는 의미에서 '추론'될 수 없습니다. 그것에 대해 매우 신중하게 생각하면 이 게시물에서 스케치 한 것처럼 비 원형으로 정의되거나 정당화 될 수없는 논리의 기본 개념이 있음을 알 수 있습니다 .
논리 시스템의 정의 또는 추론 규칙 중 하나가 아닌 논리 시스템의 진술에 대해 논리 시스템의 추론 규칙을 사용하여 증명할 수 있습니까? 아니면 일종의 직관적 인 방법을 사용해야합니까? 메타 로직 (처음에 언급했던 것)을 증명하기 위해?
이 부분은 말이되지 않습니다. 위에서 말한 것처럼 계산 가능한 형식 시스템이 주어지면 문자열이$x$ 시스템에 대한 정리 (즉 입증 된 문장)인지 아닌지가 확실하게 참 또는 거짓 (어떤 것인지 알아낼 수 있는지 여부)이며 이것은 단순히 증거가 있는지 여부입니다. $p$ 해당 시스템의 증명 검증자가 입력에 "예"를 출력하도록 $(p,x)$. 그런지 여부를 알아낼 수 있는지 여부는 중요하지 않습니다.$p$ 존재하는지, 또는 당신이 이것을 알아낼 수 있지만 그런 것을 찾을 수 없는지 $p$, 또는 어떻게 찾을 수 있는지 $p$(그렇다면). 잘못된 추론과 기회를 사용하더라도$p$, 증명 검증기를 실행하고 실제로 증명인지 확인할 수 있습니다. $x$. 증거는 당신이 그것을 얻는 방법에 관계없이 유효합니다.
그럼에도 불구하고 당신이 요청하는 것은 공식 시스템이 의미 가 있다는 것을 우리가 어떻게 아는가하는 것 입니다. 글쎄, 당신은 손으로 흔들어서 그것이 좋아 보인다고 말할 수도 있고, 또는 "실세계에서 이런 특별한 방식으로 해석 될 때 사실처럼 보이는 정리를 증명한다"와 같은 말을 할 수 있습니다. 그래서 그것은 두 번째에서 언급했듯이 경험적으로 지원됩니다. 자연의 공리 화에 대한이 게시물의 일부입니다 .
또는 MS 내에서 작업하고 공식 시스템이 $S$입니다 소리는 당신이 MS 내에서 정의하는 것이 "소리"의 몇몇 정의. 즉, 귀하와 다른 사람이 귀하가 선택한 MS가 의미 있다는 데 동의하면 MS에 대한 일부 문장의 증거를 찾을 수 있습니다.$S$ "사운드"는 MS 내에서 표현할 수있는 속성입니다.
예를 들어, FOL이 건전하다는 것을 증명할 수 있습니다 (MS 내에서). $M$ 및 모든 세트 $A$ 문장 수 $M$ 그것은 사실이다 $M$ (FOL 구조, 문장 및 진실은 모두 MS 내에서도 정의됩니다.) $A$ FOL에 대한 연역적 시스템을 사용하는 것은 $M$.
또 다른 예를 들어, 공식 시스템의 산술적 건전성을 정의 할 수 있습니다. $S$ 번역이 있다는 속성으로 $t$ 모든 산술 문장에 대해 산술 문장 (즉, PA 언어로 된 문장)에서 $Q$, 만약 $S$ 증명하다 $t(Q)$ 그때 $Q$ 사실이다 $(\mathbb{N},0,1,+,·,<)$ (물론이 구조는 MS 내에서도 구성됩니다).
우리가 선택한 MS 자체가 의미가 있다는 것을 어떻게 알 수 있습니까? 앞서 언급했듯이 우리는 비순환 적으로 알 수 없습니다. 절대적인 용어로 그 건전성에 대해 말할 수도 없습니다. 그러나 합리적인 MS에 대해 우리는 산술 문장의 번역을 가지고 있습니다 (MS가 기본적인 산술 추론을 수행 할 수 있기를 원하기 때문에), 따라서 적어도 MS가 산술적으로 일관성이 없는지, 즉 증명 여부에 대해 이야기 할 수 있습니다.$t(0=1)$. 이것은 잘 정의 된 질문이며 MS가 그렇게 하지 않기를 바랍니다 ! 그러나 Godel-Rosser가 본질적으로 보여준 것처럼, 그러한 합리적인 MS는 그것이 실제로 산술적으로 일관성이없는 경우가 아니라면 그것이 산술적으로 일관성이 있다는 것을 증명할 수도 없습니다 ... (이것은 불완전 성 정리입니다.)
마지막으로 대부분의 논리 텍스트는 ZFC 또는 적어도 ZC와 같은 합리적으로 강력한 MS를 사용합니다. 이것은 셀 수없는 이론에 대해서도 FOL에 대한 압축 정리와 같은 것을 증명하기를 원하기 때문이며, 이것은 세트 이론적 가정이 상당히 필요하기 때문입니다. 그러나 셀 수있는 이론에 대한 사실 만 증명하고 싶다면 ACA와 같은 훨씬 더 약한 MS로 할 수 있습니다 ( 이 게시물 참조 ).
논리 (예 : 1 차 / 술어 논리)를 새로운 명제를 생성하기 위해 플레이하는 게임으로 생각할 수 있습니다. 다른 게임과 마찬가지로 어딘가에서 시작해야합니다. 말하자면 시작 부분과 기본 규칙이 필요합니다. Predicate의 경우 시작 부분은 상수, 변수, 수량 자, 술어 및 논리 연산자로 구성된 명제입니다. "놀이의 규칙"은 추론 / 추론의 규칙입니다. 그들은 신이 주거나 자명하지 않습니다 . 즉, 표준 이 아닙니다 . 사람들은 자신의 목표와 신념에 따라 어떤 규칙을 사용할지 선택합니다 (참조 : 자연 추론 vs 순차 미적분 vs 힐베르트 시스템). 예를 들어, 어떤 사람들은 Predicate가 Excluded Middle의 법칙을 갖도록 허용하고 다른 많은 사람들은 거부합니다. 전자 유형의 시스템 에는 공리에서 비 구조적으로 따르는 명제가 있지만 후자에서는 그렇지 않을 수 있습니다 (예를 들어, Q 형식의 인수가$(P \vee \neg P) \Rightarrow Q,\, \therefore Q$ 모든 경우를 소진하지 않을 수 있습니다. $P$).
즉, 게임을하는 것과 같이, 어떤 종류의 명제가 허용 되든간에 시스템 (예 : 술어)이 수락 / 승인하는 새로운 명제를 생성하기 위해 확립 된 추론 규칙을 사용해야합니다. 사실, 제가 말한 내용을 문자 그대로 만드는 논리의 게임 화가 많이 있습니다 . 그중 하나가 여기 있습니다 .
편집 (더 나은 주소 하나가 있는지 여부의 질문에 있어야 정리를 생성 할 때 단지 공리를 사용) : 당신은 할 수 말하자면, "규칙을 위반"하고 비 공리 / 정리 문을 사용하여 일을 "증명"하지만, 당신이 할 수있는 공리에서 추론하거나 추론하지 않는 한 유효한 추론 규칙이라고 보장 할 수 없습니다. 예를 들어, 많은 "증거"가 존재를 보장 할 수없는 선택 기능을 포함하기 때문에 세트 이론의 ZF 시스템 (ZFC 생성)에 선택의 공리를 채택하게되었습니다.