1. 実装

1.1 言語

言語とは構文規則に則った論理式の集合のこと

命題論理の言語は以下の規則で再帰的に定める:

規則1: 原子命題記号は論理式
規則2: 論理式に NOT, AND, OR, IF したものは論理式
規則3: それ以外は論理式ではない

type VAR =
  | Proposition of string

type Formula =
  | Prime of VAR
  | NOT of Formula
  | AND of Formula * Formula
  | OR of Formula * Formula
  | IF of Formula * Formula

命題記号は文字列の内容を持てるようにした

1.2 解釈

解釈とは原子命題記号全体の部分集合。直観的に言えば成り立っている事実をかき集めたもの:

type Interpretation = 
  | Interpretation of Set<VAR>
    static member Contains v (Interpretation ipn) = Set.contains v ipn

解釈を定めると論理式の値は以下の規則で再帰的に決まる:

規則4: 原子命題記号の値はそれが解釈に含まれていればTそうでなければF
規則5: 論理式fがNOTされている時の値はfの値がTならFで、FならT
規則6: 論理式f1とf2がANDされている時の値は f1,f2の値が共にTならTで、そうでないときはF
規則7: 論理式f1とf2がORされている時の値はf1,f2の値が共にFならFで、そうでないときはT
規則8: 論理式f1とf2がIFされている時の値は「f1の値がF」か「f2の値がT」のときTで、そうでないときはF

// 論理式の値
type FormulaValue =
  | T
  | F

let formulaValue (ipn:Interpretation) (wff:Formula) =
  let rec b f =
    match f with
      | Prime p -> Interpretation.Contains p ipn
      | NOT f1 -> not (b f1)
      | AND (f1, f2) -> (b f1) && (b f2)
      | OR (f1, f2) -> (b f1) || (b f2)
      | IF (f1, f2) -> (not (b f1)) || (b f2)
  if b wff then T else F

1.3 妥当性

恒真式とは任意の解釈でTの値を持つ論理式。直観的に言えばどんな場合でも成り立つ論理式。哲学的に言えば分析的な真理。恒偽式とは任意の解釈でFの値を持つ論理式。充足可能な式とはTの値を持ちうる式:

注: ユーティリティ関数powersetは本稿末尾に記載

// 論理式の妥当性
type FormulaType =
  | Tautology
  | Contradiction
  | Satisfiable

let formulaType (allvars:VAR list) (wff:Formula) =
  let allipns = allvars |> powerset |> List.map (set >> Interpretation) 
  if List.forall (fun ipn -> (formulaValue ipn wff) = T) allipns 
  then Tautology
  else if List.forall (fun ipn -> (formulaValue ipn wff) = F) allipns 
  then Contradiction
  else Satisfiable

2. 実例

表示関数を定義:

// 表示関数
let rec meaning = function
  | Prime a -> a |> fun (Proposition p) -> p // unwrap
  | NOT a -> sprintf "%s ..でない" (meaning a)
  | AND (a,b) -> sprintf "「%s」かつ「%s」" (meaning a) (meaning b)
  | OR (a,b) -> sprintf "「%s」か「%s」のどちらか" (meaning a) (meaning b)
  | IF (a,b) -> sprintf "「%s」なら「%s」だ" (meaning a) (meaning b)

let analyze allvars wff =
  match formulaType allvars wff with
    | Tautology -> "<恒真>"
    | Contradiction -> "<恒偽>"
    | Satisfiable -> "<充足可能>"
  |> fun a -> sprintf "%s: %s" a (meaning wff)

準備

let p = Proposition "東京は梅雨"
let q = Proposition "大阪は梅雨"
let allvars = [p;q]
let shows = analyze allvars >> printfn "%s"

let P = Prime p
let Q = Prime q

2.1 排中律・無矛盾律の例

$P, P\lor\lnot P, P\land\lnot P,\lnot(P\land\lnot P)$ という四つの論理式の分析結果を記載。当たり前の結果が得られた:

P |> shows
OR (P, NOT P) |> shows
AND (P, NOT P) |> shows
NOT (AND (P, NOT P)) |> shows
(* 出力
<充足可能>: 東京は梅雨
<恒真>: 「東京は梅雨」か「東京は梅雨 ..でない」のどちらか
<恒偽>: 「東京は梅雨」かつ「東京は梅雨 ..でない」
<恒真>: 「東京は梅雨」かつ「東京は梅雨 ..でない」 ..でない
*)

2.2 前線形性の例

古典論理における $\to$ の奇妙な意味付けの例は $(P\to Q)\lor(Q\to P)$が恒真となること。実質含意のパラドックスともいわれる

OR (IF (P,Q), IF (Q,P)) |> shows

// <恒真>: 「「東京は梅雨」なら「大阪は梅雨」だ」か「「大阪は梅雨」なら「東京は梅雨」だ」のどちらか

2.3 三段論法の例

三段論法を命題論理の言語に写した $P\land(P\to Q)\to Q$ という論理式は恒真になる

IF ((AND (P, IF (P,Q))), Q) |> shows

// <恒真>: 「「東京は梅雨」かつ「「東京は梅雨」なら「大阪は梅雨」だ」」なら「大阪は梅雨」だ

3. 振り返り

Set の上手いマッチの仕方がわからずに Set と List を行ったり来たりしてしまった。Setで x::xs みたいに要素ひとつとそれ以外のようなマッチをどう実現したらいいのだろう
Satisfiableは Satisfiable of string として充足解の例を入れるという改良の余地がありそう
discriminated union とマッチが非常に相性がよいと思った
formulaTypeの実装が酷い
VAR を管理する構造があるとよさそう。VariableManager とか。

4. おまけ

使ったユーティリティ関数powerset

let rec powerset = function
  | [] -> [[]]
  | x::xs -> 
      let ps = powerset xs
      ps @ List.map (List.append [x]) ps

F# で命題論理