A simple strong completeness proof for sentential logic.
Charles M. Silver · Notre Dame Journal of Formal Logic · 1980
The following proof* is offered for any standard system of sentential logic whose language, X, consists of the sentence letters: P u P 2 , P 3 , . ..; the negation symbol: Ί; the material implication symbol: ->; and parentheses.(In terms of the two connectives 1 and -*, the other usual connectives can be defined in the standard way.)Sentences of «C ar e built up in the normal way.We use Greek letters: φ 9 ψ 9 0, X, and λ to range over sentences of £ and we use Γ and Δ (sometimes with subscripts and primes) to range over sets of sentences of JQ.A derivation in £ consists of a finite (non-empty) sequence of ordered pairs of the form (Γ', φ), such that Γ" is a finite set of sentences (premises) and φ has been obtained from Γ' according to whatever inference rules or axioms are specified for the system such that the eight metatheorems below hold in terms of the following definition of 'derivable': φ is derivable from Γ, denoted Γ h φ, just in case (Γ ; , φ) is an element of a derivation, where Γ" c Γ.These metatheorems are easily established for any standard system.Some of them are redundant, but it is convenient to list them in order to refer to them later.then Γhφ M5 If Γ'hφ and Γ' c Γ, then Γh φ M6 (a) // ΓU {lφ}hψ and ΓU {lφ}\-Ίψ, then Thφ (b) // ΓU {}HI// and ΓU {φjπiψ, then Γ f-Ίψ M7 IfThφ and Γ'hφ-* ψ, then ΓUΓhψ M8 Γt-ΊΊφiffΓ\-φ.*I wish to thank William Craig, Larry Davis, and Bill Edmundson, whose helpful suggestions improved the exposition of this proof.