I'll try to keep it short and skip the details of the mathematical framework itself.
Back in the early 1900's there was a school of mathematical logic that denied a certain axiom called the law of the excluded middle, that !!p <=> p. They said that if you used this axiom (roughly) your proof was not "constructive," whereas if you avoided it your proof was "constructive." They went as far as to deny all math that was not constructive (which I think is silly).
Their ideas faded out of popularity among mainstream mathematicians, but their goal was to rewrite the foundations of all mathematics using only constructive proofs, and to their credit they got pretty damn far in certain subjects like real analysis (calculus).
Today, their ideas are seeing a resurgence in the homotopy type theorists (HTTs). Their goal is also to rewrite all of mathematics in a constructive way, but now they have the hindsight of these great tools like category theory and homology and computers and all these great things developed in the mid to late 20th century. So they are working on building this framework and seeing what it can prove.
The HTTs are also claiming that proofs in their framework can be logically checked by a computer (because it is constructive) and one of their main selling points is that their work will eventually lead to "computer assisted mathematics," not in the sense of Stephen Wolfram but rather in the sense that a computer will check your proofs as you prove them and find stupid mistakes.
I personally am not all that excited about HTT, due to what I see as misguided hype around it. My preferred way to view it is as logicians studying a really fascinating new logical system and seeing how far they can push it. Saying things like "I deny all mathematics that's not constructive" and "computers will start doing our proofs for us," makes me cringe. But it is what it is :)
Their goal is also to rewrite all of mathematics in a constructive way,
This is not the goal of HoTT, and also not possible as some mathematics is intrinsically non-constructive.
HoTT allows non-constructive reasoning, see section 3.4 "Classical vs. intuitionistic logic" of the HoTT book http://homotopytypetheory.org/book/. You can say that HoTT derives non-constructive mathematics on top of constructive foundations.
The HTTs are also claiming that proofs in their framework can be logically checked by a computer (because it is constructive)
No. Whether a proof can be logically checked by a computer has nothing to do with whether it is constructive or not. A proof is just a syntactic object. It's just as easy to check if a proof step uses excluded middle or double negation as it is to check whether it uses a construtive principle like /\-introduction. There are many proof assitants that work with classical logic, e.g. Mizar, HOL, HOL light, Isabelle/HOL ... All of SAT-solving works classically.
The novelty of HoTT, and only extension over intensional Martin-Loef type-theory, is the univalence axiom.
A proof in mathematics is not purely syntactic because it's not purely logical. For instance, in some steps of a proof, we do something to both sides of an equation and argue that it is still balanced, based on rules that are outside of logic. Such a step can have a nonconstructive element.
A proof in mathematics is not purely syntactic because it's not purely logical.
This is confusing constructive reasoning with the decision problem for proof validity. They are different things.
The very point of logic, constructive or otherwise, or at least one of the key points for having a logic is to be able to decide whether a given proof object is indeed a valid proof. Valid proofs of course typically also make use of non-logical axioms of the ambient theory. If proof-hood is not decidable, it's not a logic.
Reasoning is constructive if it avoids certain proof principle like LEM (law of excluded middle) or double negation.
Classically, LEM and double negation are equivalent.
Intuitionistically the situation is more complicated, see the discussion in this thread by IngoBlechschmid: We can prove that LEM implies double negation, but not the other way around. Intuitionistically, we can only prove that ⊢¬¬A⊃A, then ⊢A∨¬A, but not ⊢(¬¬A⊃A)⊃(A∨¬A).
For these and related reasons, double negation is not considered constructivistically valid.
Your comment is a good first approximation to the motivation for HoTT! However, let me add a couple of remarks.
Firstly, HoTT can also be used with classical logic, i.e. where you freely use the law of excluded middle. This does not impact the ability to check proofs with the computer in any way.
Secondly, HoTT is the first foundation with which computer-formalized proofs of nontrivial theorems in a subject called "homotopy theory" are possible. In theory, this is possible with any foundational theory; but in practice, the necessary encodings to, for instance, Zermelo--Fraenkel set theory, are too involved for computer formalization.
In HoTT, one can define (and reason about) the basic concepts of homotopy theory straight from "day one". In contrast, with a more traditional foundation, one needs to setup a host of intermediate concepts first (like the real numbers, topological spaces, homotopies, ...). This is no problem for a trained mathematician, but becomes a nuisance when working with proof assistants.
Thirdly, one intriguing aspect of HoTT is that it might be possible to "run" proofs (this is the objective of current research). For example, if you prove that some group contains finitely many elements, the vision is that you could run this proof to find out how many elements it contains. This "computational interpretation" is not unique to HoTT; in fact, this is what the linked nLab article is about. But because of the second point, many more theorems are amenable to such an approach.
A last remark, not pertaining to HoTT but constructive mathematics. A simple reason why one might be interested in restricting oneself to constructive arguments is that thereby they are applicable to more general situations. There is a metatheorem to the effect that "a statement with a constructive proof holds in any topos", where "topos" is a precise formulation of "alternative mathematical universe". Such universes are routinely used in several subjects of mathematics, for instance algebraic geometry (after Grothendieck's revolution).
While constructive reasoning is has many advantages, it has one disadvantage that is rarely pointed out, but sometimes causes real trouble.
Let's say we have a formula A which is classically and constructively true. It may be the case that constructive proofs of A are longer and more complicated than classical proofs of A.
If you are working with an interactive proof assistant, this may be the difference between the proof automation being able to deal with A automatically or not.
This explosion in proof size is the reason why the (perfectly constructive) nominal techniques of Pitts et al have been implemented to a high standard in Isabelle/HOL are are used frequently, but are not really in Coq.
(one of either p or p's inverse must be true -- and thus the other false -- with no third (truth) value allowed), hence also called principle of bivalence.
What you wrote is the principle of double negation.
In general: (~p ∨ p) ⇒ (¬¬p ⇔ p) but not the other way around if I not mistaken? Please correct me if I am wrong.
You are right that for a particular formula p, the implication (~p ∨ p) ⇒ (¬¬p ⇔ p) is an intuitionistic tautology and that the reverse implication is not (in general).
However the situation is different when you quantify over all formulas. If you have (¬¬p ⇔ p) for _any_ formula p, you also have (~q ∨ q) for any formula q (written with a different letter to not get lost in variable capturing issues).
This is because, for any formula q, we have the intuitionistic tautology ~~(~q v q). (Proving this is a fun exercise. If you get stuck, see page 26 of https://github.com/iblech/talk-constructive-mathematics/raw/... or elsewhere on the Internet.) So, if you assume the principle of double negation for all formulas, then in particular you assume that, for any formula q, the implication ~~(~q v q) ⇒ (~q v q) holds. Since the antecedent is unconditionally valid, the consequent is as well. Thus you have the law of excluded middle for q.
You melted my brain. What does “quantify over all formulas” mean?
From the way you state it, that's an interesting perspective. But it seems to be from a perspective of totality which I'm wary of. Not saying you're wrong, going to check out those links. Andrej Bauer was very kind to answer an out-of-the-blue email query of mine once :)
Seriously appreciative of your response, a thousand thanks!
EDIT: Ok, I've read your paper/slides. Very interesting. Don't you show that for specific constructions you can make LEM work for classical proofs with continuation monads? How does that show that _in general_ in constructive mathematics that the implication (~p ∨ p) ⇒ (¬¬p ⇔ p) holds but not its inverse? Also, your bit about rewinding time makes complete sense imho because classical logic is atemporal and continuation monads inject the idea of flowing time into those proofs in a controlled manner.
EDIT 2: I _highly_ reccommend Dennis E. Hesseling's Gnomes in the Fog: The Reception of Brouwer's Intuitionism in the 1920s which I think gives a different slant on what Brouwer actually claimed than what you might imagine if you go with Andrej Bauer's interpretation. I can shoot you a copy if you can't lay your hands on it online :)
Sorry, didn't intend to use so much jargon. By "quantifying over all formulas" I just meant that one has to distinguish between the following two statements:
1. The law of excluded middle holds for a particular formula p.
2. The law of excluded middle holds for _all_ formulas p.
Also note that "formula" just means "formal logical statement", i.e. structured string consisting of v, ==>, and so on.
What do you mean by "perspective of totality"?
Regarding your first edit: There is indeed a metatheorem which says "any classical proof can be turned into a constructive proof". The catch is that this does _not_ apply to all formulas (of course, else the discussion would be moot), but only to formulas of a special kind. Not many formulas are of this kind, but for instance "There exist infinitely many prime numbers" and "A particular Turing machine halts" are (when suitably formulated). If you want to lookup the details, look for "Friedman's Trick".
That the implication (~p ∨ p) ⇒ (¬¬p ⇔ p) holds is because there is a direct proof of this. I didn't show (here or in the slides) that the reverse implication is not intuitionistically valid. A simple way to do this would be to proceed along your lines, that is construct a Heyting algebra in which (¬¬p ⇔ p) holds for a particular element p but in which (~p v p) does not holds for this p. A fancier way would be to look at toposes arising "in nature", not specifically constructed for giving a counterexample.
Thanks for the book recommendation! I'll check it out. I won't have Internet over the weekend but I'd be glad to continue the discussion later.
Your counterexample could work, but it is not obvious that it does so. This is because you also have to give definitions of ∧, v, and ==>, and then check that your definitions satisfy the axioms of intuitionistic logic.
As stated, your example only shows that one can define a function f on a set which contains more than two elements such that f . f = id. But this by itself is a trivial statement.
I didn't check it. If you want to do it (the key step being to verify that the axioms of intuitionistic logic holds for your definitions of AND and OR), you can check Wikipedia for the list of axioms to verify: https://en.wikipedia.org/wiki/Heyting_algebra
If you limit yourself to only constructive proofs, do you even get the real numbers? I'm not very clear on the definition of "constructive," but given that almost all real numbers are non-computable (i.e. most likely, the set of all real numbers you have ever encountered outside of computability theory has the same cardinality as the integers), it doesn't feel very constructive to me. I've always found it odd that we learn early on in discrete mathematics about how the cardinality of the reals is larger than that of the integers and rationals, and yet it seems like you'll never deal with anything from this larger set of reals unless you're studying computability.
Rest assured that (contrary to j2kun's misleading claims) if some of the world's top mathematicians and computer scientists propose a new foundation of mathematics, they don't forget real numbers.
You need to distinguish between non-computable and non-constructive. The proof that the cardinality of the reals is non-countable is perfectly constructive, see [1] for a discussion of these and related issues.
Eh? Your very own link says that there is debate within the mathematical community about whether Cantor's uncountability proof is constructive or not.
I just realised that in my mind uncountable (not in a one-to-one correspondence with the natural numbers) means non-constructive. For me countability just says that we have a (constructive) method for generating a sequence of what would be all the terms in the sequence (if it were ever to terminate which it doesn't) and no term outside the sequence in a non-repeating fashion that is unbounded.
Clearly if some sequence is uncountable it means that one of these criteria fails to hold. Which one? Not the non-repeating stipulation. Not the no term outside the sequence stipulation. It must be the stipulation that every term will be encountered during the generation. So there isn't a (constructive) method for generating uncountable sequences. The reals are uncountable, ergo there is no constructive method for generating the reals.
Where am I going wrong?
NB: I am not saying that you can't have a method for constructing individual reals like e and pi and so on.
Even though there isn't a constructive method of generating uncountable sequences, that doesn't mean that this also assumed from within the logic. In conventional mathematics you can also only write down countably many sequences, but the space of all sequences is still uncountable. We don't assume that the set of all sequences is the set of sequences which we can actually define. Similarly in constructive mathematics we don't say that ALL sequences are generated by some computer program, just that YOU are only allowed to generate sequences in that way.
So this doesn't contradict in any way that Cantor's proof is constructive (which contrary to that wikipedia article, it most definitely is).
Yes, of course. I was coming dangerously close to conflating the fact of a sequence being uncountable with the proof that the sequence is uncountable being constructive. In other words, having no constructive method for generating the reals is not at all the same thing, of course, as having a proof that the reals are uncountable. In fact having a constructive proof that the reals are uncountable indicates to us that there is no constructive method for generating them! Oof. You have to so careful with this stuff :)
I'm familiar with the diagonal argument, but the version I learned in Discrete Math courses defines the reals as little more than a (potentially infinite) series of digits with a decimal point somewhere, which I thought didn't hold up to much scrutiny. But this stuff is way above my mathematics pay grade. :) I stumbled onto the Wikipedia article "Construction of the real numbers" and I have no clue what is going on.
Back in the early 1900's there was a school of mathematical logic that denied a certain axiom called the law of the excluded middle, that !!p <=> p. They said that if you used this axiom (roughly) your proof was not "constructive," whereas if you avoided it your proof was "constructive." They went as far as to deny all math that was not constructive (which I think is silly).
Their ideas faded out of popularity among mainstream mathematicians, but their goal was to rewrite the foundations of all mathematics using only constructive proofs, and to their credit they got pretty damn far in certain subjects like real analysis (calculus).
Today, their ideas are seeing a resurgence in the homotopy type theorists (HTTs). Their goal is also to rewrite all of mathematics in a constructive way, but now they have the hindsight of these great tools like category theory and homology and computers and all these great things developed in the mid to late 20th century. So they are working on building this framework and seeing what it can prove.
The HTTs are also claiming that proofs in their framework can be logically checked by a computer (because it is constructive) and one of their main selling points is that their work will eventually lead to "computer assisted mathematics," not in the sense of Stephen Wolfram but rather in the sense that a computer will check your proofs as you prove them and find stupid mistakes.
I personally am not all that excited about HTT, due to what I see as misguided hype around it. My preferred way to view it is as logicians studying a really fascinating new logical system and seeing how far they can push it. Saying things like "I deny all mathematics that's not constructive" and "computers will start doing our proofs for us," makes me cringe. But it is what it is :)