Peirce's Law

From ProofWiki
Jump to: navigation, search

Contents

Theorem

Peirce's law is a formula in propositional logic that is commonly expressed in the following form:

$((p \implies q) \implies p) \vdash p$

or, which is equivalent:

$((p \implies q) \implies p) \implies p$

Peirce's law holds in classical propositional calculus, but not in intuitionistic propositional calculus. The precise axiom system that one chooses for classical propositional calculus determines whether Peirce's law is taken as an axiom or proven as a theorem.

Under the existential interpretation of logical graphs, Peirce's law is represented by means of the following formal equivalence or logical equation:

Peirce's Law 1.0 Splash Page.png


Strong Form of Peirce's Law

The logical implication does in fact go both ways:

$((p \implies q) \implies p) \dashv \vdash p$

or equivalently:

$((p \implies q) \implies p) \iff p$

Representing propositions as logical graphs under the existential interpretation, the strong form of Peirce's law is expressed by the following equation:

Peirce's Law Strong Form 1.0 Splash Page.png


Proof

Proof by Logical Graphs

First we show $((p \implies q) \implies p) \implies p$:

Using the axioms and theorems listed in the entry for logical graphs, Peirce's law may be proved in the following manner.

Peirce's Law 1.0 Marquee Title.png
Peirce's Law 1.0 Storyboard 1.png
Equational Inference Band Collect p.png
Peirce's Law 1.0 Storyboard 2.png
Equational Inference Band Quit ((q)).png
Peirce's Law 1.0 Storyboard 3.png
Equational Inference Band Cancel (( )).png
Peirce's Law 1.0 Storyboard 4.png
Equational Inference Band Delete p.png
Peirce's Law 1.0 Storyboard 5.png
Equational Inference Band Cancel (( )).png
Peirce's Law 1.0 Storyboard 6.png
Equational Inference Marquee QED.png

The steps of the proof are replayed in the following animation.

Peirce's Law 2.0 Animation.gif

Similarly, the strong form may be proved in the following manner:

Peirce's Law Strong Form 1.0 Marquee Title.png
Peirce's Law Strong Form 1.0 Storyboard 1.png
Equational Inference Rule Collect p.png
Peirce's Law Strong Form 1.0 Storyboard 2.png
Equational Inference Rule Quit ((q)).png
Peirce's Law Strong Form 1.0 Storyboard 3.png
Equational Inference Rule Cancel (( )).png
Peirce's Law Strong Form 1.0 Storyboard 4.png
Equational Inference Marquee QED.png

The following animation replays the steps of the proof.

Peirce's Law Strong Form 2.0 Animation.gif

Proof by Natural deduction

By the Tableau method:

$((p \implies q) \implies p) \vdash p$
Line Pool Formula Rule Depends upon Notes
1 1 $\left({p \implies q}\right) \implies p$ P (None)
2 $p \lor \lnot p$ LEM (None)
3 3 $\lnot p$ A (None) Either $p$ is false ...
4 3 $p \implies q$ Sequent Introduction 3 "If something's false, it implies anything."
5 1, 3 $p$ $\implies \mathcal E$ 1, 4
6 6 $p$ A (None) ... or it's true ...
7 1 $p$ $\lor \mathcal E$ 2, 3-5, 6-6 ... but either way it's true.

$\Box$

Now from Implication Properties, we have $p \vdash r \implies p$ which is equivalent to $p \implies (r \implies p)$.

Now we put a substitution instance of $p \implies q$ for $r$, and:

$p \implies ((p \implies q) \implies p)$

follows immediately.

$\blacksquare$


Proof by Truth Table

We can directly prove $((p \implies q) \implies p) \dashv \vdash p$.

We apply the Method of Truth Tables to the proposition.

As can be seen by inspection, the truth values under the main connectives match for all models.

$\begin{array}{|ccccc||c|}\hline ((p & \implies & q) & \implies & p) & p \\ \hline F & T & F & F & F & F \\ F & T & T & F & F & F \\ T & F & F & T & T & T \\ T & T & T & T & T & T \\ \hline \end{array}$


$\blacksquare$


Source of Name

This entry was named for Charles Sanders Peirce.


Comment

A non-obvious result that has the same strength as the Law of the Excluded Middle.

Consider $\left({\left({p \implies q}\right) \implies p}\right) \implies p$.

Now let $q = \bot$.

So we have $((p\implies \bot)\implies p)\implies p$.

What means $(\neg p\implies p)\implies p$. That is Consequentia Mirabilis.


Now let $q = p$.

So we have $((p\implies p)\implies p)\implies p$.



History

Here is Peirce's own statement and proof of the law:

A fifth icon is required for the principle of excluded middle and other propositions connected with it. One of the simplest formulae of this kind is:

$\{ (x \,-\!\!\!< y) \,-\!\!\!< x \} \,-\!\!\!< x.$

This is hardly axiomatical. That it is true appears as follows. It can only be false by the final consequent $x\!$ being false while its antecedent $(x \,-\!\!\!< y) \,-\!\!\!< x$ is true. If this is true, either its consequent, $x,\!$ is true, when the whole formula would be true, or its antecedent $x \,-\!\!\!< y$ is false. But in the last case the antecedent of $x \,-\!\!\!< y,$ that is $x,\!$ must be true. (Peirce, CP 3.384).

Peirce goes on to point out an immediate application of the law:

From the formula just given, we at once get:

$\{ (x \,-\!\!\!< y) \,-\!\!\!< a \} \,-\!\!\!< x,$

where the $a\!$ is used in such a sense that $(x \,-\!\!\!< y) \,-\!\!\!< a$ means that from $(x \,-\!\!\!< y)$ every proposition follows. With that understanding, the formula states the principle of excluded middle, that from the falsity of the denial of $x\!$ follows the truth of $x.\!$ (Peirce, CP 3.384).

Note. Peirce uses the sign of illation “$-\!\!\!<$” for implication. In one place he explains “$-\!\!\!<$” as a variant of the sign “$\le$” for less than or equal to; in another place he suggests that $A \,-\!\!\!< B$ is an iconic way of representing a state of affairs where $A,\!$ in every way that it can be, is $B.\!$


Bibliography

  • Peirce, Charles Sanders (1885), "On the Algebra of Logic : A Contribution to the Philosophy of Notation", American Journal of Mathematics 7 (1885), 180–202. Reprinted (CP 3.359–403), (CE 5, 162–190).
  • Peirce, Charles Sanders (1931–1935, 1958), Collected Papers of Charles Sanders Peirce, vols. 1–6, Charles Hartshorne and Paul Weiss (eds.), vols. 7–8, Arthur W. Burks (ed.), Harvard University Press, Cambridge, MA. Cited as (CP volume.paragraph).
  • Peirce, Charles Sanders (1981–), Writings of Charles S. Peirce : A Chronological Edition, Peirce Edition Project (eds.), Indiana University Press, Bloomington and Indianapolis, IN. Cited as (CE volume, page).


Sources

Personal tools
Namespaces
Variants
Actions
Navigation
ProofWiki.org
ToDo
Toolbox
Google AdSense