\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*{computable physics}

\begin{quote}%
This page is about [[computability]] of fundamental [[physics]] in the sense of [[computable mathematics]] and [[constructive analysis]]. It is not about \emph{[[computational physics]]}, though of course there is a relation. For computational [[complexity theory]] in physics see at [[computational complexity and physics]].


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

\hypertarget{physics}{}\paragraph*{{Physics}}\label{physics}

[[!include physicscontents]]

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

[[!include constructivism - contents]]

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

\noindent\hyperlink{idea}{Idea}\dotfill \pageref*{idea} \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}

The following idea or observation or sentiment has been expressed independently by many authors. We quote from \hyperlink{Szudzik10}{Szudzik 10, section 2}:

\begin{quote}%
The central problem is that [[model (physics)|physical models]] use [[real numbers]] to represent the values of [[observable|observable quantities]], $[...]$ Careful consideration of this problem, however, reveals that the real numbers are not actually necessary in physical models. [[natural number|Non-negative integers]] suffice for the representation of observable quantities because numbers [[measurement|measured]] in laboratory [[experiments]] necessarily have only finitely many digits of precision.


\end{quote}
Diverse conclusions have been drawn from this. One which seems useful and well-informed by the theory of [[computability]] in [[mathematics]] is the following (further quoting from \hyperlink{Szudzik10}{Szudzik 10, section 2})

\begin{quote}%
So, we suffer no loss of generality by restricting the values of all observable quantities to be expressed as [[natural numbers|non-negative integers]] --- the restriction only forces us to make the methods of error analysis, which were tacitly assumed when dealing with real numbers, an explicit part of each model.


\end{quote}
In type-I [[computability]] the [[computable functions]] are [[partial recursive functions]] and in view of this some authors concluded (e.g. \hyperlink{Kreisel74}{Kreisel 74}) (and we still quote \hyperlink{Szudzik10}{Szudzik 10, section 2} for this):

\begin{quote}%
To show that a [[model (physics)|model]] $[$ of physics $]$ is [[computable function|computable]], the model must somehow be expressed using [[partial recursive function|recursive functions]].


\end{quote}
A similar sentiment is voiced by \hyperlink{GerochHartle}{Geroch and Hartle}:

\begin{quote}%
We propose, in parallel with the notion of a computable number in mathematics, that of a measurable number in a physical theory. The question of whether there exists an algorithm for implementing a theory may then be formulated more precisely as the question of whether the measurable numbers of the theory are computable. We argue that the measurable numbers are in fact computable in the familiar theories of physics, but there is no reason why this need be the case in order that a theory have predictive power. Indeed, in some recent formulations of quantum gravity as a sum ver histories, there are candidates for numbers that are measurable but not computable.


\end{quote}
However, in [[computability theory]] there is also the concept of \emph{[[computable function (analysis)|type-II computable functions]]} used in the field of ``[[constructive analysis]]'', ``[[computable analysis]]''. This is based on the idea that for instance for specifying [[computable real numbers]] as used in [[physics]], an [[algorithm]] may work not just on single [[natural numbers]], but indefinitely on sequences of them, producing output that is in each step a finite, but in each next step a more accurate approximation.

[[!include computable mathematics -- table]]

This concept of [[computable analysis|type-II computability]] is arguably closer to actual practice in [[physics]].

Of course there is a wide-spread (but of course controversial) vague speculation (often justified by alluding to expected implications of [[quantum gravity]] on the true microscopic nature of [[spacetime]] and sometimes formalized in terms of cellular automata, e.g. \hyperlink{Zuse67}{Zuse 67}) that in some sense the [[observable universe]] is fundamentally ``[[finite object|finite]]'', so that in the end [[computability]] is a non-issue in [[physics]] as one is really operating on a large but [[finite set]] of states.

However, since fundamental physics is [[quantum physics]] and since [[quantum mechanics]] with its [[wave functions]], [[Hilbert spaces]] and [[probability amplitudes]] invokes ([[functional analysis|functional]]) [[analysis]] and hence ``non-finite mathematics'' even when describing the minimum of a [[physical system]] with only two possible configurations (a ``[[qbit]]'') a strict [[finitism]] perspective on fundamental [[physics]] runs into problems (highlighted for instance in (\hyperlink{Feynman81}{Feynman 81, slide 15})). Precisely this kind of issue is the topic of \emph{[[computable analysis]]} (``[[constructive analysis]]'', ``[[exact analysis]]'') with its type-II notion of [[computable functions]], which would therefore seem to be the right mathematical context discussing [[computability]] in fundamental (namely quantum) [[physics]]. This point is made in (\hyperlink{WeihrauchZhong02}{Weihrauch-Zhong 02}) for the [[wave equation]].

