Part of a series on |
Charles Sanders Peirce |
---|
![]() |
Pragmatism in epistemology |
Logic |
Semiotic theory |
Miscellaneous contributions |
Biographical |
In logic, Peirce's law is named after the philosopher and logician Charles Sanders Peirce. It was taken as an axiom in his first axiomatisation of propositional logic. It can be thought of as the law of excluded middle written in a form that involves only one sort of connective, namely implication.
In propositional calculus, Peirce's law says that ((P→Q)→P)→P. Written out, this means that P must be true if there is a proposition Q such that the truth of P follows from the truth of "if P then Q".
Peirce's law does not hold in intuitionistic logic or intermediate logics and cannot be deduced from the deduction theorem alone.
Under the Curry–Howard isomorphism, Peirce's law is the type of continuation operators, e.g. call/cc in Scheme. [1]
Here is Peirce's own statement of the law:
{(x ⤙ y) ⤙ x} ⤙ x. |
Peirce goes on to point out an immediate application of the law:
{(x ⤙ y) ⤙ a} ⤙ x, |
Warning: As explained in the text, "a" here does not denote a propositional atom, but something like the quantified propositional formula . The formula ((x → y) → a) → x would not be a tautology if a were interpreted as an atom.
In intuitionistic logic, if is proven or rejected, or if is provenly valid, then Piece's law for the two propositions holds. But the law's special case when is rejected, called consequentia mirabilis, is equivalent to excluded middle already over minimal logic. This also means that Piece's law entails classical logic over intuitionistic logic. Intuitionistically, not even the constraint implies the law for two propositions. Postulating the latter to be valid results in Smetanich's intermediate logic.
One proof of excluded middle from Piece's law directly is as follows: If is given, one has the equivalence . So is also equivalent to . Taking a contraposition, one finds Piece's law to be equivalent to . For , the latter simplifies to , the double-negation elimination principle. To conclude the proof, note that here the double-negated excluded middle is always already valid.
In the other direction, one can intuitionistically show that Piece's law follows from excluded middle. Using the principle of explosion, the latter may be expressed as . In words, this may be expressed as: "Every proposition either holds or implies any other proposition." Now to prove the law, note that is derivable from just implication introduction on the one hand and modus ponens on the other. Finally, in place of consider .
Another proof of the law in classical logic proceeds by passing through the classically valid reverse disjunctive syllogism twice: First note that is implied by , which is intuitionistically equivalent to . Now explosion entails that implies , and using excluded middle for entails that these two are in fact equivalent. Taken together, this means that in classical logic is equivalent to .
Peirce's law allows one to enhance the technique of using the deduction theorem to prove theorems. Suppose one is given a set of premises Γ and one wants to deduce a proposition Z from them. With Peirce's law, one can add (at no cost) additional premises of the form Z→P to Γ. For example, suppose we are given P→Z and (P→Q)→Z and we wish to deduce Z so that we can use the deduction theorem to conclude that (P→Z)→(((P→Q)→Z)→Z) is a theorem. Then we can add another premise Z→Q. From that and P→Z, we get P→Q. Then we apply modus ponens with (P→Q)→Z as the major premise to get Z. Applying the deduction theorem, we get that (Z→Q)→Z follows from the original premises. Then we use Peirce's law in the form ((Z→Q)→Z)→Z and modus ponens to derive Z from the original premises. Then we can finish off proving the theorem as we originally intended.
| 1. hypothesis |
| 2. hypothesis |
| 3. hypothesis |
| 4. hypothesis |
| 5. modus ponens using steps 4 and 1 |
| 6. modus ponens using steps 5 and 3 |
| 7. deduction from 4 to 6 |
| 8. modus ponens using steps 7 and 2 |
| 9. deduction from 3 to 8 |
| 10. Peirce's law |
| 11. modus ponens using steps 9 and 10 |
| 12. deduction from 2 to 11 |
(P→Z)→(((P→Q)→Z)→Z) | 13. deduction from 1 to 12 QED |
One reason that Peirce's law is important is that it can substitute for the law of excluded middle in the logic which only uses implication. The sentences which can be deduced from the axiom schemas:
(where P,Q,R contain only "→" as a connective) are all the tautologies which use only "→" as a connective.
Since Peirce's law implies the law of the excluded middle, it must always fail in non-classical intuitionistic logics. A simple explicit counterexample is that of Gödel many valued logics, which are a fuzzy logic where truth values are real numbers between 0 and 1, with material implication defined by:
and where Peirce's law as a formula can be simplified to:
where it always being true would be equivalent to the statement that u > v implies u = 1, which is true only if 0 and 1 are the only allowed values. At the same time however, the expression cannot ever be equal to the bottom truth value of the logic and its double negation is always true.
In classical logic, disjunctive syllogism is a valid argument form which is a syllogism having a disjunctive statement for one of its premises.
In logic, the law of excluded middle or the principle of excluded middle states that for every proposition, either this proposition or its negation is true. It is one of the three laws of thought, along with the law of noncontradiction, and the law of identity; however, no system of logic is built on just these laws, and none of these laws provides inference rules, such as modus ponens or De Morgan's laws. The law is also known as the law / principleof the excluded third, in Latin principium tertii exclusi. Another Latin designation for this law is tertium non datur or "no third [possibility] is given". In classical logic, the law is a tautology.
In logic, a logical connective is a logical constant. Connectives can be used to connect logical formulas. For instance in the syntax of propositional logic, the binary connective can be used to join the two atomic formulas and , rendering the complex formula .
The propositional calculus is a branch of logic. It is also called propositional logic, statement logic, sentential calculus, sentential logic, or sometimes zeroth-order logic. It deals with propositions and relations between propositions, including the construction of arguments based on them. Compound propositions are formed by connecting propositions by logical connectives representing the truth functions of conjunction, disjunction, implication, equivalence, and negation. Some sources include other connectives, as in the table below.
In logic, proof by contradiction is a form of proof that establishes the truth or the validity of a proposition, by showing that assuming the proposition to be false leads to a contradiction. Although it is quite freely used in mathematical proofs, not every school of mathematical thought accepts this kind of nonconstructive proof as universally valid.
In propositional logic and Boolean algebra, De Morgan's laws, also known as De Morgan's theorem, are a pair of transformation rules that are both valid rules of inference. They are named after Augustus De Morgan, a 19th-century British mathematician. The rules allow the expression of conjunctions and disjunctions purely in terms of each other via negation.
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 logic, negation, also called the logical not or logical complement, is an operation that takes a proposition to another proposition "not ", standing for " is not true", written , or . It is interpreted intuitively as being true when is false, and false when is true. Negation is thus a unary logical connective. It may be applied as an operation on notions, propositions, truth values, or semantic values more generally. In classical logic, negation is normally identified with the truth function that takes truth to falsity. In intuitionistic logic, according to the Brouwer–Heyting–Kolmogorov interpretation, the negation of a proposition is the proposition whose proofs are the refutations of .
Intuitionistic logic, sometimes more generally called constructive logic, refers to systems of symbolic logic that differ from the systems used for classical logic by more closely mirroring the notion of constructive proof. In particular, systems of intuitionistic logic do not assume the law of the excluded middle and double negation elimination, which are fundamental inference rules in classical logic.
In mathematics, constructive analysis is mathematical analysis done according to some principles of constructive mathematics.
In mathematical logic, sequent calculus is a style of formal logical argumentation in which every line of a proof is a conditional tautology instead of an unconditional tautology. Each conditional tautology is inferred from other conditional tautologies on earlier lines in a formal argument according to rules and procedures of inference, giving a better approximation to the natural style of deduction used by mathematicians than to David Hilbert's earlier style of formal logic, in which every line was an unconditional tautology. More subtle distinctions may exist; for example, propositions may implicitly depend upon non-logical axioms. In that case, sequents signify conditional theorems in a first-order language rather than conditional tautologies.
In mathematics, a Heyting algebra (also known as pseudo-Boolean algebra) is a bounded lattice (with join and meet operations written ∨ and ∧ and with least element 0 and greatest element 1) equipped with a binary operation a → b of implication such that (c ∧ a) ≤ b is equivalent to c ≤ (a → b). From a logical standpoint, A → B is by this definition the weakest proposition for which modus ponens, the inference rule A → B, A ⊢ B, is sound. Like Boolean algebras, Heyting algebras form a variety axiomatizable with finitely many equations. Heyting algebras were introduced by Arend Heyting (1930) to formalize intuitionistic logic.
In propositional logic, double negation is the theorem that states that "If a statement is true, then it is not the case that the statement is not true." This is expressed by saying that a proposition A is logically equivalent to not (not-A), or by the formula A ≡ ~(~A) where the sign ≡ expresses logical equivalence and the sign ~ expresses negation.
Paraconsistent logic is an attempt at a logical system to deal with contradictions in a discriminating way. Alternatively, paraconsistent logic is the subfield of logic that is concerned with studying and developing "inconsistency-tolerant" systems of logic, which reject the principle of explosion.
In mathematical logic, Heyting arithmetic is an axiomatization of arithmetic in accordance with the philosophy of intuitionism. It is named after Arend Heyting, who first proposed it.
In mathematics, a set is inhabited if there exists an element .
Consequentia mirabilis, also known as Clavius's Law, is used in traditional and classical logic to establish the truth of a proposition from the inconsistency of its negation. It is thus related to reductio ad absurdum, but it can prove a proposition using just its own negation and the concept of consistency. For a more concrete formulation, it states that if a proposition is a consequence of its negation, then it is true, for consistency. In formal notation:
In logic, especially mathematical logic, a Hilbert system, sometimes called Hilbert calculus, Hilbert-style deductive system or Hilbert–Ackermann system, is a type of system of formal deduction attributed to Gottlob Frege and David Hilbert. These deductive systems are most often studied for first-order logic, but are of interest for other logics as well.
In logic and mathematics, contraposition refers to the inference of going from a conditional statement into its logically equivalent contrapositive, and an associated proof method known as proof by contraposition. The contrapositive of a statement has its antecedent and consequent inverted and flipped.
Minimal logic, or minimal calculus, is a symbolic logic system originally developed by Ingebrigt Johansson. It is an intuitionistic and paraconsistent logic, that rejects both the law of the excluded middle as well as the principle of explosion, and therefore holding neither of the following two derivations as valid: