メタロジック

形式言語とは、記号が体系的に整理された集合であり、その記号は形状と配置によって形式言語を正確に定義する。したがって、形式言語は表現の意味を参照することなく定義することができ、いかなる解釈が与えられる前、つまり意味を持つ前に存在し得る。一階述語論理は、何らかの形式言語で表現される。形式文法は、形式言語においてどの記号および記号の集合が論理式となるかを決定する。

形式言語は、固定アルファベット α 上の文字列 (有限シーケンス) の集合Aとして形式的に定義できます。ルドルフ・カルナップを含む一部の著者は、言語を順序対 <α, A > として定義しています。^{[ 3 ]}カルナップはまた、α の各要素がAの少なくとも 1 つの文字列に出現する必要があることを要求しています。

構成規則（形式文法とも呼ばれる）は、形式言語の整形式式を正確に記述したものである。これらは、形式言語のアルファベット上の文字列のうち、整形式式を構成する文字列の集合と同義である。ただし、構成規則は文字列の意味（つまり、文字列が何を意味するか）を記述するものではない。

形式体系（論理計算体系、または論理システムとも呼ばれる）は、形式言語と演繹装置（演繹システムとも呼ばれる）から構成される。演繹装置は、変換規則（推論規則とも呼ばれる）の集合、公理の集合、またはその両方から構成される。形式体系は、1つまたは複数の他の式から1つの式を導出するために用いられる。

形式システムは、順序付きトリプル <α、として形式的に定義できます。${\displaystyle {\mathcal {I}}}$、${\displaystyle {\mathcal {D}}}$d>、ここで${\displaystyle {\mathcal {D}}}$d は直接導出可能性の関係です。この関係は、形式体系の原始文が空の文の集合から直接導出可能であるという包括的な意味で理解されます。直接導出可能性は、文と有限で、場合によっては空の文の集合との間の関係です。公理は、すべての第一位の要素が${\displaystyle {\mathcal {D}}}$d はメンバーです${\displaystyle {\mathcal {I}}}$そして、2位のメンバーはすべて有限部分集合である${\displaystyle {\mathcal {I}}}$。

形式システムは、関係のみで定義することもできます。${\displaystyle {\mathcal {D}}}$d. これにより省略可能${\displaystyle {\mathcal {I}}}$また、解釈型形式言語および解釈型形式システム の定義におけるαも含まれる。しかし、この方法は理解や使用がより困難になる可能性がある。^{[ 3 ]}

形式的証明とは、形式言語の整形式な式の列であり、その最後の式が形式体系の定理である。定理は、証明体系においてそれより前に続くすべての整形式な式の構文的帰結である。整形式な式が証明の一部として認められるためには、それが証明列における前の整形式な式に、何らかの形式体系の演繹装置の規則を適用することによって得られるものでなければならない。

形式体系の解釈とは、その体系の記号に意味を、文に真理値を割り当てることである。解釈の研究は形式意味論と呼ばれる。解釈を与えることは、モデルを構築することと同義である。

メタ論理学では、形式言語は対象言語と呼ばれることがあります。対象言語に関する記述を行うために用いられる言語は、メタ言語と呼ばれます。この区別は、論理学とメタ論理学の重要な違いです。論理学は、ある形式言語で表現された形式体系における証明を扱うのに対し、メタ論理学は、ある対象言語に関するメタ言語で表現された形式体系に関する証明を扱います。

メタ論理学において、「構文論」は形式言語または形式体系そのものに関係し、それらの解釈は考慮しないのに対し、「意味論」は形式言語の解釈に関係する。「構文論的」という用語は、「証明論的」よりもやや広い範囲を指す。なぜなら、演繹体系を持たない形式言語の特性にも、形式体系にも適用できるからである。「意味論的」は「モデル理論的」と同義である。

メタ論理学では、 「使用」と「言及」という言葉は、名詞形と動詞形の両方において、重要な区別を明確にするために専門的な意味合いを持つ。^{[ 2 ]}使用と言及の区別（ 「言葉としての言葉の区別」と呼ばれることもある）とは、単語（または句）を使用することと、それを言及することの区別である。通常、表現が使用されているのではなく言及されていることは、引用符で囲むか、イタリック体で印刷するか、表現を単独で一行に置くことによって示される。表現を引用符で囲むことで、表現の名前が得られる。例えば、次のようになる。

この記事のタイトルは「メタロジック」です。 この記事はメタロジックについてです。

型トークンの区別はメタ論理における区別であり、抽象的な概念と、その概念の具体的な事例である対象を区別するものです。例えば、あなたのガレージにある特定の自転車は、 「自転車」という種類のもののトークンです。一方、ガレージにある自転車は特定の場所、特定の時間に存在しますが、「自転車は最近人気が高まっている」という文で使われる「自転車」はそうではありません。この区別は、形式言語の記号の意味を明確にするために用いられます。