命題論理の構文論　syntax　：　トピック一覧　　

概説：命題論理の構文論syntax,証明論proof theory

　構文論という向き合い方

・論理式を作成する際に準拠すべき《規約》をあらかじめ定めた上で、
　個々の論理式について、
　　　その《規約》枠内の操作のみで作成されるか？
　という点に絞って問うていくのが、
　構文論syntaxという《命題論理への向き合い方》。

　*　構文論syntaxは、証明論proof theoryとも呼ばれる[戸次]。

　構文論のキーワード　〜　定理、証明、形式的体系

・その《規約》枠内の操作のみで作成される論理式を、
　その《規約》における《定理》と呼ぶ。[→詳細]

・定理が《規約》に準拠して作成されていくプロセスを、
　その定理のその《規約》における《証明》と呼ぶ。[→詳細]

・あらかじめ定めた《定理を作成する際に準拠すべき規約》のなかで、
　作成してよい論理式そのものズバリを明示した条項を、
　《公理》と呼ぶ。　　

・あらかじめ定めた《定理を作成する際に準拠すべき規約》のなかで、
　どのようなかたちの論理式のセットを与えられたときに、
　どのようなかたちの論理式へ書き換えてよいか明示した条項を、
　《推論規則・導出規則》と呼ぶ。

・《推論規則・導出規則》にしたがって、
　　《推論規則・導出規則》が指定した論理式のセットを、
　　《推論規則・導出規則》が指定した論理式へ書き換える操作を、
　　《〜から…を導出する》と呼ぶ。　　

・あらかじめ定めた《定理を作成する際に準拠すべき規約》の総体を、
　《形式的体系》と呼ぶ。[→詳細]

　構文論と意味論　〜　相違と関係

・命題論理の意味論で考察された論理式の真理値（真偽）という概念は、
　命題論理の構文論では一切導入されない。
　命題論理の構文論は、
　特定の論理式が、規約に照らして、正当な手続きで作成されたかのみを問うのであって、
　特定の論理式の真偽という点は、無視される。

・このように、命題論理の構文論と意味論は、いったん切り離されたうえで、
　のちに、両者の関係（そして、論理式の、規約に照らした作成手続きの正当性と、真偽の関連性）が、
　健全性soundness・完全性completenessの検討で論ぜられることになる。　

 構文論のメリット　〜　命題論理の形式的体系導入の意義　

構文論のメリット　〜　命題論理に形式的体系を導入する意義　　

定義：命題論理（命題計算）の形式的体系(証明体系・公理系)：公理と推論規則

【はじめに読む定義】

・命題論理の「形式的体系formal system」とは、下記二点を指定する規約・規格のこと。

　　[指定1]　公理axiomと呼ばれる論理式のセット

　　[指定2]　推論規則inference rule・導出規則と呼ばれる《論理式の変形規則》のセット

　*　どういうこと？　→　概説：構文論　

・上記二点の指定内容の変更によって、
　命題論理の「形式的体系」に、様々なバリエーションが生み出される。→形式的体系の諸タイプ　　

・命題論理の「形式的体系」が公理として指定する論理式は、
　　1個でも、複数でも、0個でも構わない。

・命題論理の「形式的体系」が推論規則・導出規則として指定する《論理式の変形規則》とは、
　　変形前の論理式のセットと、変形後の論理式を、下記体裁で明示したもの。　　　　　

【厳密な定義】

　命題論理の「形式的体系」とは、
　次項で定められる集合のこと。
　・公理axiomを元とする集合（公理は論理式の特定のものを表している）
　・推論規則rule of inferenceとよばれる図形の有限集合{Ri}
　　　Riにたいして自然数jが一意に定まり、
　　　任意のj個の表現の集合
　　　　　　　

