前回、大小関係の>を演繹してよい規則を勝手に作りましたので、その規則を一般化できるか試してみます。
我流大小関係
復習
記号
⊢\vdash は、ターンスタイル（turnstile、回転扉）あるいはティー (tee) と呼ばれ、意味的には「生成する」あるいは「証明する」と読まれる。これは言語内の記号ではなく、証明を論じる際のメタ言語内の記号である。上記のようなシークエントの直観的な意味は、Γ を前提としたとき、結論である Σ を証明可能ということである。
Wikipedia
で、下が前回の大小関係の我流の定義。
論理学や数学の思想を覚える為のものなので、厳密さは無視しています。
∃x(1+x=3)⊢3>1
日本語に翻訳すると
「『1+x=3』を満たすようなxが存在するなら、3>1を演繹してよい。」
論理式だけならば、「1に自然数の集合の要素の何かを加えると、3になる」としか言っていないのですが、それはある側面では「3は1の後者(いくつ後ろから置いといて)である」ことを意味し、さらにそれは「3は1より大きい」と解釈できます。
地球の数学を知らない宇宙人に説明する為の書き方と思うしかないですね。むしろ「より大きい」という認識の無駄を省くとこうなってしまうのだから、これが純粋な認識の在り方なのかもしれません。
1.1+x=3(仮定)
2.x=2(仮定)
3.1+2=3(代入)
4.3=3(加法定義)
5.∃x(1+x=3)(∃導入)
6.3>1(>導入)
前回の>の演繹です。
仮定を解消した方が完結させた観が気持ちが良いので、>を演繹する際は仮定も解消できるとしておきます。参考書の∃除去でも仮定の解消を認めているので、ひとまずこれで良しとしておきます。
1.[1+x=3]
2.[[x=2]
3.1+2=3(代入)
4.3=3(加法定義)
5.∃x(1+x=3)(∃導入)
6.3>1(>導入)
7.1+x=3→3>1
1+x=3→3>1って定理を推論規則から演繹しましたが、具体的な数字だと汎用性がないので代数的に∃と∀記号を用いて表現。
∀x∃y(S(x)=y)⊢y>x
任意のxの後者yが存在する場合、y>xを演繹してよい。
我流なので厳密性は保証しませんので悪しからず。
1.[2](仮定)
2.S(1)=2(加法定義)
3.∃y(S(1)=y)(∃導入)
4.∀x∃x(S(x)=y)(∀導入)
5.2>1
大小関係を一般化できていのか不安ですが、まあ今はこんなもんで納得しておきます。楽しければ正しさは二の次。この認識を頭の中に置いといて整合性が取れない場合にのみ修正していく、ボクシングの習得と同じ方針です。
コメント