\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*{intuitionistic mathematics}

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

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

[[!include foundations - contents]]

\hypertarget{constructivism_realizability_computability}{}\paragraph*{{Constructivism, Realizability, Computability}}\label{constructivism_realizability_computability}

[[!include constructivism - contents]]

\hypertarget{mathematics}{}\paragraph*{{Mathematics}}\label{mathematics}

[[!include mathematicscontents]]

\hypertarget{intuitionistic_mathematics}{}\section*{{Intuitionistic mathematics}}\label{intuitionistic_mathematics}

\noindent\hyperlink{Idea}{Idea}\dotfill \pageref*{Idea} \linebreak
\noindent\hyperlink{Terminology}{Terminology}\dotfill \pageref*{Terminology} \linebreak
\noindent\hyperlink{mathematical_principles}{Mathematical principles}\dotfill \pageref*{mathematical_principles} \linebreak
\noindent\hyperlink{feel}{Feel}\dotfill \pageref*{feel} \linebreak
\noindent\hyperlink{related_concepts}{Related concepts}\dotfill \pageref*{related_concepts} \linebreak
\noindent\hyperlink{References}{References}\dotfill \pageref*{References} \linebreak


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

\emph{Intuitionistic mathematics} (often abbreviated INT) is the earliest full-blown variety of [[constructive mathematics]], done according to the mathematical principles developed by [[L.E.J. Brouwer]] through his philosophy of \emph{intuitionism}.

Beware that this terminology is not consistent across mathematics. Not infrequently the word ``intuitionistic'' is used to refer simply to [[constructive mathematics]] in general, or to [[constructive logic]], or to [[predicative mathematics|impredicative]] [[set theory]] done in constructive logic. This page is about \emph{Brouwer's intuitionism}, which is a specific variety of constructive mathematics that (unlike ``neutral'' constructive mathematics) uses axioms that [[contradiction|contradict]] [[classical mathematics]]. For more on this see at \emph{\hyperlink{Terminology}{Terminology}} below.

The first main philosophical idea is that mathematical truth (a true statement) can only be attained in one's mind, by carefully arranging one's concepts and constructions in such a way that there remains absolutely no doubt that every aspect of the statement is verified, unambiguously, without reliance on any `outside' assumption, for instance about the platonic nature of reality. (The [[principle of excluded middle]] is such an assumption, and Brouwer gave mathematical counterexamples to its validity, eventually leading to the foundational crisis in mathematics (Grundlagenstreit) around 1930, and Brouwer's conflict with Hilbert).

The second main philosophical idea is that the mind works over time. One does not have everything ready and done from the start. Infinity is a (perceived) idealized property of time, but one cannot have completed any infinite process or construction on any given day. Infinity is potential, not actual.

The main mathematical idea then becomes that we can only build mathematical structures and truths starting from the natural numbers $0, 1, ...$ (where the dots indicate potential, not actual infinity). Natural numbers are definite and precise, but most real numbers, such as $\pi$, have a very different nature. We can only form something that we call `$\pi$' through a never-finished process of approximation.

Nonetheless, a substantial part of mathematics can be built up (`constructed') in this way. What mainly differentiates intuitionistic mathematics from [[constructive mathematics]] are two added axioms.

Brouwer `deduced' two axiomatic insights, notably `continuous choice' and a transfinite-induction based knowledge principle called `the Bar Theorem'. 'Continuous choice' conflicts with classical mathematics, the Bar Theorem is classically true (it boils down to stating that any open cover of Baire space is inductive).

Kleene \& Vesley (in \emph{Foundations of Intuitionistic Mathematics}, 1965) offered a clean axiomatic approach which is nowadays called FIM. Kleene proved that FIM is equiconsistent with classical mathematics. Kleene also proved that theorems of FIM are recursively [[realizability|realizable]], which shows the computational content of FIM.

\hypertarget{Terminology}{}\subsection*{{Terminology}}\label{Terminology}

Terminological ambiguity is often present in [[constructive mathematics]] and its varieties. Intuitionistic mathematics (INT) includes [[axioms]] that contradict [[classical logic]]; but people in non-foundational disciplines often use ``intuitionistic'' to mean roughly the same as ``[[constructive|constructive mathematics]]'' (say: mathematics without the [[principle of excluded middle]], usually with computational/algorithmic content and some restriction on impredicativity, but nothing added that contradicts classical mathematics).

There are a variety of ways to use the term `intuitionistic'. We list them here, roughly from the most specific to the most general, and contrast (where appropriate) with the term `constructive':

\begin{itemize}%
\item \textbf{Intuitionism} is an early-20th-century [[philosophy of mathematics]] developed by [[Brouwer]], according to which [[mathematics]] is a free creation of a mind, and valid results are about what that mind creates (rather than about an external reality, as in [[platonism]], or about nothing, as in [[formalism]]). From this controversial starting point, Brouwer drew even more controversial conclusions about both [[mathematics]] and [[logic]] (which he saw as derived from mathematics, rather than conversely as in [[logicism]]). Intuitionism is one particular philosophy of [[constructivism]].


\item \textbf{Intuitionistic mathematics} is the mathematics along the lines of the mathematics that Brouwer came up with. However, it's not necessary to accept Brouwer's philosophy to practise intuitionistic mathematics; conversely, one may accept Brouwer's philosophical starting place but not his conclusions about the resulting mathematics. Intuitionistic mathematics is one particular variety of [[constructive mathematics]].

One example of intuitionistic mathematics (which nicely shows that intuitionism is not a matter of ``belief'' but of subject) is type II [[computable mathematics]] (see for instance \hyperlink{Bauer05}{Bauer 05, section 4.3.1}).


\item \textbf{[[intuitionistic set theory|Intuitionistic set theory]]} is a [[set theory]], generally proffered as a [[foundation of mathematics]], intended to capture intuitionistic mathematics. As the terminology is usually used (for example in the name of IZF, [[IZF|intuitionistic Zermelo-Frankel set theory]]), `intuitionistic' means that [[excluded middle]] fails but [[power sets]] are included (making it [[impredicative mathematics|impredicative]]). In contrast, `constructive' set theory (such as CZF, [[CZF|constructive Zermelo-Frankel set theory]]) has [[function sets]] but not power sets (making it [[weakly predicative mathematics|weakly predicative]]). The former is technically convenient, but the latter is better motivated. That said, Brouwer's mathematics was even more predicative, making \emph{both} of these set theories stronger than he would accept.


\item \textbf{[[intuitionistic type theory|Intuitionistic type theory]]} is generally proffered as a [[foundation of mathematics]] that is (in most of its forms) both [[constructivism|constructive]] and [[predicativism|predicative]]. For purposes of comparing type theory to set theory, it might be nice if `intuitionistic' and `constructive' were distinguished for type theories as they are for set theories, but they aren't. (Then again, there was never much sense in making that distinction for set theories using that terminology.)



\end{itemize}
There is variant of the [[NuPrl]] type theory with choice sequences: \href{http://www.nuprl.org/html/Nuprl2Coq/continuity.pdf}{PDF}.

\begin{itemize}%
\item \textbf{[[Intuitionistic logic]]} is the [[logic]] that intuitionistic mathematics, set theory, and type theory use, which lacks the principle of [[excluded middle]]; other forms of [[constructive mathematics]] also use intuitionistic logic, which is therefore also known as \emph{constructive logic}.

\end{itemize}
\hypertarget{mathematical_principles}{}\subsection*{{Mathematical principles}}\label{mathematical_principles}

Brouwer did not believe in a rigourous formalization of mathematics, for various reasons (amongst which the mathematical incompleteness of formal systems, as later proved by [[Gödel's incompleteness theorem]]). He saw mathematical logic and formal systems as a correct part of mathematics, but held that this part could capture the essence nor the scope of mathematics in a meaningful way. Nonetheless he admitted that certain often-used arguments and mental constructions could be formalized `as an abbreviation'.

Brouwer's student Arend Heyting (who later succeeded Brouwer as professor in Amsterdam) formalized what is now known as [[intuitionistic logic]]. He also is largely responsible for the [[Brouwer-Heyting-Kolmogorov interpretation]] (BHK) of intuitionistic logic, BHK can be seen as a precursor to realizability.

\begin{itemize}%
\item In hindsight, we may say that intuitionistic mathematics is done in a [[pretopos]] identified as [[Set]].


\item We have the [[axiom of infinity]] and [[countable choice]], as in [[classical mathematics]].


\item We have the classically false principles of [[continuity principle|continuity]] and [[continuous choice]].


\item We have the [[fan theorem]] and [[bar theorem]], which are classically true but fail in [[Russian constructivism]].


\item There's also some stuff about [[choice sequences]] that is highly philosophical, involving mathematical principles such as the [[Brouwer-Kripke scheme]].



\end{itemize}
Although it's not enough to derive all of the above, much of the essence of intuitionistic mathematics, or at least intuitionistic [[analysis]], can be summarized in the theorem that every (set-theoretic) [[function]] from the [[unit interval]] to the [[real line]] is [[uniformly continuous map|uniformly continuous]].

Intuitionistic mathematics is often regarded as a specialization of [[Bishop's constructive mathematics]] obtained by adding the above principles, but this is somewhat questionable if it refers to what Bishop actually did (and in particular the fact that he worked with [[Bishop sets]]); see [[Bishop's constructive mathematics]] for discussion.

\hypertarget{feel}{}\subsection*{{Feel}}\label{feel}

In intuitionistic mathematics, already [[set theory]] behaves a lot like [[topology]], a point stressed by [[Frank Waaldijk]] (\href{http://www.fwaaldijk.nl/mathematics.html}{web}). He uses the [[Kleene-Vesley]] system. Fourman's [[continuous truth]] makes this remark precise using [[topos theory]].

Although intuitionistic mathematics does not accept all [[function sets]] (much less [[power sets]]), it seems to allow for both [[induction|inductive]] and [[coinduction|coinductive]] structures; see \href{http://golem.ph.utexas.edu/category/2008/12/the_status_of_coalgebra.html#c020731}{a Caf\'e{} comment}. The reluctance to add function spaces is similar to the problem of function spaces in topology; see [[nice category of spaces]].

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

\begin{itemize}%
\item [[constructive mathematics]]


\item [[intuitionistic type theory]]


\item [[realizability]]


\item [[choice sequence]]



\end{itemize}
\hypertarget{References}{}\subsection*{{References}}\label{References}

The roots of Brouwer's intuitionism are apparently in his PhD thesis

\begin{itemize}%
\item [[L.E.J. Brouwer]], \emph{Over de Grondslagen der Wiskunde, PhD thesis}, Universiteit van Amsterdam, 1907.

\end{itemize}
A reference written by Brouwer and still in print in English is

\begin{itemize}%
\item [[L.E.J. Brouwer]], \emph{Brouwer's Cambridge Lectures on Intuitionism}, edited by D. van Dalen

\end{itemize}
Then an axiomatization of intuitionistic mathematics is given in

\begin{itemize}%
\item [[Stephen Kleene]], R. E. Vesley, \emph{The foundations of intuitionistic mathematics}, North-Holland (1965)

\end{itemize}
in terms of [[realizability]] (the [[Kleene-Vesley topos]]), and hence intuitionistic mathematics is shown to be consistent.

General reviews include

\begin{itemize}%
\item Stanford Encyclopedia of Philosophy, \emph{\href{http://plato.stanford.edu/entries/intuitionism/}{Intuitionism in the Philosophy of Mathematics}}

\end{itemize}
Reviews with further developments include for instance

\begin{itemize}%
\item [[Frank Waaldijk]], \emph{On the foundations of constructive mathematics -- especially in relation to the theory of continuous functions} (\href{http://www.fwaaldijk.nl/mathematics.html#onthefoundations}{web})

(with a focus on [[constructive analysis]]).



\end{itemize}
Discussion of one approach to basic [[topology]] in intuitionistic mathematics is in

\begin{itemize}%
\item [[Frank Waaldijk]], \emph{modern intuitionistic topology}, 1996 (\href{http://www.fwaaldijk.nl/modern%20intuitionistic%20topology.pdf}{pdf})

\end{itemize}
For more see also the references at \emph{[[constructive mathematics]]}.

[[!redirects intuitionistic mathematics]] [[!redirects intuitionism]]



\end{document}