定義
希爾伯特一貝爾奈斯命題演算系統(Hilbert- Bernays' system of propositional calculus)一種簡明的命題演算系統.由德國數學家希爾伯特 (Hilbert,D.)和德國學者貝爾奈斯(Bernays,P.)在 1934年出版的《數學的基礎》一書中提出的命題演算系統.該系統有五個基本聯結詞:“~”(蘊涵)， “邑，，(合取)"V”(析取)，“~”(等價)，“一”(否定).該系統與其他系統不同的顯著特徵是其公理按五個基本聯結詞分成五組.每組有三條公理，它刻畫了一個基本聯結詞的特徵.各組公理是相對獨立的，就是說，僅含某幾種聯結詞的定理公式可由與其對應的幾組公理推導出.該系統的公理如下: 1.關於蘊涵詞:
