ZFCert — 集合論証明スタジオ

自然演繹と ZFC 集合論に基づく、検証済みの定理証明支援系です。

証明スクリプト

カーネル結果

∴

準備完了

証明を待っています

スクリプトを検証すると、ここにカーネル結果が表示されます。

対話的ゴール

未開始

↓で定理宣言から開始します。

タクティク

intro H.含意または全称量化を導入 intros.利用可能な束縛を自動名で導入 exact H.事実でゴールを閉じる apply H.後ろ向きに推論する specialize H a as Ha.全称量化を具体化 obtain x Hx from H.存在量化を消去 put theorem_name.以前の定理を仮定に加える refl.等号の反射律 split.連言または同値を導入 cases H.仮定を分解する left. / right.選言を導入 use x.存在の証人を選ぶ resolution.一階述語論理の導出 separation ….分出公理図式 replacement ….置換公理図式

ZFC 公理ライブラリ

公理ライブラリを読み込んでいます…