<p>It is is worth thinking about WHY intuistionistic logic is the natural logic for computation, since all too often people get lost in the technical details and fail to grasp the essence of the issue.</p>

<p>Very simply, classical logic is a logic of perfect information: all statements within the system are assumed to be known or knowable as unambiguously true or false.</p>

<p>Intuistionistic logic, on the other hand, has room for statements with unknown and unknowable truth values.  This is essential for computation, since, thanks to the undecidability of termination in the general case, it will not always be certain what the truth value of some statements will be, or even whether or not a truth value can ever be assigned to certain statements.</p>

<p>Beyond this, it turns out that even in strongly normalizing environments, where termination is always guaranteed, classical logic is still problematic, since double negation elimination $\neg\neg P \implies P$ ultimately boils down to being able to pull a value "out of thin air" rather than directly computing it.</p>

<p>In my opinion, these "semantic" reasons are a much more important motivation for the use of  intuistionistic logic for computation than any other technical reasons one could marshal. </p>

CC BY-SA 3.0
2013-05-21T14:11:22.673Z
2013-05-21T14:11:22.673Z
Marc Hamann
<p>Real-world cryptographic hash functions like MD5 &amp; SHA are keyless. As such, it makes it quite difficult to apply techniques from theoretical cryptography to reason about their security. The simple reason why: for any keyless hash function, there exists a very small program/adversary which outputs a collision under that hash function; namely, a program that has such a collision -- which must exist! -- hard-coded.</p>

<p>Phil Rogaway's paper <a href="http://www.cs.ucdavis.edu/~rogaway/papers/ignorance.pdf" rel="nofollow">Formalizing Human Ignorance: Collision-Resistant Hashing without the Keys</a> deals with this problem. In it he shows that some very standard theorems for keyed hash functions (like the Merkle-Damg&aring;rd construction &amp; hash-then-sign paradigm) can be adapted and re-proven with  "intuitionist-friendly" theorem statements applying to unkeyed hash functions.</p>

CC BY-SA 3.0
2013-05-20T23:00:56.530Z
2013-05-21T16:01:07.507Z
2013-05-21T16:01:07.507Z
mikero
<p>here is a nice chapter on Intuitionistic Logic from a comprehensive online book <em>Logic for Computer Science</em>, 300pp.[1] sec 9.5, p210, summary on p220:</p>

<blockquote>
  <p>Intuitionistic
  logic
  arose
  out
  of
  the
  constructivist
  movement
  in
  mathematics
  which
  rejected
  non-constructive
  existence
  proofs
  or
  those
  based
  on
  the
  law
  of
  the
  excluded
  middle.
  Recently
  a
  connection
  between
  intuitionistic
  mathematics
  and
  programming
  has
  come
  out
  of
  the
  observation
  that
  propositions
  and
  types
  (in
  the
  programming
  sense)
  are
  equivalent.
  Algorithm
  development
  in
  this
  formal
  system,
  which
  is
  based
  on
  natural
  deduction,
  consists
  of
  writing
  a
  specification
  in
  logical
  notation
  and
  then,
  considering
  this
  as
  a
  type,
  proving
  that
  it
  is
  non-empty.
  Because
  the
  underlying
  logic
  is
  constructive
  the
  proof,
  if
  it
  can
  be
  carried
  out,
  must
  embody
  the
  explicit construction of an object of the appropriate type.</p>
</blockquote>

<p>another nearby perspective comes from TCSist Andrej Bauer writing on "Mathematics and computation; mathematics for computers"[2] who proposes basically that "intuitionistic mathematics is good for physics". the presentation is mainly in terms of physics, but for those who consider <a href="https://cstheory.stackexchange.com/questions/2074/physics-results-in-tcs">CS tightly coupled with physics</a> the ideology will generally carry to TCS.</p>

<blockquote>
  <p><strong>Computational interpretation.</strong> This is the interpretation of intuitionistic logic commonly presented in computer science. We view all sets as represented by suitable data structures—a reasonable point of view for a computer scientist. Then a statement is taken to be true if there exists a program (computational evidence) witnessing its truth.</p>
</blockquote>

<p>[1] <a href="http://www.cs.waikato.ac.nz/~stever/LCS.pdf" rel="nofollow noreferrer">Logic for Computer Science,</a> Reeves and Clark</p>