This matters: there are solutions to the [[wave equation]] with type-I computable initial values which are not themselves type-I computable (\hyperlink{PourEl83}{Pour-El et al. 83}). If type-I computability were the right concept of computabuility in physics, this result would show a violation of the [[Church-Turing thesis]]. But in (\hyperlink{WeihrauchZhong02}{Weihrauch-Zhong 02}) it is argued that the correct concept to use is indeed type-II computability and it is shown (\hyperlink{WeihrauchZhong02}{Weihrauch-Zhong 02, theorem 3.2}) that the solution operator to the wave equation is indeed type-II computable. The same is shown for the [[Schrödinger equation]] of [[quantum mechanics]] in (\hyperlink{WeihrauchZhong01}{Weihrauch-Zhong 01}, \hyperlink{WeihrauchZhong06}{Weihrauch-Zhong 06}) where it is found that the Schr\"o{}dinger operator is computable on the [[Lebesgue space]] $L^p$ precisely for the physically relevant value $p = 2$. A similar conclusion is reached by \hyperlink{Baez}{Baez}.

In the vein of type-II computability the issue specifically of computable [[quantum physics]]/[[quantum logic]] has only been further considered in (\hyperlink{Streicher12}{Streicher 12}), where it is shown that at least a fair bit of the [[Hilbert space]] technology of [[quantum mechanics]]/[[quantum logic]] sits inside the [[function realizability topos]] $RT(\mathcal{K}_2)$.

The question whether the [[observable universe]] or at least all [[experiments]] done within are computable is part of the (strong) [[physical Church-Turing thesis]]. See there for more, and see (\hyperlink{Waaldijk03}{Waaldijk 03}). Experiments showing non-computability in quantum processes have been claimed in (\hyperlink{CDDS10}{CDDS 10}).

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

\begin{itemize}%
\item [[interpretation of quantum mechanics]]


\item [[measurement problem]]


\item [[quantum logic]], [[quantum computation]]


\item [[coordination]]


\item [[p-adic physics]]


\item [[hypercomputation]]


\item [[constructive mathematics]], [[geometry of physics]]



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

Decent discussion of computability in physics includes the following

\begin{itemize}%
\item Robert Rosen, \emph{Church's thesis and its relation to the concept of realizability in biology and physics}, Bulletin of Mathematical Biophysics 24 (1962), 375--393.


\item [[Konrad Zuse]], \emph{Rechnender Raum}, Elektronische Datenverarbeitung 8 (1967), 336--344.


\item [[Georg Kreisel]], \emph{A notion of mechanistic theory}, Synthese 29 (1974), 11--26.


\item [[Richard Feynman]], \emph{Simulating physics with computers}, talk at \emph{1st conference on Physics and Computation} MIT (1981), (talk notes by P. Birnbaum, E. Tromer: \href{http://www.wisdom.weizmann.ac.il/~naor/COURSE/feynman-simulating.pdf}{pdf})


\item Marian Boykan Pour-El, J. Ian Richards, \emph{Computability and noncomputability in classical analysis', Trans. Amer. Math. Soc. 275 (1983) 539-560.}

Marian Pour-El, Ning Zhong, \emph{The wave equation with computable initial data whose unique solution is nowhere computable}, Math. Logic Quart. 43 (1997) no. 4, 499-509.


\item [[Douglas Bridges]], \emph{Constructive mathematics and unbounded operators -- a reply to Hellman}, J. Philosophical Logic 24, 549--561 (1995)


\item [[Klaus Weihrauch]], Ning Zhong, \emph{Is the linear Schr\"o{}dinger Propagator Turing Computable?} , in Jens Blanck et al (eds.) \emph{Computability and Complexity in Analysis: 4th International Workshop} , CCA, Springer 2001


\item [[Klaus Weihrauch]], Ning Zhong, \emph{Is wave propagation computable or can wave computers beat the Turing machine?}, Proc. of the London Math. Soc. (3) 85 (2002) (\href{http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.95.5994}{web})


\item [[Frank Waaldijk]], section 7 of \emph{On the foundations of constructive mathematics -- especially in relation to the theory of continuous functions}, 2003 (\href{http://www.fwaaldijk.nl/foundations%20of%20constructive%20mathematics.pdf}{pdf}, \href{http://fwaaldijk.wordpress.com/2014/01/14/experiment-to-disprove-strong-physical-church-turing-thesis/}{web discussion}).


\item [[Klaus Weihrauch]], \emph{Computing Schr\"o{}dinger propagators on Type-2 Turing machines}, Journal of Complexity Volume 22, Issue 6, December 2006, Pages 918--935


\item [[Matthew Szudzik]], \emph{The Computable Universe Hypothesis}, in [[Hector Zenil]] (ed.) \emph{\href{http://www.worldscientific.com/worldscibooks/10.1142/8306}{A Computable Universe: Understanding and Exploring Nature as Computation}} , World Scientific, 2012, pp. 479-523 (\href{http://arxiv.org/abs/1003.5831}{arXiv:1003.5831})


\item Cristian Calude, Michael Dinneen, Monica Dumitrescu, Karl Svozil, \emph{Experimental Evidence of Quantum Randomness Incomputability}, Phys. Rev. A 82, 022102 (2010) (\href{http://arxiv.org/abs/1004.1521}{arxiv:1004.1521}, \href{http://www.technologyreview.com/view/418445/first-evidence-that-quantum-processes-generate-truly-random-numbers/}{web announcement})


\item [[Thomas Streicher]], \emph{Computability Theory for Quantum Theory}, talk at Logic Seminar Univ. Utrecht in July 2012 (\href{http://www.mathematik.tu-darmstadt.de/~streicher/TALKS/qtdm.pdf}{pdf})


\item Stanford Encyclopedia of Philosophy, \emph{\href{http://plato.stanford.edu/entries/computation-physicalsystems/}{Computation in physics}}



\end{itemize}
Some general remarks on the impact of [[realizability]] ([[intuitionistic mathematics|intuitionistic]]/[[constructive mathematics]]) on computability in physics and the [[Church-Turing thesis]] are in

\begin{itemize}%
\item [[Andrej Bauer]], section 4 of \emph{Intuitionistic Mathematics and Realizability in the Physical World}, in [[Hector Zenil]] (ed.) \emph{\href{http://www.worldscientific.com/worldscibooks/10.1142/8306}{A Computable Universe: Understanding and Exploring Nature as Computation}}, World Scientific 2012 (\href{http://math.andrej.com/2014/03/04/intuitionistic-mathematics-and-realizability-in-the-physical-world/}{web}, \href{http://math.andrej.com/wp-content/uploads/2014/03/real-world-realizability.pdf}{pdf})

\end{itemize}
A useful set of lecture notes on the mathematical background of [[computability]] and [[realizability]] is in

\begin{itemize}%
\item [[Andrej Bauer]], \emph{Realizability as connection between constructive and computable mathematics}, in T. Grubba, P. Hertling, H. Tsuiki, and [[Klaus Weihrauch]], (eds.) \emph{CCA 2005 - Second International Conference on Computability and Complexity in Analysis}, August 25-29,2005, Kyoto, Japan, ser. Informatik Berichte, , vol. 326-7/2005. FernUniversit\"a{}t Hagen, Germany, 2005, pp. 378--379. (\href{http://math.andrej.com/data/c2c.pdf}{pdf})


\item Robert Geroch, [[James Hartle]], \emph{Computability and physical theories}, Foundations of Physics June 1986, Volume 16, Issue 6, pp 533-550 (\href{http://dx.doi.org/10.1007/BF01886519}{doi}, \href{http://link.springer.com/content/pdf/10.1007/BF01886519.pdf}{PDF})


\item John Baez, \emph{Recursivity in Quantum Mechanics}, \href{http://math.ucr.edu/home/baez/recursivity.pdf}{PDF} [[!redirects computable quantum physics]]



\end{itemize}
Ye presents a constructive development of part of quantum theory and relativity theory.

\begin{itemize}%
\item Feng Ye, \emph{Strict Finitism and the Logic of Mathematical Applications} \href{http://www.phil.pku.edu.cn/cllc/people/fengye/finitismAndTheLogicOfMathematicalApplications.pdf}{PDF preprint} [[!redirects computability in physics]]

\end{itemize}


\end{document}