\documentclass[12pt,titlepage]{article}

\usepackage{amsmath}
\usepackage{mathrsfs}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{amsthm}
\usepackage{mathtools}
\usepackage{graphicx}
\usepackage{color}
\usepackage{ucs}
\usepackage[utf8x]{inputenc}
\usepackage{xparse}
\usepackage{hyperref}

%----Macros----------
%
% Unresolved issues:
%
%  \righttoleftarrow
%  \lefttorightarrow
%
%  \color{} with HTML colorspec
%  \bgcolor
%  \array with options (without options, it's equivalent to the matrix environment)

% Of the standard HTML named colors, white, black, red, green, blue and yellow
% are predefined in the color package. Here are the rest.
\definecolor{aqua}{rgb}{0, 1.0, 1.0}
\definecolor{fuschia}{rgb}{1.0, 0, 1.0}
\definecolor{gray}{rgb}{0.502, 0.502, 0.502}
\definecolor{lime}{rgb}{0, 1.0, 0}
\definecolor{maroon}{rgb}{0.502, 0, 0}
\definecolor{navy}{rgb}{0, 0, 0.502}
\definecolor{olive}{rgb}{0.502, 0.502, 0}
\definecolor{purple}{rgb}{0.502, 0, 0.502}
\definecolor{silver}{rgb}{0.753, 0.753, 0.753}
\definecolor{teal}{rgb}{0, 0.502, 0.502}

% Because of conflicts, \space and \mathop are converted to
% \itexspace and \operatorname during preprocessing.

% itex: \space{ht}{dp}{wd}
%
% Height and baseline depth measurements are in units of tenths of an ex while
% the width is measured in tenths of an em.
\makeatletter
\newdimen\itex@wd%
\newdimen\itex@dp%
\newdimen\itex@thd%
\def\itexspace#1#2#3{\itex@wd=#3em%
\itex@wd=0.1\itex@wd%
\itex@dp=#2ex%
\itex@dp=0.1\itex@dp%
\itex@thd=#1ex%
\itex@thd=0.1\itex@thd%
\advance\itex@thd\the\itex@dp%
\makebox[\the\itex@wd]{\rule[-\the\itex@dp]{0cm}{\the\itex@thd}}}
\makeatother

% \tensor and \multiscript
\makeatletter
\newif\if@sup
\newtoks\@sups
\def\append@sup#1{\edef\act{\noexpand\@sups={\the\@sups #1}}\act}%
\def\reset@sup{\@supfalse\@sups={}}%
\def\mk@scripts#1#2{\if #2/ \if@sup ^{\the\@sups}\fi \else%
  \ifx #1_ \if@sup ^{\the\@sups}\reset@sup \fi {}_{#2}%
  \else \append@sup#2 \@suptrue \fi%
  \expandafter\mk@scripts\fi}
\def\tensor#1#2{\reset@sup#1\mk@scripts#2_/}
\def\multiscripts#1#2#3{\reset@sup{}\mk@scripts#1_/#2%
  \reset@sup\mk@scripts#3_/}
\makeatother

% \slash
\makeatletter
\newbox\slashbox \setbox\slashbox=\hbox{$/$}
\def\itex@pslash#1{\setbox\@tempboxa=\hbox{$#1$}
  \@tempdima=0.5\wd\slashbox \advance\@tempdima 0.5\wd\@tempboxa
  \copy\slashbox \kern-\@tempdima \box\@tempboxa}
\def\slash{\protect\itex@pslash}
\makeatother

% math-mode versions of \rlap, etc
% from Alexander Perlis, "A complement to \smash, \llap, and lap"
%   http://math.arizona.edu/~aprl/publications/mathclap/
\def\clap#1{\hbox to 0pt{\hss#1\hss}}
\def\mathllap{\mathpalette\mathllapinternal}
\def\mathrlap{\mathpalette\mathrlapinternal}
\def\mathclap{\mathpalette\mathclapinternal}
\def\mathllapinternal#1#2{\llap{$\mathsurround=0pt#1{#2}$}}
\def\mathrlapinternal#1#2{\rlap{$\mathsurround=0pt#1{#2}$}}
\def\mathclapinternal#1#2{\clap{$\mathsurround=0pt#1{#2}$}}

