様相論理の一点フレームに関する定理
Thm
$ Aは様相論理式とする．
何らかのKripkeフレーム$ Fで$ F \vDash Aのとき，非反射的な一点フレームまたは反射的なフレームのどちらかでもvalid． proof
$ Fがdead-end$ xを持つとき，非反射的な一点フレーム$ G := \lang \{x\}, \emptyset \rangとすると$ Fのgenerated-submodelになるのでgeneration theoremより$ G \vDash A
持たないとき，適当な反射的な一点フレーム$ \lang \{x\},\{\lang x,x \rang\} \rangとして$ Fの全ての点を$ xに写像する$ fを作る．この$ fは$ Fから$ G := \lang \{x\},\{\lang x,x \rang\} \rangへのp-morphismとなるため，reduction theoremより$ G \vDash A
ref
memo
非反射的な一点フレームは$ \bf Verと関係がある：すなわち$ Aは$ \bf Verの定理となる．
反射的な一点フレームは$ \bf Trivと関係がある．
しかもdead-endを持たない：任意の$ Fの各点はsuccessorを持つ：すなわちSerialなので，元のフレームは$ \bf KDと関係がある．
すなわち，$ Aは$ \bf KDから$ \bf Trivのどこかの間の論理の定理である．
纏めると，$ \bf Kの定理は
$ \bf Verの定理か，
$ \bf KDから$ \bf Trivの論理の定理か
のどちらかである．