Effective ATS:
命題をエンコードする

この記事では、形式的な定理証明の例を通じて、ATS で命題を直接エンコードする方法を示します。 この記事で使うコード全体は、ファイル prop-logic.satsprop-logic.dats を見てください。

真理値をエンコードする

真理値は抽象命題 PTRUEPFALSE としてエンコードされます:

absprop PTRUE // for true
absprop PFALSE // for false
true に対しては、1つ導入 (introduction) 規則があり、除去 (elimination) 規則はありません:
praxi true_intr((*void*)): PTRUE
false に対しては、導入規則はありませんが、1つの除去規則があります:
praxi false_elim{A:prop}(pf: PFALSE): A
明確に、規則 false_elimfalse の証明からはどのような命題も導けることを示しています。

否定 (negation) をエンコードする

明細 A が与えられたとき、A を否定するのに PNEG(A) を使います。

absprop PNEG(A: prop) // for negation
propdef ~(A: prop) = PNEG(A) // shorthand
便宜上、PNEG(A)~A と書くこともできます。 否定に対して、1つの導入規則と1つの除去規則があります:
praxi neg_intr{A:prop}(fpf: A -> PFALSE): ~A
praxi neg_elim{A:prop}(pf1: ~A, pf2: A): PFALSE
本質的に neg_intr は、もし A のどのような証明も false の証明の構築に使えるなら、~A が導出できることを意味しています。 否定の除去として neg_elim は、証明 ~AA の上に false の証明が構築できることを示しています。

neg_elimfalse_elim を合成することで、証明 A~A からどのような命題 B も導出できることを示す次の規則が得られます:

//
prfn
neg_elim2
  {A:prop}{B:prop}
  (pf1: A, pf2: ~A): B = false_elim(neg_elim(pf1, pf2))
//

論理積 (conjunction) をエンコードする

2つの命題 AB が与えられたとき、AB の論理積を表わすのに PCONJ(A, B) を使います:

absprop
PCONJ(A: prop, B: prop)
propdef &&(A: prop, B: prop) = PCONJ(A, B) // shorthand
便宜上、PCONJ(A, B)A && B と書くこともできます。 論理積に関連して、1つの導入規則と2つの除去規則があります:
//
praxi
conj_intr
  {A,B:prop} : (A, B) -> A && B
//
praxi
conj_elim_l{A,B:prop} : (A && B) -> A
praxi
conj_elim_r{A,B:prop} : (A && B) -> B
//
例として、次の証明は論理積が可換であることを示しています:
//
prfn
conj_commute
  {A,B:prop}(pf: A && B): B && A =
  conj_intr(conj_elim_r(pf), conj_elim_l(pf))
//

論理和 (disjunction) をエンコードする

2つの命題 AB が与えられたとき、AB の論理和を表わすのに PDISJ(A, B) を使います:

dataprop
PDISJ(A: prop, B: prop) =
  | disj_intr_l(A, B) of (A)
  | disj_intr_r(A, B) of (B)
//
propdef ||(A: prop, B: prop) = PDISJ(A, B)
//
便宜上、PDISJ(A, B)A || B と書くこともできます。 例として、次の証明は論理和が可換であることを示しています:
//
prfn
disj_commute
  {A,B:prop}(pf0: A || B): B || A =
  case+ pf0 of
  | disj_intr_l(pf0_l) => disj_intr_r(pf0_l)
  | disj_intr_r(pf0_r) => disj_intr_l(pf0_r)
//
PDISJ に関連した2つのコンストラクタ disj_intr_ldisj_intr_r は論理和に関連する2つの導入規則に対応しています。 そして次の関数 disj_elim は論理和に関連した除去規則をエンコードしています:
//
prfn
disj_elim{A,B:prop}{C:prop}
  (pf0: A || B, fpf1: A -> C, fpf2: B -> C): C =
  case+ pf0 of
  | disj_intr_l(pf0_l) => fpf1(pf0_l)
  | disj_intr_r(pf0_r) => fpf2(pf0_r)
//
別の例として、次のコードは論理積が論理和に対して分配法則を満たすことを示す証明関数を実装しています:
prfn
conj_disj_distribute
  {A,B,C:prop}
(
  pf0: A && (B || C)
) : (A && B) || (A && C) = let
//
val pf0_l = conj_elim_l(pf0)
val pf0_r = conj_elim_r(pf0)
//
in
//
case+ pf0_r of
| disj_intr_l(pf0_rl) =>
    disj_intr_l(conj_intr(pf0_l, pf0_rl))
  // end of [disj_intr_l]
| disj_intr_r(pf0_rr) =>
    disj_intr_r(conj_intr(pf0_l, pf0_rr))
  // end of [disj_intr_r]
//
end // end of [conj_disj_distribute]

論理包含 (implication) をエンコードする

2つの命題 AB が与えられたとき、A から B への論理包含を表わすのに PIMPL(A, B) を使います:

//
absprop
PIMPL(A: prop, B: prop)
//
infixr (->) ->>
propdef ->>(A: prop, B: prop) = PIMPL(A, B)
//
便宜上、PIMPL(A, B)A ->> B と書くこともできます。 論理包含に対して、1つの導入規則と1つの除去規則があります:
//
praxi
impl_intr{A,B:prop}(pf: A -> B): A ->> B
//
praxi
impl_elim{A,B:prop}(pf1: A ->> B, pf2: A): B
//
本質的に、A から B への論理包含は型 A -> B の関数として解釈されます。

例として、証明 (A ->> (B ->> C)) ->> ((A ->> B) ->> (A ->> C)) は次のようになります:

prfn
Subst{A,B,C:prop}
(
// argless
) : (A ->> (B ->> C)) ->> ((A ->> B) ->> (A ->> C)) =
impl_intr(
  lam pf1 =>
  impl_intr(
    lam pf2 =>
    impl_intr(
      lam pf3 =>
      impl_elim(impl_elim(pf1, pf3), impl_elim(pf2, pf3))
    )
  )
)

同値 (equivalence) をエンコードする

2つの命題 AB が与えられたとき、AB が(命題として)同値であることを表わすのに PEQUIV(A, B) を使います:

absprop
PEQUIV(A: prop, B: prop)
propdef == (A: prop, B: prop) = PEQUIV(A, B)
便宜上、PEQUIV(A, B)A == B と書くこともできます。 命題的な同値に対して、1つの導入規則と2つの除去規則があります:
//
praxi
equiv_intr
  {A,B:prop}(A ->> B, B ->> A): A == B
//
praxi
equiv_elim_l{A,B:prop}(pf: A == B): A ->> B
praxi
equiv_elim_r{A,B:prop}(pf: A == B): B ->> A
//

二重否定律

二重否定律は次のようにエンコードできます:

praxi LDN{A:prop}(~(~A)): A

排中律

排中律は次のようにエンコードできます:

praxi LEM{A:prop}((*void*)): A || ~A

パースの法則

パースの法則は次のようにエンコードできます:

praxi
Peirce{P,Q:prop}((*void*)): ((P ->> Q) ->> P) ->> P
このパースの法則は LEM と等価で、論理含意を結合した項でのみで示された LEM である見なすことができます。


この記事は Hongwei Xi によって書かれ、 Japan ATS User Group によって翻訳されています。