論理システムでステートメントを証明するとき、直感的な「メタ」ロジックを使用しますか、それともシステムからの控除ルールを使用しますか？
私はこの主題に不慣れですが、現在、命題論理と述語論理についての講義ノートを読んでいます。私は特に論理と言語の境界線に興味があります。私がここで述べていることのいくつかが間違っている場合は、訂正してください。
想像できる世界のあらゆるものについて声明を出すことができ、この声明（ある言語での声明が何であれ）は真または偽（またはその中間の可能性があるもの）である可能性があります。他のステートメントがすでに真実であるという条件で、言語で作成できるいくつかのステートメントの有効性について直感的に理解しています。
All cats live on earth.
Simon is a cat.
THEREFOR Simon lives on earth.
私は、文の有効性を判断するこのプロセスを形式化する論理システムを理解しています（猫または何らかの多様体を記述しているかどうかに関係なく）-ここで間違っている場合は、私を訂正してください。
AFAIKは、論理システムを「発明」するときに、いくつかの定義を書き留めます（たとえば、論理記号、述語、式などの特定のオブジェクトの呼び出し方法、またはそれらの構造は何か）。定義は何かを呼び出す方法についての単なる合意であるため、これは私にとっては問題ありません。私の脳は、私が知覚するオブジェクトを私がそれらと呼びたい方法で呼ぶ世界に住むのに十分強力です）。
次に、前の文から真と偽のステートメントがどのように続くかを書き留めます。私の現在の理解では、これらのルールを想定する必要があり、メタ言語や原則から推測することはできません。どこかから始めなければなりません。そうですか？
この時点で、私が遭遇したほとんどの講義ノートは、健全性、完全性、一貫性、および構文と意味の真理の同等性などについて話し始めます。そして、彼らは論理システムについて結論を出し始めます。
私の質問は次のとおりです。論理システムの定義でも推論規則の1つでもない論理システムのステートメントについては、論理システムの推論規則のみを使用してそれらを証明しますか？それとも、それらを証明するために、ある種の直感的なメタロジック（最初に話したもの）を使用しますか？
回答
私は、文の有効性を判断するこのプロセスを形式化する論理システムを理解しています（猫または何らかの多様体を記述しているかどうかに関係なく）-ここで間違っている場合は、私を訂正してください。
あなたは正しいです。特に、正式なシステムは、あなたが推測できる文を規定するだけです。システムは、記号や文に意味を与えません。それはあなたが何を推測できるかをあなたに伝えるだけです。あなたが彼らに何らかの意味を帰したいのなら、もちろんあなたはそのシステムの中でそうすることはできませんが、それの外でそれをしなければなりません。ヒルベルト流の体系では、モーダスポネンスの法則と公理を使用して、演繹できる文が規定されています。他の形式システム（フィッチスタイルシステムなど）には、さまざまな種類の推論規則があります。
AFAIKは、論理システムを「発明」するときに、いくつかの定義を書き留めます（たとえば、論理記号、述語、式などの特定のオブジェクトの呼び出し方法、またはそれらの構造は何か）。
それはあなたが「論理システム」によって正確に何を意味するかによります。「基礎システム」を意味する場合、重要なのは、証明が計算可能に検証可能であるということです。つまり、システムで証明できるすべての文には、証明と呼ばれる（有限の）文字列による証明可能性の証人があり、文字列の任意の入力ペアを指定する単一の証明検証プログラムがあります。$(p,x)$ 常に停止し、その出力は「はい」です。 $p$ 文のシステムに対する有効な証拠です $x$。これは、（私たちが知る限り）人間がこれまでに使用できる基本システムの最も一般的な概念です。
非古典的理論や型理論を含む、数学史で提案されている他のすべての基礎システムと同様に、計算可能に決定可能な公理のセットと適切な帰納的システムを備えたFOL理論はすべて上記の概念に含まれることに注意してください。
ただし、一般的なFOL理論（おそらく計算不可能または数えられない言語または公理を持っている可能性があります）などの「抽象的な形式システム」を意味する場合は、必然的にメタシステム内で作業する必要があります（これからMSと呼びます）。 ）、正式に行わなくても。MSは、上記の概念に従って、常にそれ自体が基本的なシステムであることに注意してください。
次に、前の文から真と偽のステートメントがどのように続くかを書き留めます。私の現在の理解では、これらのルールを想定する必要があり、メタ言語や原則から推測することはできません。どこかから始めなければなりません。そうですか？
はい、これらは先に述べた推論規則です。しかし、「[...]から真と偽のステートメントがどのように続くか」と言うのはそれほど正確ではありません。正式なシステムは単に構文規則を規定するだけであり、「真」または「偽」の概念はないことを忘れないでください。そのような意味的な意味は、MS内であろうと、現実世界の自然言語内であろうと、外部からのみ割り当てることができます。
また、はい、ルールと公理は意味のある意味で「推論」することはできません。それについて非常に注意深く考えると、この投稿でスケッチしているように、論理には非循環的に定義または正当化できない基本的な概念があることがわかります。
論理システムの定義でも推論規則の1つでもない論理システムのステートメントについては、論理システムの推論規則のみを使用してそれらを証明しますか？それとも、ある種の直感的なものを使用する必要がありますか？それらを証明するためのメタロジック（最初に話したもの）？
この部分は実際には意味がありません。私が上で言ったことによると、任意の計算可能な形式システムを考えると、文字列かどうか$x$ はシステム上の定理（つまり証明された文）であるかどうかは、決定的に真か偽か（それがどれであるかを理解できるかどうか）であり、これは単に証拠があるかどうかです。 $p$ そのシステムの証明検証者が入力に「はい」を出力するように $(p,x)$。あなたがそのようなかどうかを理解できるかどうかは関係ありません$p$ 存在するか、これを理解できるがそのようなものを見つけることができないかどうか $p$、またはどのように見つけることができますか $p$（もしあなたがそうするなら）。あなたがそのような時に間違った推論とチャンスを使用したとしても$p$、証明ベリファイアを実行して、それが実際に証明であることを確認できます $x$。証明は、どのように入手したかに関係なく有効です。
それにもかかわらず、おそらくあなたが求めているのは、正式なシステムが意味があることを私たちがどのように知っているかということです。さて、あなたは手を振ってそれが良さそうだと言うか、あるいは「現実の世界でこの特定の方法で解釈されたときに真実に見える定理を証明する」のようなことを言うことができるので、2番目に述べたように経験的にもサポートされています自然の公理化についてのこの投稿の一部。
または、MS内で作業して、正式なシステムであることを証明できます。 $S$ある音は、あなたがMS内で定義することを「音」のいくつかの定義については、。つまり、あなたと他の誰かがあなたが選んだMSが意味があることに同意するなら、あなたはMS上である文の証拠を見つけることに進むことができます。$S$ は音です。ここで、「音」はMS内で表現できるプロパティです。
たとえば、（MS内で）FOLが健全であることを証明できます。つまり、任意の1次構造が与えられます。 $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でやり遂げることができるかもしれません（この投稿を参照）。
一階述語論理や述語論理などの論理は、新しい提案を作成するためにプレイするゲームと考えることができます。他のゲームと同様に、どこかから始める必要があります。いわば、出発点と基本的なルールが必要です。述語の場合、開始部分は、定数、変数、数量詞、述語、および論理演算子から構築された命題です。その場合、「遊びのルール」は推論/演繹のルールです。それらは神から与えられたものでも自明でもありません。つまり、正規のものではありません。人々は、自分の目標と信念に基づいて、どのルールで遊ぶかを選択します（自然演繹vsシークエント計算vsヒルベルトシステムを参照）。例として、一部の人々は述語に排中律を持つことを許可しますが、他の多くの人々はそれを拒否します。前者のタイプのシステムでは、公理から非建設的に続く命題がありますが、後者ではそうではないかもしれません（たとえば、形式のQの引数のため）$(P \vee \neg P) \Rightarrow Q,\, \therefore Q$ すべてのケースを使い果たすとは限りません $P$）。
したがって、要するに、ゲームをプレイするのと同じように、システム（述語など）が受け入れる/承認する新しい命題を生成するには、許可されているあらゆる種類の命題について、確立された推論規則を使用する必要があります。実際、私が言ったことを非常に文字通りにする論理のゲーミフィケーションはたくさんありますが、そのうちの1つがここにあります。
編集（定理を作成するときに公理のみを使用する必要があるかどうかの問題に適切に対処するため）：いわば「規則を破る」ことができ、非公理/定理ステートメントを使用して物事を「証明」することができますが、それを1つとして受け入れるか、後で公理から推論しない限り、それが有効な推論規則であるとは保証されません。これは、たとえば、集合論のZFシステム（ZFCの作成）に選択公理を採用することにつながります。これは、多くの「証明」に、存在が保証できない選択関数が含まれているためです。