論理式の集合\Gammaと、と論理式\varphiが与えられたとき、

\Gammaに属する論理式と、公理から、

有限回の推論で\varphiに至る論証があるとき\varphiは\Gammaから証明可能である、という

\Gamma\vdash \varphiと表記する

\Gammaは公理系

\Gammaは空集合でも、有限集合でも無限集合でも良い

ref 論理学に関する記号とその意味

\Gammaから\varphiが導出できるとき、\Gamma\vdash\varphiと書く

解消されていない仮定が全て\Gammaに属している

結論が\varphiである導出図が存在する

ことが満たされる

定義

\varphiは論理式

論理式の有限列\varphi_1,\cdots,\varphi_n=\varphiは以下の条件を満たしているとする

各\varphi_i\in \top

各\varphi_iは公理

\varphi_kは\varphi_iと\varphi_jからの形式的推論

ただしi,j\lt k

このとき論理式の有限列\varphi_1,\cdots,\varphi_nを\varphiの証明という

証明が存在する論理式を「証明可能な論理式」という

\Gamma\vdash \varphiと書く

例が欲しいっす

参考