この記事では、形式的な定理証明の例を通じて、ATS で命題を直接エンコードする方法を示します。 この記事で使うコード全体は、ファイル prop-logic.sats と prop-logic.dats を見てください。
真理値は抽象命題 PTRUE と PFALSE としてエンコードされます:
absprop PTRUE // for true absprop PFALSE // for falsetrue に対しては、1つ導入 (introduction) 規則があり、除去 (elimination) 規則はありません:
praxi true_intr((*void*)): PTRUE
false に対しては、導入規則はありませんが、1つの除去規則があります:
praxi false_elim{A:prop}(pf: PFALSE): A
明確に、規則 false_elim は false の証明からはどのような命題も導けることを示しています。
明細 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 は、証明 ~A と A の上に false の証明が構築できることを示しています。
neg_elim と false_elim を合成することで、証明 A と ~A からどのような命題 B も導出できることを示す次の規則が得られます:
// prfn neg_elim2 {A:prop}{B:prop} (pf1: A, pf2: ~A): B = false_elim(neg_elim(pf1, pf2)) //
2つの命題 A と B が与えられたとき、A と B の論理積を表わすのに 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)) //
2つの命題 A と B が与えられたとき、A と B の論理和を表わすのに 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_l と disj_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]
2つの命題 A と B が与えられたとき、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))
)
)
)
2つの命題 A と B が与えられたとき、A と B が(命題として)同値であることを表わすのに 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 である見なすことができます。