Home > Research > Publications & Outputs > Yet another proof of Goedel's completeness theo...

Text available via DOI:

View graph of relations

Yet another proof of Goedel's completeness theorem for first-order classical logic

Research output: Working paperPreprint

Publication date11/10/2009
<mark>Original language</mark>English

Publication series

NamearXiv preprint arXiv:0910.2059


A Henkin-style proof of completeness of first-order classical logic is given with respect to a very small set (notably missing cut rule) of Genzten deduction rules for intuitionistic sequents. Insisting on sparing on derivation rules, satisfiability theorem is seen to need weaker assumptions than completeness theorem, the missing request being exactly the rule ~ p --> p, which gives a hint of intuitionism's motivations from a classical point of view. A bare treatment of standard, basic first-order syntax somehow more algebraic-flavoured than usual is also given.