　*命題論理に限らず、一般的に、
　「形式的体系S」とは、次の１〜４で定められる集合のこと。
　1.記号symbolを元とする可算集合（ここでは、論理記号と命題変数）
　　　　　ときとして、⊥を加えることがある[高崎VII.自然演繹(その1)1.1論理式・公理系・推論規則]
　2.表現expressionを元とする可算集合（ここでは論理式）
　　（表現は記号の有限列からつくられる）
　3.公理axiomを元とする集合（公理は表現の特定のものを表している）
　4.推論規則rule of inferenceとよばれる図形の有限集合{Ri}
　　　Riにたいして自然数jが一意に定まり、
　　　任意のj個の表現の集合{B1,…,Bj}および任意の表現Aに対して、
　　　{B1,…,Bj}がAとRiの関係にあるか否かが決定できる。
　　　このとき、Aは、{B1,…,Bj}から推論規則Riによって直接導かれているという。

　命題論理において「形式的体系」は、
　1.記号symbolを元とする可算集合として、
　　論理記号と命題変数の集合
　2.表現expressionを元とする可算集合として、
　　論理式の集合
　を使うので、
　この設定のもとで、
　命題論理の「形式的体系」とは、次の3,4で定められる集合のことになる。
　3.公理axiomを元とする集合（公理は論理式の特定のものを表している）
　4.推論規則rule of inferenceとよばれる図形の有限集合

「証明proof」の定義

【くわしい定義】

命題論理において、

・論理式A1が
　論理式A1の《形式的体系Sにおける証明proof》になっているとは、
　論理式A1が、
　　「形式的体系S」の公理そのものでである
　ということ。

・論理式の列A1,A2が
　論理式A2の《形式的体系Sにおける証明proof》になっていると は、
　　・論理式A1が、
　　　「形式的体系S」の公理そのものであって、
　　・論理式A2が、
　　　論理式A1から「形式的体系S」の推論規則の一つによって直接導かれたものである
　　ということ。

・論理式の列　A1,A2,A3が
　論理式A3の《形式的体系Sにおける証明proof》になっていると は、
　・論理式A1が、
　　「形式的体系S」の公理そのものであって、
　・論理式A2が、
　　　「形式的体系S」の公理そのものか、
　　　論理式A1から「形式的体系S」の推論規則の一つによって直接導かれたものか、
　　であって、
　・論理式A3が、
　　　　A1,A2のなかの論理式から「形式的体系S」の推論規則の一つによって直接導かれたもの
　　　である
　ということ。

・論理式の有限列A1,A2,…,Anが
　論理式Anの《形式的体系Sにおける証明proof》に なっている とは、

　・論理式A1が、「形式的体系S」の公理そのものであって、

　・論理式A2が、
　　　「形式的体系S」の公理そのものか、
　　　論理式A1から「形式的体系S」の推論規則の一つによって直接導かれたものか、
　　であって
　：
　：
　・論理式An-1が、
　　　「形式的体系S」の公理そのものか、
　　　A1,…,An-2のなかの論理式から「形式的体系S」の推論規則の一つによって直接導かれたものか、
　　であって

　・論理式Anが、
　　　A1,…,An-1のなかの論理式から「形式的体系S」の推論規則の一つによって直接導かれたもである
　ということ。

一般に、

　「形式的体系S」における表現（論理式）A1が
　「形式的体系S」における表現（論理式）A1の証明proofになっているとは、
　表現（論理式）A1が、「形式的体系S」の公理そのものでであるということ。

　「形式的体系S」における表現（論理式）の列　A1,A2が
　「形式的体系S」における表現（論理式）A2の証明proofになっているとは、
　　・表現（論理式）A1が、「形式的体系S」の公理そのものであって、
　　・表現（論理式）A2が、表現（論理式）A1から「形式的体系S」の推論規則の一つによって直接導かれたものである
　　ということ。

　「形式的体系S」における表現（論理式）の列　A1,A2,A3が
　「形式的体系S」における表現（論理式）A3の証明proofになっているとは、
　・表現（論理式）A1が、「形式的体系S」の公理そのものであって、
　・表現（論理式）A2が、
　　　「形式的体系S」の公理そのものか、
　　　表現（論理式）A1から「形式的体系S」の推論規則の一つによって直接導かれたものか、
　　であって、
　・表現（論理式）A3が、
　　　　A1,A2のなかの表現（論理式）から「形式的体系S」の推論規則の一つによって直接導かれたもの
　　　である
　ということ。


