Talk:Peirce's law - Revision history

Jon Awbrey: /* LaTeX Version */

2009-07-27T12:34:48Z

LaTeX Version

Jon Awbrey: delete worksheet

2008-06-27T01:26:47Z

delete worksheet

Jon Awbrey: /* Content from PlanetMath */ convert to wiki markup

2008-06-27T01:22:21Z

Content from PlanetMath: convert to wiki markup

Jon Awbrey: copy content from PlanetMath

2008-06-26T20:24:18Z

copy content from PlanetMath

New page

==Content from PlanetMath==

<pre>
\textbf{Peirce's law} is a proposition in propositional calculus that is commonly expressed in the following form:

\[ ((p \Rightarrow q) \Rightarrow p) \Rightarrow 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.

\section{History}

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

\begin{quote}
A \textit{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 \prec y) \prec x \} \prec 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 \prec y) \prec x$ is true. If this is true, either its consequent, $x$, is true, when the whole formula would be true, or its antecedent $x \prec y$ is false. But in the last case the antecedent of $x \prec y$, that is $x$, must be true. (Peirce, CP 3.384).
\end{quote}

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

\begin{quote}
From the formula just given, we at once get:

\[ \{ (x \prec y) \prec a \} \prec x, \]

where the $a$ is used in such a sense that $(x \prec y) \prec a$ means that from $(x \prec 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).
\end{quote}

\textbf{Note.} The above transcription uses the ``precedes sign" ($\prec$) for the ``sign of illation'' that Peirce customarily wrote as a cursive symbol somewhat like a gamma ($\gamma$) turned on its side or else typed as a bigram consisting of a dash and a ``less than" sign.

\section{Graphic proof}

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

\begin{verbatim}
o-----------------------------------------------------------o
| Peirce's Law. . . . . . . . . . . . . . . . . . . . . . . |
o-----------------------------------------------------------o
| . . . . . . . . . . . . . . . . . . . . . . . . . . . . . |
| . . . . p o---o q . . . . . . . . . . . . . . . . . . . . |
| . . . . . | . . . . . . . . . . . . . . . . . . . . . . . |
| . . . . . o---o p . . . . . . . . . . . . . . . . . . . . |
| . . . . . | . . . . . . . . . . . . . . . . . . . . . . . |
| . . . . . o---o p . . . . . . . . . . . . . . . . . . . . |
| . . . . . | . . . . . . . . . . . . . . . . . . . . . . . |
| . . . . . @ . . . . . . . . = . . . . . . . . . @ . . . . |
| . . . . . . . . . . . . . . . . . . . . . . . . . . . . . |
o-----------------------------------------------------------o
| . . . . . . . . . . . . . . . . . . . . . . . . . . . . . |
| . . .(((p (q)) (p)) (p))) . = . . . . . . . . . . . . . . |
| . . . . . . . . . . . . . . . . . . . . . . . . . . . . . |
o-----------------------------------------------------------o
\end{verbatim}

\textbf{Proof.} Using the axiom set given in the entry for logical graphs, Peirce's law may be proved in the following manner.

\begin{verbatim}
o-----------------------------------------------------------o
| Peirce's Law. . Proof . . . . . . . . . . . . . . . . . . |
o-----------------------------------------------------------o
| . . . . . . . . . . . . . . . . . . . . . . . . . . . . . |
| . . . . p o---o q . . . . . . . . . . . . . . . . . . . . |
| . . . . . | . . . . . . . . . . . . . . . . . . . . . . . |
| . . . . . o---o p . . . . . . . . . . . . . . . . . . . . |
| . . . . . | . . . . . . . . . . . . . . . . . . . . . . . |
| . . . . . o---o p . . . . . . . . . . . . . . . . . . . . |
| . . . . . | . . . . . . . . . . . . . . . . . . . . . . . |
| . . . . . @ . . . . . . . . . . . . . . . . . . . . . . . |
| . . . . . . . . . . . . . . . . . . . . . . . . . . . . . |
o==================================< Collect >==============o
| . . . . . . . . . . . . . . . . . . . . . . . . . . . . . |
| . . . . . o---o q . . . . . . . . . . . . . . . . . . . . |
| . . . . . | . . . . . . . . . . . . . . . . . . . . . . . |
| . . . . . o---o . . . . . . . . . . . . . . . . . . . . . |
| . . . . . | . . . . . . . . . . . . . . . . . . . . . . . |
| . . . . p o---o p . . . . . . . . . . . . . . . . . . . . |
| . . . . . | . . . . . . . . . . . . . . . . . . . . . . . |
| . . . . . @ . . . . . . . . . . . . . . . . . . . . . . . |
| . . . . . . . . . . . . . . . . . . . . . . . . . . . . . |
o==================================< Recess >===============o
| . . . . . . . . . . . . . . . . . . . . . . . . . . . . . |
| . . . . . o---o . . . . . . . . . . . . . . . . . . . . . |
| . . . . . | . . . . . . . . . . . . . . . . . . . . . . . |
| . . . . p o---o p . . . . . . . . . . . . . . . . . . . . |
| . . . . . | . . . . . . . . . . . . . . . . . . . . . . . |
| . . . . . @ . . . . . . . . . . . . . . . . . . . . . . . |
| . . . . . . . . . . . . . . . . . . . . . . . . . . . . . |
o==================================< Refold >===============o
| . . . . . . . . . . . . . . . . . . . . . . . . . . . . . |
| . . . . p o---o p . . . . . . . . . . . . . . . . . . . . |
| . . . . . | . . . . . . . . . . . . . . . . . . . . . . . |
| . . . . . @ . . . . . . . . . . . . . . . . . . . . . . . |
| . . . . . . . . . . . . . . . . . . . . . . . . . . . . . |
o==================================< Delete >===============o
| . . . . . . . . . . . . . . . . . . . . . . . . . . . . . |
| . . . . . o---o . . . . . . . . . . . . . . . . . . . . . |
| . . . . . | . . . . . . . . . . . . . . . . . . . . . . . |
| . . . . . @ . . . . . . . . . . . . . . . . . . . . . . . |
| . . . . . . . . . . . . . . . . . . . . . . . . . . . . . |
o==================================< Refold >===============o
| . . . . . . . . . . . . . . . . . . . . . . . . . . . . . |
| . . . . . @ . . . . . . . . . . . . . . . . . . . . . . . |
| . . . . . . . . . . . . . . . . . . . . . . . . . . . . . |
o==================================< QED >==================o
\end{verbatim}

\section{Bibliography}

\begin{itemize}
\item
Peirce, Charles Sanders (1885), ``On the Algebra of Logic : A Contribution to the Philosophy of Notation", \textit{American Journal of Mathematics} 7 (1885), 180--202. Reprinted (CP 3.359--403), (CE 5, 162--190).
\item
Peirce, Charles Sanders (1931--1935, 1958), \textit{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).
\item
Peirce, Charles Sanders (1981--), \textit{Writings of Charles S. Peirce : A Chronological Edition}, Peirce Edition Project (eds.), Indiana University Press, Bloomington and Indianapolis, IN. Cited as (CE volume, page).
\end{itemize}
</pre>

← Older revision		Revision as of 12:34, 27 July 2009
Line 1:		Line 1:
	==Notes & Queries==		==Notes & Queries==

−	[[~~User~~:~~Jon Awbrey\|Jon Awbrey~~]] 18:26, ~~26 June 2008~~ (~~PDT~~)	+	==Place for Discussion==
		+
		+	==LaTeX Version==
		+
		+	<pre>
		+	\PMlinkescapeword{algebra}
		+	\PMlinkescapeword{Algebra}
		+	\PMlinkescapeword{application}
		+	\PMlinkescapeword{Application}
		+	\PMlinkescapeword{calculus}
		+	\PMlinkescapeword{Calculus}
		+	\PMlinkescapeword{chooses}
		+	\PMlinkescapeword{Chooses}
		+	\PMlinkescapeword{connected}
		+	\PMlinkescapeword{Connected}
		+	\PMlinkescapeword{ma}
		+	\PMlinkescapeword{MA}
		+	\PMlinkescapeword{place}
		+	\PMlinkescapeword{Place}
		+	\PMlinkescapeword{point}
		+	\PMlinkescapeword{Point}
		+	\PMlinkescapeword{project}
		+	\PMlinkescapeword{Project}
		+	\PMlinkescapeword{qed}
		+	\PMlinkescapeword{QED}
		+	\PMlinkescapeword{side}
		+	\PMlinkescapeword{Side}
		+	\PMlinkescapeword{states}
		+	\PMlinkescapeword{States}
		+	\PMlinkescapeword{strong}
		+	\PMlinkescapeword{Strong}
		+	\PMlinkescapeword{stronger}
		+	\PMlinkescapeword{Stronger}
		+	\PMlinkescapeword{volume}
		+	\PMlinkescapeword{Volume}
		+
		+	\textbf{Peirce's law} is a formula in propositional calculus that is commonly expressed in the following form:
		+
		+	\[ ((p \Rightarrow q) \Rightarrow p) \Rightarrow 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.
		+
		+	\tableofcontents
		+
		+	\section{History}
		+
		+	Here is Peirce's own statement and proof of the law:
		+
		+	\begin{quote}
		+	A \textit{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).
		+	\end{quote}
		+
		+	Peirce goes on to point out an immediate application of the law:
		+
		+	\begin{quote}
		+	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).
		+	\end{quote}
		+
		+	\textbf{Note.} Peirce uses the ``sign of illation'' ($-\!\!\!<$) for implication. In one place he explains it as a variant of the sign ($\le$) for ``less than or equal to''; in another place he suggests reading $A \,-\!\!\!< B$ as ``$A$, in every way that it can be, is $B$''.
		+
		+	\section{Graphical proof}
		+
		+	Representing \PMlinkname{propositions}{PropositionalCalculus} as \PMlinkname{logical graphs}{LogicalGraph} under the \PMlinkname{existential interpretation}{LogicalGraphFormalDevelopment}, Peirce's law is expressed by means of the following formal equation:
		+
		+	\begin{center}\begin{tabular}{cc}
		+	\includegraphics[scale=0.8]{PeircesLawFigure1} & (1) \\
		+	\end{tabular}\end{center}
		+
		+	\textbf{Proof.} Using the axiom set given in the entry for \PMlinkname{logical graphs}{LogicalGraph}, Peirce's law may be proved in the following manner.
		+
		+	\begin{center}\begin{tabular}{cc}
		+	\includegraphics[scale=0.8]{PeircesLawFigure2} & (2) \\
		+	\end{tabular}\end{center}
		+
		+	\section{Equational form}
		+
		+	A stronger form of Peirce's law also holds, in which the final implication is observed to be reversible:
		+
		+	\[ ((p \Rightarrow q) \Rightarrow p) \Leftrightarrow p \]
		+
		+	\subsection{Proof 1}
		+
		+	Given what precedes, it remains to show that:
		+
		+	\[ p \Rightarrow ((p \Rightarrow q) \Rightarrow p) \]
		+
		+	But this is immediate, since $p \Rightarrow (r \Rightarrow p)$ for any proposition $r.$
		+
		+	\subsection{Proof 2}
		+
		+	Representing \PMlinkname{propositions}{PropositionalCalculus} as \PMlinkname{logical graphs}{LogicalGraph} under the \PMlinkname{existential interpretation}{LogicalGraphFormalDevelopment}, the strong form of Peirce's law is expressed by the following equation:
		+
		+	\begin{center}\begin{tabular}{cc}
		+	\includegraphics[scale=0.8]{PeircesLawFigure3} & (3) \\
		+	\end{tabular}\end{center}
		+
		+	Using the axioms and theorems listed in the entries on \PMlinkname{logical graphs}{LogicalGraph}, the equational form of Peirce's law may be proved in the following manner:
		+
		+	\begin{center}\begin{tabular}{cc}
		+	\includegraphics[scale=0.8]{PeircesLawFigure4} & (4) \\
		+	\end{tabular}\end{center}
		+
		+	\section{Bibliography}
		+
		+	\begin{itemize}
		+	\item
		+	Peirce, Charles Sanders (1885), ``On the Algebra of Logic : A Contribution to the Philosophy of Notation", \textit{American Journal of Mathematics} 7 (1885), 180--202. Reprinted (CP 3.359--403), (CE 5, 162--190).
		+	\item
		+	Peirce, Charles Sanders (1931--1935, 1958), \textit{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).
		+	\item
		+	Peirce, Charles Sanders (1981--), \textit{Writings of Charles S. Peirce : A Chronological Edition}, Peirce Edition Project (eds.), Indiana University Press, Bloomington and Indianapolis, IN. Cited as (CE volume, page).
		+	\end{itemize}
		+	</pre>

← Older revision		Revision as of 01:26, 27 June 2008
Line 1:		Line 1:
−	=~~Content from PlanetMath~~=	+	==Notes & Queries==

−	~~'''Peirce's law''' is a proposition in~~ [[~~propositional calculus]] that is commonly expressed in the following form:~~	+	[[User:Jon Awbrey\|Jon Awbrey]] 18:26, 26 June 2008 (PDT)
−
−	~~<p><center><math>((p \Rightarrow q) \Rightarrow p) \Rightarrow p</math></center></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.
−
−	~~==History==~~
−
−	~~Here is Peirce's own statement and proof of the law:~~
−
−	~~<blockquote>~~
−	~~<p>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:</p>~~
−
−	~~<p><center><math>\{ (x \prec y) \prec x \} \prec x.</math></center></p>~~
−
−	<p>This is hardly axiomatical. That it is true appears as follows. It can only be false by the final consequent <math>x\!</math> being false while its antecedent <math>(x \prec y) \prec x</math> is true. If this is true, either its consequent, <math>x,\!</math> is true, when the whole formula would be true, or its antecedent <math>x \prec y</math> is false. But in the last case the antecedent of <math>x \prec y,</math> that is <math>x,\!</math> must be true. (Peirce, CP 3.384).</p>
−	~~</blockquote>~~
−
−	~~Peirce goes on to point out an immediate application of the law~~:
−
−	~~<blockquote>~~
−	~~<p>From the formula just given, we at once get:</p>~~
−
−	~~<p><center><math>\{ (x \prec y) \prec a \} \prec x,</math></center></p>~~
−
−	<p>where the <math>a\!</math> is used in such a sense that <math>(x \prec y) \prec a</math> means that from <math>(x \prec y)</math> every proposition follows. With that understanding, the formula states the principle of excluded middle, that from the falsity of the denial of <math>x\!</math> follows the truth of <math>x.\!</math> (Peirce, CP 3.384).</p>
−	~~</blockquote>~~
−
−	'''Note.''' The above transcription uses the "precedes sign" (<math>\prec</math>) for the "sign of illation" that Peirce customarily wrote as a cursive symbol somewhat like a gamma (<math>\gamma\!</math>) turned on its side or else typed as a bigram consisting of a dash and a "less than" sign.
−
−	~~==Graphic proof==~~
−
−	~~Under the existential interpretation of Peirce's [[logical graphs]], Peirce's law is represented by means of the following formal equivalence or logical equation.~~
−
−	~~<blockquote><pre>~~
−	~~o-----------------------------------------------------------o~~
−	~~\| Peirce's Law. . . . . . . . . . . . . . . . . . . . . . . \|~~
−	~~o-----------------------------------------------------------o~~
−	~~\| . . . . . . . . . . . . . . . . . . . . . . . . . . . . . \|~~
−	~~\| . . . . p o---o q . . . . . . . . . . . . . . . . . . . .~~ \|
−	~~\| . . . . . \| . . . . . . . . . . . . . . . . . . . . . . . \|~~
−	~~\| . . . . . o---o p . . . . . . . . . . . . . . . . . . . . \|~~
−	~~\| . . . . . \| . . . . . . . . . . . . . . . . . . . . . . . \|~~
−	~~\| . . . . . o---o p . . . . . . . . . . . . . . . . . . . . \|~~
−	~~\| . . . . . \| . . . . . . . . . . . . . . . . . . . . . . . \|~~
−	~~\| . . . . . @ . . . . . . . . = . . . . . . . . . @ . . . . \|~~
−	~~\| . . . . . . . . . . . . . . . . . . . . . . . . . . . . . \|~~
−	~~o-----------------------------------------------------------o~~
−	~~\| . . . . . . . . . . . . . . . . . . . . . . . . . . . . . \|~~
−	~~\| . . .(((p (q)) (p)) (p))) . = . . . . . . . . . . . . . . \|~~
−	~~\| . . . . . . . . . . . . . . . . . . . . . . . . . . . . . \|~~
−	~~o-----------------------------------------------------------o~~
−	~~</pre></blockquote>~~
−
−	~~'''Proof.''' Using the axiom set given in the entry for [[logical graphs~~]]~~, Peirce's law may be proved in the following manner.~~
−
−	~~<blockquote><pre>~~
−	~~o-----------------------------------------------------------o~~
−	~~\| Peirce's Law. . Proof . . . . . . . . . . . . . . . . . . \|~~
−	~~o-----------------------------------------------------------o~~
−	~~\| . . . . . . . . . . . . . . . . . . . . . . . . . . . . . \|~~
−	~~\| . . . . p o---o q . . . . . . . . . . . . . . . . . . . . \|~~
−	~~\| . . . . . \| . . . . . . . . . . . . . . . . . . . . . . . \|~~
−	~~\| . . . . . o---o p . . . . . . . . . . . . . . . . . . . . \|~~
−	~~\| . . . . . \| . . . . . . . . . . . . . . . . . . . . . . . \|~~
−	~~\| . . . . . o---o p . . . . . . . . . . . . . . . . . . . . \|~~
−	~~\| . . . . . \| . . . . . . . . . . . . . . . . . . . . . . . \|~~
−	~~\| . . . . . @ . . . . . . . . . . . . . . . . . . . . . . . \|~~
−	~~\| . . . . . . . . . . . . . . . . . . . . . . . . . . . . . \|~~
−	~~o==================================< Collect >==============o~~
−	~~\| . . . . . . . . . . . . . . . . . . . . . . . . . . . . . \|~~
−	~~\| . . . . . o---o q . . . . . . . . . . . . . . . . . . . . \|~~
−	~~\| . . . . . \| . . . . . . . . . . . . . . . . . . . . . . . \|~~
−	~~\| . . . . . o---o . . . . . . . . . . . . . . . . . . . . . \|~~
−	~~\| . . . . . \| . . . . . . . . . . . . . . . . . . . . . . . \|~~
−	~~\| . . . . p o---o p . . . . . . . . . . . . . . . . . . . . \|~~
−	~~\| . . . . . \| . . . . . . . . . . . . . . . . . . . . . . . \|~~
−	~~\| . . . . . @ . . . . . . . . . . . . . . . . . . . . . . . \|~~
−	~~\| . . . . . . . . . . . . . . . . . . . . . . . . . . . . . \|~~
−	~~o==================================< Recess >===============o~~
−	~~\| . . . . . . . . . . . . . . . . . . . . . . . . . . . . . \|~~
−	~~\| . . . . . o---o . . . . . . . . . . . . . . . . . . . . . \|~~
−	~~\| . . . . . \| . . . . . . . . . . . . . . . . . . . . . . . \|~~
−	~~\| . . . . p o---o p . . . . . . . . . . . . . . . . . . . . \|~~
−	~~\| . . . . . \| . . . . . . . . . . . . . . . . . . . . . . . \|~~
−	~~\| . . . . . @ . . . . . . . . . . . . . . . . . . . . . . . \|~~
−	~~\| . . . . . . . . . . . . . . . . . . . . . . . . . . . . . \|~~
−	~~o==================================< Refold >===============o~~
−	~~\| . . . . . . . . . . . . . . . . . . . . . . . . . . . . . \|~~
−	~~\| . . . . p o---o p . . . . . . . . . . . . . . . . . . . . \|~~
−	~~\| . . . . . \| . . . . . . . . . . . . . . . . . . . . . . . \|~~
−	~~\| . . . . . @ . . . . . . . . . . . . . . . . . . . . . . . \|~~
−	~~\| . . . . . . . . . . . . . . . . . . . . . . . . . . . . . \|~~
−	~~o==================================< Delete >===============o~~
−	~~\| . . . . . . . . . . . . . . . . . . . . . . . . . . . . . \|~~
−	~~\| . . . . . o---o . . . . . . . . . . . . . . . . . . . . . \|~~
−	~~\| . . . . . \| . . . . . . . . . . . . . . . . . . . . . . . \|~~
−	~~\| . . . . . @ . . . . . . . . . . . . . . . . . . . . . . . \|~~
−	~~\| . . . . . . . . . . . . . . . . . . . . . . . . . . . . . \|~~
−	~~o==================================< Refold >===============o~~
−	~~\| . . . . . . . . . . . . . . . . . . . . . . . . . . . . . \|~~
−	~~\| . . . . . @ . . . . . . . . . . . . . . . . . . . . . . . \|~~
−	~~\| . . . . . . . . . . . . . . . . . . . . . . . . . . . . . \|~~
−	~~o==================================< QED >==================o~~
−	~~</pre></blockquote>~~
−
−	~~==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).

@@ Line 1: / Line 1: @@
-==Content from PlanetMath==
+=Content from PlanetMath=
-<pre>
+'''Peirce's law''' is a proposition in [[propositional calculus]] that is commonly expressed in the following form:
-\[ ((p \Rightarrow q) \Rightarrow p) \Rightarrow p \]
+<p><center><math>((p \Rightarrow q) \Rightarrow p) \Rightarrow p</math></center></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.
-\section{History}
+==History==
 Here is Peirce's own statement and proof of the law:
-\begin{quote}
+<blockquote>
-A \textit{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:
+<p>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:</p>
-\[ \{ (x \prec y) \prec x \} \prec x. \]
+<p><center><math>\{ (x \prec y) \prec x \} \prec x.</math></center></p>
-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 \prec y) \prec x$ is true.  If this is true, either its consequent, $x$, is true, when the whole formula would be true, or its antecedent $x \prec y$ is false.  But in the last case the antecedent of $x \prec y$, that is $x$, must be true.  (Peirce, CP 3.384).
+<p>This is hardly axiomatical.  That it is true appears as follows.  It can only be false by the final consequent <math>x\!</math> being false while its antecedent <math>(x \prec y) \prec x</math> is true.  If this is true, either its consequent, <math>x,\!</math> is true, when the whole formula would be true, or its antecedent <math>x \prec y</math> is false.  But in the last case the antecedent of <math>x \prec y,</math> that is <math>x,\!</math> must be true.  (Peirce, CP&nbsp;3.384).</p>
-\end{quote}
+</blockquote>
 Peirce goes on to point out an immediate application of the law:
-\begin{quote}
+<blockquote>
-From the formula just given, we at once get:
+<p>From the formula just given, we at once get:</p>
-\[ \{ (x \prec y) \prec a \} \prec x, \]
+<p><center><math>\{ (x \prec y) \prec a \} \prec x,</math></center></p>
-where the $a$ is used in such a sense that $(x \prec y) \prec a$ means that from $(x \prec 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).
+<p>where the <math>a\!</math> is used in such a sense that <math>(x \prec y) \prec a</math> means that from <math>(x \prec y)</math> every proposition follows.  With that understanding, the formula states the principle of excluded middle, that from the falsity of the denial of <math>x\!</math> follows the truth of <math>x.\!</math>  (Peirce, CP&nbsp;3.384).</p>
-\end{quote}
+</blockquote>
-\textbf{Note.}  The above transcription uses the ``precedes sign" ($\prec$) for the ``sign of illation'' that Peirce customarily wrote as a cursive symbol somewhat like a gamma ($\gamma$) turned on its side or else typed as a bigram consisting of a dash and a ``less than" sign.
+'''Note.'''  The above transcription uses the "precedes sign" (<math>\prec</math>) for the "sign of illation" that Peirce customarily wrote as a cursive symbol somewhat like a gamma (<math>\gamma\!</math>) turned on its side or else typed as a bigram consisting of a dash and a "less than" sign.
-\section{Graphic proof}
+==Graphic proof==
-Under the existential interpretation of Peirce's logical graphs, Peirce's law is represented by means of the following formal equivalence or logical equation.
+Under the existential interpretation of Peirce's [[logical graphs]], Peirce's law is represented by means of the following formal equivalence or logical equation.
-\begin{verbatim}
+<blockquote><pre>
 o-----------------------------------------------------------o
 | Peirce's Law. . . . . . . . . . . . . . . . . . . . . . . |