<p>[2] <a href="http://math.andrej.com/2008/08/13/intuitionistic-mathematics-for-physics/" rel="nofollow noreferrer">Intuitionistic mathematics for physics</a> Bauer</p>

CC BY-SA 3.0
2013-05-22T18:17:31.863Z
2013-05-22T18:17:31.863Z
2017-04-13T12:32:28.167Z
vzn
<p>As I said in the comments, intuitionist logic is not the main point. The more important point is having a constructive proof. I think Martin-Löf's type theory is much more relevant to programming language theory than intuitionistic logic and there are experts who have argued that Martin-Löf's work is the main reason for the revival of the general interest in constructive mathematics.</p>

<p>The computability interpretation of constructiveness is one possible perspective, but it is not the only one. We should be careful here when we want to compare constructive proofs to classical proofs. Although both might use the same symbols, what they mean by those symbols are different. </p>

<p>It is always good to remember that classical proofs can be translated to intuitionistic proofs. In other words, in a sense, classical logic is a subsystem of intuitionistic logic. Therefore you can realize (say using computable functions) classical proofs in a sense. On the other hand, we can think of constructive mathematics as some mathematical system in classical setting.</p>

<p>At the end, formalisms, whether classical or constructive, are tools for us to express statements. Taking a classical theorem and trying to prove it constructively without this perspective doesn't make much sense IMHO. When I say $A \lor B$ classically I mean something different from what I say $A \lor B$ constructively. You can argue what "should" be the real meaning of "$\lor$" but I think that is not interesting if we are not discussing what we want to express in the first place. Do we mean (at least) one of them holds and we know which one? Or do we simply mean one of them holds?</p>

<p>Now, with this perspective, if we want to prove a statement like $\forall x \ \exists y \ \varphi(x,y)$ and we want to relate this to a mapping from $x$ to some $y$ satisfying $\varphi(x,y)$ then the better way to express can be the constructive way. On the other hand, if we only care about the existence of $y$ and do not care about how to find them then the classical way would probably make more sense. When you prove the statement constructively, you are also implicitly building an algorithm for finding $y$ from $x$. You can do the same thing explicitly with a more complicate formula like "the algorithm $A$ has the property that for all $x$, $\varphi(x,A(x))$" where $A$ is some explicitly given algorithm.
If it is not clear why one may prefer the constructive way to express this, think about programming languages as an analogy: you can write a program for the Kruskal's MST algorithm in x86 assembly language where you have to care about lots of side issues or you can write a program in Python.</p>

<p>Now why we don't use intuitionist logic in practice? There are several reasons. For example, most of us are not trained with that mind setting. Also finding a classical proof of a statement might be much easier than finding a constructive proof of it. Or we might care about low-level details which are hidden and not accessible in a constructive setting (see also <a href="https://en.wikipedia.org/wiki/Linear_logic" rel="nofollow noreferrer">linear logic</a>). Or we might simply be uninterested in getting the extra stuff that comes with a constructive proof. And although there are tools to extract programs from proofs these tools generally need very detailed proofs and haven't been user-friendly enough for the general theorist. In short, too much pain for too little benefit.</p>

<p>Here is one possible reason why we don't see much constructive proofs in theory A:
our theorems in theory A are often $\Pi^0_2$ statements and are proven using not very strong theories (say they are provable in $PA$) and by <a href="https://en.wikipedia.org/wiki/Friedman_translation" rel="nofollow noreferrer">a meta-theorem</a> all of them are also provable constructively (in the constructive counterpart of $PA$). In fact, many theory A results can be proven in theories much weaker than $PA$.</p>

<p>I remember that <a href="http://www.math.canterbury.ac.nz/~d.bridges/" rel="nofollow noreferrer">Douglas S. Bridges</a> in the introduction to his computability theory book argued that we should prove our results constructively. He gives an example which IIRC is essentially as follows: </p>

<blockquote>
  <p>Assume that you work for a big software company and your manager asks you for a program to solve a problem. Would it be acceptable to return with two programs and tell your manager one of these two solves correctly but I don't know which one?</p>
</blockquote>

<p>At end, we should keep in mind that although we use the same symbols for classical and intuitionistic logics these symbols have different meanings, and the one to use depends on what we want to express.</p>

<p>For your last question, I think <a href="https://en.wikipedia.org/wiki/Robertson%E2%80%93Seymour_theorem" rel="nofollow noreferrer">Robertson–Seymour theorem</a> would be an example of a theorem that we know it is true classically but we don't have any constructive proof of it. See also </p>

<ul>
<li><a href="https://cstheory.stackexchange.com/questions/12162/are-there-non-constructive-algorithm-existence-proofs">Are there non-constructive algorithm existence proofs?</a></li>
</ul>

CC BY-SA 3.0
2017-10-27T15:54:12.277Z
What is "theory A" and why should I specifically care about proofs inside of it?
Stella Biderman
CC BY-SA 3.0
2017-10-27T21:14:54.250Z
@StellaBiderman: http://blog.computationalcomplexity.org/2003/03/theory-and-theory-b.html
Kaveh
CC BY-SA 3.0
2013-05-23T00:32:55.167Z
2013-05-23T00:43:19.393Z
2017-04-13T12:32:28.077Z
Kaveh
<p>From what I understand (which is very little, so please correct me where I err!), theory of programming languages is often concerned with "intuitionistic" proofs. In my own interpretation, the approach requires us to take seriously the consequences of <em>computation</em> on logic and provability. A proof cannot exist unless there exists an <em>algorithm</em> constructing the consequences from the hypotheses. We might reject as an axiom the principle of the excluded middle, for instance, because it exhibits some object, which is either $X$ or $\lnot X$, nonconstructively.</p>

<p>The above philosophy might lead us to prefer intuitionistically valid proofs over ones that are not. However, I have not seen any concern about actually using intuitionistic logic in papers in other areas of theoretical CS. We seem happy to prove our results using classical logic. For example, one might imagine using the principle of the excluded middle to prove that an algorithm is correct. In other words, we care about and take seriously a computationally-limited universe in our results, but not necessarily in our proofs of these results.</p>