　「形式的体系S」における表現（論理式）の有限列A1,A2,…,Anが
　「形式的体系S」における表現（論理式）Anの証明proofになっている とは、
　・表現（論理式）A1が、「形式的体系S」の公理そのものであって、
　・表現（論理式）A2が、
　　「形式的体系S」の公理そのものか、
　　表現（論理式）A1から「形式的体系S」の推論規則の一つによって直接導かれたものか、
　　であって
　：
　：
　・表現（論理式）An-1が、
　　「形式的体系S」の公理そのものか、
　　A1,…,An-2のなかの表現（論理式）から「形式的体系S」の推論規則の一つによって直接導かれたものか、
　　であって
　・表現（論理式）Anが、
　　　A1,…,An-1のなかの表現（論理式）から「形式的体系S」の推論規則の一つによって直接導かれたもである
　ということ。　　

松本ママ
　「形式的体系S」における表現（論理式）Anの証明proofとは、
　次の条件1,2のいずれかを満足するようなSの表現の有限列A1,…An(An=A)をいう。
　すなわち、各i(i=1,…n)に対して、
　　(条件1)　Aiは「形式的体系S」の公理そのものである
　　(条件2)　Aiが「形式的体系S」の推論規則の一つによって、
　　　　　　　有限個の表現Aj(j<i)から直接導かれている。

「定理」の定義

【はじめに読む定義】

・論理式Aが命題論理の形式的体系Sにおける定理である
　　⊢A　　
　とは、
　形式的体系Sに準拠した操作のみで、論理式Aをつくれるということ、

　つまり、
　　・形式的体系Sが公理として指定した論理式をそのまま作成という操作
　　・形式的体系Sが推論規則として指定した《論理式の変形規則》に準拠して論理式を変形するという操作
　の組み合わせ・繰り返しのみで、論理式Aをつくれる

　ということ。

　*　どういうこと？　→　概説：構文論　

【くわしい定義】 

　論理式Aが《形式的体系Sの定理》であるとは、
　論理式Aの《形式的体系Sにおける証明proof》が存在するということ、
　　
　　つまり、
　　論理式Aそのものが、論理式Aの《形式的体系Sにおける証明proof》になっている
　　か、
　　論理式A1,Aが、論理式Aの《形式的体系Sにおける証明proof》になっている
　　か、
　　論理式の列A1,A2,Aが、論理式Aの《形式的体系Sにおける証明proof》になっている
　　か、
　　：
　　論理式の列A1,A2,…,AnAが、論理式Aの《形式的体系Sにおける証明proof》になっている
　　か、
   であるということ。

　　ママ「Sの表現Aが、Sの定理であるとは、SにおけるAの証明が存在するときをいう。」
　　　　[松本 定義5：定理theorem]

定義：派生推論規則　derived rule

・派生推論規則とは、
　形式的体系Sの推論規則のいくつかを組み合わせて、
　一つの推論規則とみなしたもののこと。[高崎]　

定義：⊢　（turnstile）　

【形式的体系一般において】
・論理式Aが、論理式の集合Γから導かれる
　　Γ⊢A

　とは、　
　　・Γに属す論理式
　　か、
　　・形式的体系Sが公理として指定する論理式
　から出発して、
　形式的体系Sが推論規則として指定する変形の繰り返しのみによって、
　論理式Aが得られること。

【命題論理の自然演繹において】

　　仮定のdischargeの説明が必要。

　論理式Aが《論理式の集合》Γから導かれる
　　Γ⊢A 　　
　とは、

　　・命題論理の形式的体系「自然演繹」に準拠した操作 　　
　　　つまり、公理の書き出し・仮定の書き出し・推論規則による書き換え　　　
　　　のみで、
　　　論理式Aが得られ、

命題論理の形式的体系の諸タイプ