@@ Line 54: / Line 53: @@
 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . |
 o-----------------------------------------------------------o
-\end{verbatim}
+</pre></blockquote>
-\textbf{Proof.}  Using the axiom set given in the entry for logical graphs, Peirce's law may be proved in the following manner.
+'''Proof.'''  Using the axiom set given in the entry for [[logical graphs]], Peirce's law may be proved in the following manner.
-\begin{verbatim}
+<blockquote><pre>
 o-----------------------------------------------------------o
 | Peirce's Law. . Proof . . . . . . . . . . . . . . . . . . |
@@ Line 106: / Line 105: @@
 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . |
 o==================================< QED >==================o
-\end{verbatim}
+</pre></blockquote>
-\section{Bibliography}
+==Bibliography==
-\begin{itemize}
+* Peirce, Charles Sanders (1885), "On the Algebra of Logic : A Contribution to the Philosophy of Notation", ''American Journal of Mathematics'' 7 (1885), 180&ndash;202.  Reprinted (CP&nbsp;3.359&ndash;403), (CE&nbsp;5, 162&ndash;190).
-\item
-Peirce, Charles Sanders (1885), ``On the Algebra of Logic : A Contribution to the Philosophy of Notation", \textit{American Journal of Mathematics} 7 (1885), 180--202.  Reprinted (CP 3.359--403), (CE 5, 162--190).
+* Peirce, Charles Sanders (1931&ndash;1935, 1958), ''Collected Papers of Charles Sanders Peirce'', vols. 1&ndash;6, Charles Hartshorne and Paul Weiss (eds.), vols. 7&ndash;8, Arthur W. Burks (ed.), Harvard University Press, Cambridge, MA.  Cited as (CP&nbsp;volume.paragraph).
-\item
-Peirce, Charles Sanders (1931--1935, 1958), \textit{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&ndash;), ''Writings of Charles S. Peirce : A Chronological Edition'', Peirce Edition Project (eds.), Indiana University Press, Bloomington and Indianapolis, IN.  Cited as (CE&nbsp;volume,&nbsp;page).