 Case 1: For some n, φn is not satisfiable. Then, Gödel argued, using the already known completeness theorem for propositional  logic,[7]  that ¬φn is provable, and hence so is ∀x0,…, xn+1¬φn. Thus ¬∃x0…∃xn+1φn is provable and therefore the ¬φ is provable, i.e., φ is refutable in the Hilbert-Ackermann system. (Some partial results about propositional logic in addition to those already mentioned include the semantic completeness of the propositional calculus due to Post (1921), as well as a more general completeness theorem for the same due to Bernays in 1918; the latter appears in Bernays’ unpublished Habilitationsschrift of 1918; see also Bernays 1926.)