← ファイル一覧
（保存にはログインが要ります）
1_basis/1_logic.book
ヘッダ
行番号
title 論理 author admin mathel default thmel default
section 一階論理記号 txt このシステムでは(等号を持つ)一階論理は仮定され、次の記号が使用されます。 word ⊤ ⊥ word ¬ word and or ⇒ ⇔ word ∀ ∃ word = txt 例えば `∀ x P^` はp-Formです。 br txt 結合力が異なる次の記号もあります。 word ⟹ ⟺ lower ⟹ lower ⟺ txt form内の \(\mathbb{W}_{++}\) はlower規則によって、処理されます。なお `$P` や `$Q` はformの穴(formが代入されるもの)です。 br txt 二項述語の否定を作るword関数ともいうべきものがあります。 word {/} lower {/} txt 引数のwordとの間にスペースは入れません。不等号は `{/}=` で作れます。なお `$..p` は？ section 省略表現 txt 通常の数学でよく使用される省略表現が用意されています。 txt 省略表現は abbr規則 により処理されます。`…` や `\n` はしかるべく処理されます。 abbr col txt 例 `[ x ; y ∈ A ]` ≈ `x ∈ A and y ∈ A` br abbr chain txt 次のような補題を用意しておくと便利なことがあります。 prop ⇔\n thm ⇔3 -| O prf `( [ chain |P1^ ⇔ |P2^ ⇔ |P3^ ] ) ⟺ ( [ chain |P1^ ⇒ |P2^ ⇒ |P3^ ⇒ |P1^ ] )` p-| O; ⇔3 h-| O; br abbr ∀ abbr ∃ txt このような変換規則の表現内では `x1` などはv-Formではなく v-Formの穴 です。
保存にはMatheliaへのログインが要ります。