after a contradiction symbol. In fact, this often occurs in a proof by contradiction to indicate that the original assumption was proved false—and hence that its negation must be true. The notion of contradiction in an axiomatic system and a proof of its consistency In general, a consistency proof requires the following two things: An axiomatic system A demonstration that it is not the case that both the formula p and its negation ~p can be derived in the system. But by whatever method one goes about it, all consistency proofs would seem to necessitate the primitive notion of contradiction. Moreover, it seems as if this notion would simultaneously have to be "outside" the formal system in the definition of tautology. When Emil Post, in his 1921 "Introduction to a General Theory of Elementary Propositions", extended his proof of the consistency of the propositional calculus (i.e. the logic) beyond that of Principia Mathematica (PM), he observed that with respect to a generalized set of postulates (i.e. axioms), he would no longer be able to automatically invoke the notion of "contradiction"such a notion might not be contained in the postulates: Post's solution to the problem is described in the demonstration "An Example of a Successful Absolute Proof of Consistency", offered by Ernest Nagel and James R. Newman in their 1958 Gödel's Proof. They too observed a problem with respect to the notion of "contradiction" with its usual "truth values" of "truth" and "falsity". They observed that: Given some "primitive formulas" such as PM's primitives S1 V S2 [inclusive OR] and ~S (negation), one is forced to define the axioms in terms of these primitive notions. In a thorough manner, Post demonstrates in PM, and defines (as do Nagel and Newman, see below) that the property of tautologous – as yet to be defined – is "inherited": if one begins with a set of tautologous axioms (postulates) and a deduction system that contains substitution and modus ponens, then a consistent system will yield only tautologous formulas. On the topic of the definition of tautologous, Nagel and Newman create two mutually exclusive and exhaustive classes K1 and K2, into which fall (the outcome of) the axioms when their variables (e.g. S1 and S2 are assigned from these classes). This also applies to the primitive formulas. For example: "A formula having the form S1 V S2 is placed into class K2, if both S1