In traditional logic, a contradiction occurs when a proposition conflicts either with itself or established fact. It is often used as a tool to detect disingenuous beliefs and bias. Illustrating a general tendency in applied logic, Aristotle's law of noncontradiction states that "It is impossible that the same thing can at the same time both belong and not belong to the same object and in the same respect." In modern formal logic and type theory, the term is mainly used instead for a single proposition, often denoted by the falsum symbol ; a proposition is a contradiction if false can be derived from it, using the rules of the logic. It is a proposition that is unconditionally false (i.e., a self-contradictory proposition). This can be generalized to a collection of propositions, which is then said to "contain" a contradiction. History By creation of a paradox, Plato's Euthydemus dialogue demonstrates the need for the notion of contradiction. In the ensuing dialogue, Dionysodorus denies the existence of "contradiction", all the while that Socrates is contradicting him: Indeed, Dionysodorus agrees that "there is no such thing as false opinion ... there is no such thing as ignorance", and demands of Socrates to "Refute me." Socrates responds "But how can I refute you, if, as you say, to tell a falsehood is impossible?". In formal logic In classical logic, particularly in propositional and first-order logic, a proposition is a contradiction if and only if . Since for contradictory it is true that for all (because ), one may prove any proposition from a set of axioms which contains contradictions. This is called the "principle of explosion", or "ex falso quodlibet" ("from falsity, anything follows"). In a complete logic, a formula is contradictory if and only if it is unsatisfiable. Proof by contradiction For a set of consistent premises and a proposition , it is true in classical logic that (i.e., proves ) if and only if (i.e., and leads to a contradiction). Therefore, a proof that also proves that is true under the premises . The use of this fact forms the basis of a proof technique called proof by contradiction, which mathematicians use extensively to establish the validity of a wide range of theorems. This applies only in a logic where the law of excluded middle is accepted as an axiom. Using minimal logic, a logic with similar axioms to classical logic but