<p><strong>1. Are researchers in theoretical CS ever concerned about writing intuitionistically valid proofs?</strong> I could easily imagine a subfield of theoretical computer science that seeks to understand when TCS results, especially algorithmic ones, hold in intuitionistic logic (or more interestingly, when they don't). But I have not yet come across any.</p>

<p><strong>2. Is there any philosophical argument that they should?</strong> It seems like one could claim that computer science results ought to be proven intuitionistically when possible, and we ought to know which results require <em>e.g.</em> PEM. Has anyone tried to make such an argument? Or perhaps there is a consensus that this question is just not very important?</p>

<p><strong>3.</strong> As a side question, I am curious to know examples of cases where this actually matters: <strong>Are there important TCS results known to hold in classical logic but not in intuitionistic logic?</strong> Or suspected not to hold in intuitionistic logic. </p>

<p>Apologies for the softness of the question! It may require rewording or reinterpretation after hearing from the experts.</p>

CC BY-SA 3.0
2013-05-20T17:13:43.087Z
One aspect of this question has been researched 'to death'. The name for the connection between intuitionistic proofs and programs is [Curry–Howard correspondence](https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence). In brief, programs = intuitionistic proofs, types = propositions, double negation == jumps.
Martin Berger
CC BY-SA 3.0
2013-05-20T22:01:58.297Z
An important TCS result known not to hold in intuitionistic logic but does in classical logic: every program either terminates, or runs for an unbounded amount of time. :)
cody
CC BY-SA 3.0
2013-05-20T22:13:30.217Z
@MartinBerger - yes, but to state my question another way, do we actually care whether the proofs we *write* are intuitionist, or are we only interested in *studying* such proofs abstractly?
usul
CC BY-SA 3.0
2013-05-21T01:35:56.743Z
@cody, a.k.a. [Markov's Principle](https://en.wikipedia.org/wiki/Markov%27s_principle). +usul, I think what you have in mind is not *intuitionistic logic* but *constructive mathematics*. You can't do much in intuitionistic logic alone and it seems to me that your emphasis on intuitionism comes from not distinguishing it from constructive mathematics.
Kaveh
CC BY-SA 3.0
2013-05-21T08:40:48.190Z
@usul Yes, we do care, because according to the Curry-Howard correspondence, intuitionistic proofs are programs in 'nice' programming languages (e.g. no funky control constructs), while genuinely classical proofs are programs in more complicated languages.
Martin Berger
CC BY-SA 3.0
2013-05-21T15:12:32.890Z
@Kaveh: Markov's principle is certainly relevant, but not enough to prove the statement I mentioned (as a joke).
cody
CC BY-SA 3.0
2013-05-22T18:55:17.597Z
@MartinBerger that's an answer to usul's question only if you write all your proofs in a programming language
Sasho Nikolov
CC BY-SA 3.0
2013-05-22T22:30:43.713Z
@SashoNikolov The point of the Curry-Howard correspondence is that proofs, especially intuitionistic ones, are a programming language, at least when you are being precise. Most proofs in TCS (and other forms of maths) are too imprecise for this really to come to the fore. So in this sense it is the lack of precision and rigour in most of TCS that makes the question of intuitionistic otherwise irrelevant. NB I'm not saying that all proofs should be formalised in an interactive proof assistant, because the technology is not yet ready for widespread usage.
Martin Berger
<lo.logic><soft-question><pl.programming-languages><constructive-mathematics>
When does (or should) Theoretical CS care about intuitionistic proofs?
usul
# When does (or should) Theoretical CS care about intuitionistic proofs?

(Asked by: username_0 on 2013-05-20)

From what I understand (which is very little, so please correct me where I err!), theory of programming languages is often concerned with "intuitionistic" proofs. In my own interpretation, the approach requires us to take seriously the consequences of *computation* on logic and provability. A proof cannot exist unless there exists an *algorithm* constructing the consequences from the hypotheses. We might reject as an axiom the principle of the excluded middle, for instance, because it exhibits some object, which is either $X$ or $\lnot X$, nonconstructively.

The above philosophy might lead us to prefer intuitionistically valid proofs over ones that are not. However, I have not seen any concern about actually using intuitionistic logic in papers in other areas of theoretical CS. We seem happy to prove our results using classical logic. For example, one might imagine using the principle of the excluded middle to prove that an algorithm is correct. In other words, we care about and take seriously a computationally-limited universe in our results, but not necessarily in our proofs of these results.

**1. Are researchers in theoretical CS ever concerned about writing intuitionistically valid proofs?** I could easily imagine a subfield of theoretical computer science that seeks to understand when TCS results, especially algorithmic ones, hold in intuitionistic logic (or more interestingly, when they don't). But I have not yet come across any.

**2. Is there any philosophical argument that they should?** It seems like one could claim that computer science results ought to be proven intuitionistically when possible, and we ought to know which results require *e.g.* PEM. Has anyone tried to make such an argument? Or perhaps there is a consensus that this question is just not very important?

**3.** As a side question, I am curious to know examples of cases where this actually matters: **Are there important TCS results known to hold in classical logic but not in intuitionistic logic?** Or suspected not to hold in intuitionistic logic.

Apologies for the softness of the question! It may require rewording or reinterpretation after hearing from the experts.

**Tags:** lo.logic, soft-question, pl.programming-languages, constructive-mathematics
> **Comments:**
> **username_1**: One aspect of this question has been researched 'to death'. The name for the connection between intuitionistic proofs and programs is [Curry–Howard correspondence](https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence). In brief, programs = intuitionistic proofs, types = propositions, double negation == jumps.  
> **username_2**: An important TCS result known not to hold in intuitionistic logic but does in classical logic: every program either terminates, or runs for an unbounded amount of time. :)  
> **username_0**: @MartinBerger - yes, but to state my question another way, do we actually care whether the proofs we *write* are intuitionist, or are we only interested in *studying* such proofs abstractly?  
> **username_3**: @cody, a.k.a. [Markov's Principle](https://en.wikipedia.org/wiki/Markov%27s_principle). +usul, I think what you have in mind is not *intuitionistic logic* but *constructive mathematics*. You can't do much in intuitionistic logic alone and it seems to me that your emphasis on intuitionism comes from not distinguishing it from constructive mathematics.  
> **username_1**: @usul Yes, we do care, because according to the Curry-Howard correspondence, intuitionistic proofs are programs in 'nice' programming languages (e.g. no funky control constructs), while genuinely classical proofs are programs in more complicated languages.  
> **username_2**: @Kaveh: Markov's principle is certainly relevant, but not enough to prove the statement I mentioned (as a joke).  
> **username_4**: @MartinBerger that's an answer to usul's question only if you write all your proofs in a programming language  
> **username_1**: @SashoNikolov The point of the Curry-Howard correspondence is that proofs, especially intuitionistic ones, are a programming language, at least when you are being precise. Most proofs in TCS (and other forms of maths) are too imprecise for this really to come to the fore. So in this sense it is the lack of precision and rigour in most of TCS that makes the question of intuitionistic otherwise irrelevant. NB I'm not saying that all proofs should be formalised in an interactive proof assistant, because the technology is not yet ready for widespread usage.  

---

## 4 answers

### Answer by username_3 on 2013-05-23. Score: 6 | Accepted answer

As I said in the comments, intuitionist logic is not the main point. The more important point is having a constructive proof. I think Martin-Löf's type theory is much more relevant to programming language theory than intuitionistic logic and there are experts who have argued that Martin-Löf's work is the main reason for the revival of the general interest in constructive mathematics.

The computability interpretation of constructiveness is one possible perspective, but it is not the only one. We should be careful here when we want to compare constructive proofs to classical proofs. Although both might use the same symbols, what they mean by those symbols are different.

It is always good to remember that classical proofs can be translated to intuitionistic proofs. In other words, in a sense, classical logic is a subsystem of intuitionistic logic. Therefore you can realize (say using computable functions) classical proofs in a sense. On the other hand, we can think of constructive mathematics as some mathematical system in classical setting.

At the end, formalisms, whether classical or constructive, are tools for us to express statements. Taking a classical theorem and trying to prove it constructively without this perspective doesn't make much sense IMHO. When I say $A \lor B$ classically I mean something different from what I say $A \lor B$ constructively. You can argue what "should" be the real meaning of "$\lor$" but I think that is not interesting if we are not discussing what we want to express in the first place. Do we mean (at least) one of them holds and we know which one? Or do we simply mean one of them holds?

Now, with this perspective, if we want to prove a statement like $\forall x \ \exists y \ \varphi(x,y)$ and we want to relate this to a mapping from $x$ to some $y$ satisfying $\varphi(x,y)$ then the better way to express can be the constructive way. On the other hand, if we only care about the existence of $y$ and do not care about how to find them then the classical way would probably make more sense. When you prove the statement constructively, you are also implicitly building an algorithm for finding $y$ from $x$. You can do the same thing explicitly with a more complicate formula like "the algorithm $A$ has the property that for all $x$, $\varphi(x,A(x))$" where $A$ is some explicitly given algorithm.
If it is not clear why one may prefer the constructive way to express this, think about programming languages as an analogy: you can write a program for the Kruskal's MST algorithm in x86 assembly language where you have to care about lots of side issues or you can write a program in Python.

Now why we don't use intuitionist logic in practice? There are several reasons. For example, most of us are not trained with that mind setting. Also finding a classical proof of a statement might be much easier than finding a constructive proof of it. Or we might care about low-level details which are hidden and not accessible in a constructive setting (see also [linear logic](https://en.wikipedia.org/wiki/Linear_logic)). Or we might simply be uninterested in getting the extra stuff that comes with a constructive proof. And although there are tools to extract programs from proofs these tools generally need very detailed proofs and haven't been user-friendly enough for the general theorist. In short, too much pain for too little benefit.

Here is one possible reason why we don't see much constructive proofs in theory A:
our theorems in theory A are often $\Pi^0\_2$ statements and are proven using not very strong theories (say they are provable in $PA$) and by [a meta-theorem](https://en.wikipedia.org/wiki/Friedman_translation) all of them are also provable constructively (in the constructive counterpart of $PA$). In fact, many theory A results can be proven in theories much weaker than $PA$.

I remember that [Douglas S. Bridges](http://www.math.canterbury.ac.nz/~d.bridges/) in the introduction to his computability theory book argued that we should prove our results constructively. He gives an example which IIRC is essentially as follows:

> Assume that you work for a big software company and your manager asks you for a program to solve a problem. Would it be acceptable to return with two programs and tell your manager one of these two solves correctly but I don't know which one?

At end, we should keep in mind that although we use the same symbols for classical and intuitionistic logics these symbols have different meanings, and the one to use depends on what we want to express.

For your last question, I think [Robertson–Seymour theorem](https://en.wikipedia.org/wiki/Robertson%E2%80%93Seymour_theorem) would be an example of a theorem that we know it is true classically but we don't have any constructive proof of it. See also

* [Are there non-constructive algorithm existence proofs?](https://cstheory.stackexchange.com/questions/12162/are-there-non-constructive-algorithm-existence-proofs)

> **Comments:**
> **username_8**: What is "theory A" and why should I specifically care about proofs inside of it?  
> **username_3**: @StellaBiderman: http://blog.computationalcomplexity.org/2003/03/theory-and-theory-b.html  

---

### Answer by username_5 on 2013-05-21. Score: 7

It is is worth thinking about WHY intuistionistic logic is the natural logic for computation, since all too often people get lost in the technical details and fail to grasp the essence of the issue.

Very simply, classical logic is a logic of perfect information: all statements within the system are assumed to be known or knowable as unambiguously true or false.

Intuistionistic logic, on the other hand, has room for statements with unknown and unknowable truth values. This is essential for computation, since, thanks to the undecidability of termination in the general case, it will not always be certain what the truth value of some statements will be, or even whether or not a truth value can ever be assigned to certain statements.

Beyond this, it turns out that even in strongly normalizing environments, where termination is always guaranteed, classical logic is still problematic, since double negation elimination $\neg\neg P \implies P$ ultimately boils down to being able to pull a value "out of thin air" rather than directly computing it.

In my opinion, these "semantic" reasons are a much more important motivation for the use of intuistionistic logic for computation than any other technical reasons one could marshal.


---

### Answer by username_6 on 2013-05-20. Score: 3

Real-world cryptographic hash functions like MD5 & SHA are keyless. As such, it makes it quite difficult to apply techniques from theoretical cryptography to reason about their security. The simple reason why: for any keyless hash function, there exists a very small program/adversary which outputs a collision under that hash function; namely, a program that has such a collision -- which must exist! -- hard-coded.

Phil Rogaway's paper [Formalizing Human Ignorance: Collision-Resistant Hashing without the Keys](http://www.cs.ucdavis.edu/~rogaway/papers/ignorance.pdf) deals with this problem. In it he shows that some very standard theorems for keyed hash functions (like the Merkle-Damgård construction & hash-then-sign paradigm) can be adapted and re-proven with "intuitionist-friendly" theorem statements applying to unkeyed hash functions.


---

### Answer by username_7 on 2013-05-22. Score: 0

here is a nice chapter on Intuitionistic Logic from a comprehensive online book *Logic for Computer Science*, 300pp.[1] sec 9.5, p210, summary on p220:

> Intuitionistic
> logic
> arose
> out
> of
> the
> constructivist
> movement
> in
> mathematics
> which
> rejected
> non-constructive
> existence
> proofs
> or
> those
> based
> on
> the
> law
> of
> the
> excluded
> middle.
> Recently
> a
> connection
> between
> intuitionistic
> mathematics
> and
> programming
> has
> come
> out
> of
> the
> observation
> that
> propositions
> and
> types
> (in
> the
> programming
> sense)
> are
> equivalent.
> Algorithm
> development
> in
> this
> formal
> system,
> which
> is
> based
> on
> natural
> deduction,
> consists
> of
> writing
> a
> specification
> in
> logical
> notation
> and
> then,
> considering
> this
> as
> a
> type,
> proving
> that
> it
> is
> non-empty.
> Because
> the
> underlying
> logic
> is
> constructive
> the
> proof,
> if
> it
> can
> be
> carried
> out,
> must
> embody
> the
> explicit construction of an object of the appropriate type.

another nearby perspective comes from TCSist Andrej Bauer writing on "Mathematics and computation; mathematics for computers"[2] who proposes basically that "intuitionistic mathematics is good for physics". the presentation is mainly in terms of physics, but for those who consider [CS tightly coupled with physics](https://cstheory.stackexchange.com/questions/2074/physics-results-in-tcs) the ideology will generally carry to TCS.

> **Computational interpretation.** This is the interpretation of intuitionistic logic commonly presented in computer science. We view all sets as represented by suitable data structures—a reasonable point of view for a computer scientist. Then a statement is taken to be true if there exists a program (computational evidence) witnessing its truth.

[1] [Logic for Computer Science,](http://www.cs.waikato.ac.nz/~stever/LCS.pdf) Reeves and Clark

[2] [Intuitionistic mathematics for physics](http://math.andrej.com/2008/08/13/intuitionistic-mathematics-for-physics/) Bauer


---

