Soundness And Completeness
This chapter contains a proof that the basic tableau rules are sound and complete with respect to generalized Henkin models. Soundness is by the “usual” argument, is straightforward, and is what I begin with. Completeness is something else altogether. For that I use the ideas developed simultaneously in [Tak67, Pra68], where they were applied to give a non-constructive proof of a cut eliminat ion theorem.
Unable to display preview. Download preview PDF.