% Renames \sqrt as \oldsqrt and redefine root to result in \sqrt[#1]{#2}
\let\oldroot\root
\def\root#1#2{\oldroot #1 \of{#2}}
\renewcommand{\sqrt}[2][]{\oldroot #1 \of{#2}}

% Manually declare the txfonts symbolsC font
\DeclareSymbolFont{symbolsC}{U}{txsyc}{m}{n}
\SetSymbolFont{symbolsC}{bold}{U}{txsyc}{bx}{n}
\DeclareFontSubstitution{U}{txsyc}{m}{n}

% Manually declare the stmaryrd font
\DeclareSymbolFont{stmry}{U}{stmry}{m}{n}
\SetSymbolFont{stmry}{bold}{U}{stmry}{b}{n}

% Manually declare the MnSymbolE font
\DeclareFontFamily{OMX}{MnSymbolE}{}
\DeclareSymbolFont{mnomx}{OMX}{MnSymbolE}{m}{n}
\SetSymbolFont{mnomx}{bold}{OMX}{MnSymbolE}{b}{n}
\DeclareFontShape{OMX}{MnSymbolE}{m}{n}{
    <-6>  MnSymbolE5
   <6-7>  MnSymbolE6
   <7-8>  MnSymbolE7
   <8-9>  MnSymbolE8
   <9-10> MnSymbolE9
  <10-12> MnSymbolE10
  <12->   MnSymbolE12}{}

% Declare specific arrows from txfonts without loading the full package
\makeatletter
\def\re@DeclareMathSymbol#1#2#3#4{%
    \let#1=\undefined
    \DeclareMathSymbol{#1}{#2}{#3}{#4}}
\re@DeclareMathSymbol{\neArrow}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\neArr}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\seArrow}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\seArr}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\nwArrow}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\nwArr}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\swArrow}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\swArr}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\nequiv}{\mathrel}{symbolsC}{46}
\re@DeclareMathSymbol{\Perp}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\Vbar}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\sslash}{\mathrel}{stmry}{12}
\re@DeclareMathSymbol{\bigsqcap}{\mathop}{stmry}{"64}
\re@DeclareMathSymbol{\biginterleave}{\mathop}{stmry}{"6}
\re@DeclareMathSymbol{\invamp}{\mathrel}{symbolsC}{77}
\re@DeclareMathSymbol{\parr}{\mathrel}{symbolsC}{77}
\makeatother

% \llangle, \rrangle, \lmoustache and \rmoustache from MnSymbolE
\makeatletter
\def\Decl@Mn@Delim#1#2#3#4{%
  \if\relax\noexpand#1%
    \let#1\undefined
  \fi
  \DeclareMathDelimiter{#1}{#2}{#3}{#4}{#3}{#4}}
\def\Decl@Mn@Open#1#2#3{\Decl@Mn@Delim{#1}{\mathopen}{#2}{#3}}
\def\Decl@Mn@Close#1#2#3{\Decl@Mn@Delim{#1}{\mathclose}{#2}{#3}}
\Decl@Mn@Open{\llangle}{mnomx}{'164}
\Decl@Mn@Close{\rrangle}{mnomx}{'171}
\Decl@Mn@Open{\lmoustache}{mnomx}{'245}
\Decl@Mn@Close{\rmoustache}{mnomx}{'244}
\makeatother

% Widecheck
\makeatletter
\DeclareRobustCommand\widecheck[1]{{\mathpalette\@widecheck{#1}}}
\def\@widecheck#1#2{%
    \setbox\z@\hbox{\m@th$#1#2$}%
    \setbox\tw@\hbox{\m@th$#1%
       \widehat{%
          \vrule\@width\z@\@height\ht\z@
          \vrule\@height\z@\@width\wd\z@}$}%
    \dp\tw@-\ht\z@
    \@tempdima\ht\z@ \advance\@tempdima2\ht\tw@ \divide\@tempdima\thr@@
    \setbox\tw@\hbox{%
       \raise\@tempdima\hbox{\scalebox{1}[-1]{\lower\@tempdima\box
\tw@}}}%
    {\ooalign{\box\tw@ \cr \box\z@}}}
\makeatother

% \mathraisebox{voffset}[height][depth]{something}
\makeatletter
\NewDocumentCommand\mathraisebox{moom}{%
\IfNoValueTF{#2}{\def\@temp##1##2{\raisebox{#1}{$\m@th##1##2$}}}{%
\IfNoValueTF{#3}{\def\@temp##1##2{\raisebox{#1}[#2]{$\m@th##1##2$}}%
}{\def\@temp##1##2{\raisebox{#1}[#2][#3]{$\m@th##1##2$}}}}%
\mathpalette\@temp{#4}}
\makeatletter

% udots (taken from yhmath)
\makeatletter
\def\udots{\mathinner{\mkern2mu\raise\p@\hbox{.}
\mkern2mu\raise4\p@\hbox{.}\mkern1mu
\raise7\p@\vbox{\kern7\p@\hbox{.}}\mkern1mu}}
\makeatother

%% Fix array
\newcommand{\itexarray}[1]{\begin{matrix}#1\end{matrix}}
%% \itexnum is a noop
\newcommand{\itexnum}[1]{#1}

%% Renaming existing commands
\newcommand{\underoverset}[3]{\underset{#1}{\overset{#2}{#3}}}
\newcommand{\widevec}{\overrightarrow}
\newcommand{\darr}{\downarrow}
\newcommand{\nearr}{\nearrow}
\newcommand{\nwarr}{\nwarrow}
\newcommand{\searr}{\searrow}
\newcommand{\swarr}{\swarrow}
\newcommand{\curvearrowbotright}{\curvearrowright}
\newcommand{\uparr}{\uparrow}
\newcommand{\downuparrow}{\updownarrow}
\newcommand{\duparr}{\updownarrow}
\newcommand{\updarr}{\updownarrow}
\newcommand{\gt}{>}
\newcommand{\lt}{<}
\newcommand{\map}{\mapsto}
\newcommand{\embedsin}{\hookrightarrow}
\newcommand{\Alpha}{A}
\newcommand{\Beta}{B}
\newcommand{\Zeta}{Z}
\newcommand{\Eta}{H}
\newcommand{\Iota}{I}
\newcommand{\Kappa}{K}
\newcommand{\Mu}{M}
\newcommand{\Nu}{N}
\newcommand{\Rho}{P}
\newcommand{\Tau}{T}
\newcommand{\Upsi}{\Upsilon}
\newcommand{\omicron}{o}
\newcommand{\lang}{\langle}
\newcommand{\rang}{\rangle}
\newcommand{\Union}{\bigcup}
\newcommand{\Intersection}{\bigcap}
\newcommand{\Oplus}{\bigoplus}
\newcommand{\Otimes}{\bigotimes}
\newcommand{\Wedge}{\bigwedge}
\newcommand{\Vee}{\bigvee}
\newcommand{\coproduct}{\coprod}
\newcommand{\product}{\prod}
\newcommand{\closure}{\overline}
\newcommand{\integral}{\int}
\newcommand{\doubleintegral}{\iint}
\newcommand{\tripleintegral}{\iiint}
\newcommand{\quadrupleintegral}{\iiiint}
\newcommand{\conint}{\oint}
\newcommand{\contourintegral}{\oint}
\newcommand{\infinity}{\infty}
\newcommand{\bottom}{\bot}
\newcommand{\minusb}{\boxminus}
\newcommand{\plusb}{\boxplus}
\newcommand{\timesb}{\boxtimes}
\newcommand{\intersection}{\cap}
\newcommand{\union}{\cup}
\newcommand{\Del}{\nabla}
\newcommand{\odash}{\circleddash}
\newcommand{\negspace}{\!}
\newcommand{\widebar}{\overline}
\newcommand{\textsize}{\normalsize}
\renewcommand{\scriptsize}{\scriptstyle}
\newcommand{\scriptscriptsize}{\scriptscriptstyle}
\newcommand{\mathfr}{\mathfrak}
\newcommand{\statusline}[2]{#2}
\newcommand{\tooltip}[2]{#2}
\newcommand{\toggle}[2]{#2}

% Theorem Environments
\theoremstyle{plain}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}{Lemma}
\newtheorem{prop}{Proposition}
\newtheorem{cor}{Corollary}
\newtheorem*{utheorem}{Theorem}
\newtheorem*{ulemma}{Lemma}
\newtheorem*{uprop}{Proposition}
\newtheorem*{ucor}{Corollary}
\theoremstyle{definition}
\newtheorem{defn}{Definition}
\newtheorem{example}{Example}
\newtheorem*{udefn}{Definition}
\newtheorem*{uexample}{Example}
\theoremstyle{remark}
\newtheorem{remark}{Remark}
\newtheorem{note}{Note}
\newtheorem*{uremark}{Remark}
\newtheorem*{unote}{Note}

%-------------------------------------------------------------------

\begin{document}

%-------------------------------------------------------------------


\section*{classical logic}

\hypertarget{context}{}\subsubsection*{{Context}}\label{context}

\hypertarget{foundations}{}\paragraph*{{Foundations}}\label{foundations}

[[!include foundations - contents]]

\hypertarget{contents}{}\section*{{Contents}}\label{contents}

\noindent\hyperlink{Idea}{Idea}\dotfill \pageref*{Idea} \linebreak
\noindent\hyperlink{details}{Details}\dotfill \pageref*{details} \linebreak
\noindent\hyperlink{classical_propositional_logic}{Classical propositional logic}\dotfill \pageref*{classical_propositional_logic} \linebreak
\noindent\hyperlink{related_concepts}{Related concepts}\dotfill \pageref*{related_concepts} \linebreak


\hypertarget{Idea}{}\subsection*{{Idea}}\label{Idea}

There are many systems of \emph{[[formal logic]]}. By ``classical logic'' one broadly refers to those such systems which reflect the kind of logic as understood, quite literally, by the classics, say starting with \href{excluded+middle#AristotleMetaphysics}{Aristotle, Metaphysics 1011b24}. If you have never heard of any alternative system of logic, then classical logic is just the kind of logic that you have heard about.

There is some variance in what exactly counts as classical and as non-classical in [[logic]], but one main characteristic of classical logic is its use of the \emph{[[principle of excluded middle]]}. Informally this says that every [[proposition]] is either [[true]] or [[false]]. (Slightly more carefully it says that for any proposition $P$, either it or its [[negation]] is true, where the `or' is to be read in an `internal' sense, i.e., as a formal [[disjunction]] $P \vee \neg P$.)

It is the apparent self-evidence of this principle of excluded middle that made people take it for granted for a long period of human civilization, so that it became ``classical''.

One consequence of the [[principle of excluded middle]] in classical logic is the possibility to obtain [[proof]] of a [[proposition]] by showing that its [[negation]] is [[false]] ([[proof by contradiction]]). Evident as this may superficially seem, it has the noteworthy consequence that one may for instance prove [[existential quantifier|existence]] of mathematical objects without having any way to actually construct an example.

This ``non-constructive'' nature of classical logic eventually led people to consider alternative and hence \emph{non-classical} systems of logic, such as [[constructive logic]]/[[intuitionistic logic]], where the [[principle of excluded middle]], and possibly other principle of classical logic, are not considered by default. There is still a close relation between classical and [[constructive logic]]. For example a [[proposition]] is provable in classical logic precisely if its [[double negation]] is provable in [[constructive logic]] (``[[double negation translation]]'').

Other considerations such as the [[internal logic]] of [[categories]] also led to constructive/intuitionistic logics. More recently, other ``nonclassical'' logics such as [[linear logic]], [[paraconsistent logic]], [[relevance logic]], [[quantum logic]], and so on have also gained prominence.

There are other principles that are often associated with classical logic, which still seemed self-evident at a time, but maybe less so than the principle of excluded middle. One such is the [[set theory|set-theoretic]] \emph{[[axiom of choice]]} or one of its equivalent incarnations, such as [[Zorn's lemma]]. The presently most popular formal [[foundation of mathematics]] via the [[set theory]], called \emph{[[ZFC]]}, includes both the [[principle of excluded middle]] as well as the [[axiom of choice]]. In this form classical logic serves as the foundation for \emph{[[classical mathematics]]}.

\hypertarget{details}{}\subsection*{{Details}}\label{details}

Classical logic is the form of [[logic]] usually accepted and taught as standard among working mathematicians, and traced back (at least) to Aristotle. Some particular features that distinguish classical logic are (perhaps not a complete list):

\begin{itemize}%
\item a [[distributive lattice]] of logical operations ($\wedge$ and $\vee$);
\item the [[structural rule]]s of weakening, contraction, and (where meaningful) exchange;
\item an involutory [[negation]].

\end{itemize}
In contrast, [[minimal logic|minimal]], [[intuitionistic logic|intuitionistic]], and (some forms of) [[paraconsistent logic|paraconsistent]] logics have the distributive lattice and the structural rules but no involutory negation. On the other hand, [[linear logic]] (at least, ``classical'' linear logic) and (other forms of) paraconsistent logic have logical operations with at least some distributive properties and an involutory negation, but lack some structural rules. Then again, [[quantum logic]] and (yet other forms of) paraconsistent logic have the structural rules and the involutory negation, but lack any sort of distributivity.

In [[category theory]] (and in the [[foundations]] of mathematics generally), it is intuitionistic logic that is most often contrasted to classical logic; the difference is given by the law of [[excluded middle]], which holds classically but not intuitionistically.

\hypertarget{classical_propositional_logic}{}\subsection*{{Classical propositional logic}}\label{classical_propositional_logic}

Before describing what makes a [[propositional logic]] `classical', let us quickly recall what propositional logic is in the first place.

In general, a (deductive) [[logic]] specifies rules of [[syntax]] for forming well-formed [[formulas]] which can be considered as assertions, and rules of inference for deriving one formula (called a `conclusion') from other formulas (called `premises'), in such a way that truth of the conclusion follows on the assumption of truth of the premises. In short, a [[formal logic]] specifies a mode of reasoning that is considered valid for a particular mathematical context.

In [[propositional logic]], one forms a formula by applying basic logical operations such as $\wedge$ ('[[logical conjunction|and]]'), $\vee$ ('[[logical disjunction|or]]'), and $\Rightarrow$ ('[[implication|implies]]') to simpler formulas. The simplest formulas are called atomic formulas, and usually take the form of an [[equation]] $s = t$ between two [[terms]] (and underneath there are rules for term formation as well), or something like $R(a_1, \ldots, a_n)$ where $R$ stands for some basic relation (between terms $a_1, \ldots, a_n$) belonging to whatever language one is working with. A standard list of \emph{propositional} operations would be

\begin{itemize}%
\item $\wedge, \vee, \Rightarrow$ (binary operations), $\neg$ (`not', an unary operator), and $\top, \bot$ (`true' and `false', basic logical constants or nullary operators).

\end{itemize}
Missing from propositional logic \emph{per se} are [[quantifiers]] such as $\exists$ ([[existential quantifier]]) and $\forall$ ([[universal quantifier]]), which properly speaking belong to [[predicate logic]]. (One way of thinking about propositional logic is that it treats formulas as assertions ``all of the same type'', whereas quantifiers allow one to shift between classes of assertions of one type to assertions of another type.)

As we said, there are also rules of inference. There are various styles in which these are presented, such as [[natural deduction]] or [[sequent calculus]]. But a simple example might look like this:

\begin{displaymath}
\frac{P \wedge Q}{P}
\end{displaymath}
(``from $P \wedge Q$ we may infer $P$''). This might also be written $P \wedge Q \vdash P$ (``pronounced $P \wedge Q$ entails $P$''), thought of as asserting a relation between propositions called entailment. Two of the universal rules of propositional logic (whether classical or intuitionistic or quantum or whatever) is that the entailment relation should be [[reflexive relation|reflexive]] and [[transitive relation|transitive]]: the rules of inference allow an entailment $P \vdash P$ for any formula $P$, and if they allow entailments $A \vdash B$ and $B \vdash C$, then they allow $A \vdash C$.

Thus, in a propositional logic, formulas together with the entailment relation that is provided for by the rules of inference form a [[preorder]]. Sometimes one goes a little further: in situations where one can derive $A \vdash B$ and $B \vdash A$, one says that $A$ and $B$ are provably equivalent (often abbreviated as $A \equiv B$), and one may pass to the [[poset]] of provable equivalence classes (the usual way in which a poset is associated with a preorder).

One knows that one is in the realm of \emph{classical} propositional logic if the poset of provable equivalence classes is a [[Boolean algebra]], in which $\wedge$ induces the meet operation and $\vee$ the join operation. Here the rules of inference allow bi-entailments such as

\begin{displaymath}
A \Rightarrow B \equiv \neg A \vee B
\end{displaymath}
and in fact the different types of propositional logic are usually conveniently described by specifying what type of algebraic structure we get on the poset of provable equivalence classes. For example, in [[intuitionistic logic]] this poset forms a [[Heyting algebra]].

\hypertarget{related_concepts}{}\subsection*{{Related concepts}}\label{related_concepts}

\begin{itemize}%
\item [[logic]]
\item [[classical mathematics]]
\item [[constructive logic]] / [[intuitionistic logic]]
\item [[material set theory]]

\end{itemize}


\end{document}