2006-12-08 [長年日記]
λ. 自由変数と限量子∀∃
かがみさんが「自由変数って」ということを書いていたので、自分の自由変数の理解を書いてみる。
任意の言語Lに対して、Lに含まれない定数記号xを新たに加えた言語をL{x}とする。そして、自由変数を含む式 φ(x) はLの式ではなくL{x}の式と考える。L{x}に更に新たな定数記号yを加えた言語はL{x}{y}と書けるが、L{x}{y}とL{y}{x}は区別せずに単にL{x,y}と書くことにする。そうすると、論理式φの自由変数の集合がFV(φ)であるとき、φ∈L(FV(φ))が成り立つ。
それから、LからL{x}への埋め込み I: L→L{x} が定義できる。この埋め込みには右随伴 L{x}→L や左随伴 L{x}→L が存在する場合があり、それぞれ(∀x)や(∃x)と書かれる。すなわち、任意の φ∈L, ψ∈L{x} に対して
- I(φ) |-L{x} ψ iff φ |-L (∀x)(ψ)
- (∃x)(ψ) |-L φ iff ψ |-L{x} I(φ)
【2006-12-14 追記】 檜山さんが「論理とはなにか？ (4:完) -- 論理から圏へ」で、「論理と圏の対応関係がうまくいっている例として直観主義論理があります」と書いていましたが、限量子を随伴で説明できることから、述語論理も圏と対応させることが出来ることがわかります。
こんにちは、鏡です。<br>モデル理論で全称記号や存在記号の解釈を行う場合、定数を水増しする手法が有効なことは知っていたのですが、自由変数水増し法 (というのか？) は始めて知りました。なるほど、この方式だと見通しが良い感じがします。あっ、すみません、私の数学って、基本的に「こういう感じ」数学なので(^^。<br>ああ、なんか少しもやもやがとれたような。ありがとうございます。
かみさんが、と読んでびびった。<br><br>あと、数式が顔文字に見えた。
ものすごく細かくて恐縮ですが<br><br>φ∈L(FV(φ))<br><br>ではなく，<br><br>φ∈L{FV(φ)}が成り立つ。<br><br>のような気がしました．気になったので (x∀x)<br><br>面白い話のような気がしますが，右随伴や左随伴という圏論用語 (?) がさっぱりという… orz<br><br># ささださんのネタを見て，この流れならイケる ！ と便乗コメント
＞かがみさん<br>お役に立てたみたいで良かったです。<br>モデル理論での事については知らなかったのですが、それも面白そうですね。<br><br>＞ささださん<br>かみさんって、コロンボかよ!<br>数式が顔文字に見えるのは、ありがちですよね。<br>最初に「∀」を顔文字に使った人は偉大だ……<br><br>＞あろはさん<br>記法は適当にでっち上げただけなので、細かいこと気にしたら負けです(笑<br>一応、FV(φ)が既に集合なので、φ∈L{FV(φ)} と書くと集合の集合に見えてしまって良くないと思い、こう書いてます。<br>それと、ここでの随伴は「すなわち」以下に書いた意味しかないので、圏論の知識がなくてもとりあえず平気です。