6
$\begingroup$

The question is motivated by this surprising sentence from Freek Wiedijk's The QED Manifesto Revisited.

I agree that the QED-like systems that exist today are not good enough to start developing a library as is described in the QED manifesto.

Surprising to me, that is, who had not heard of the QED project before.

(Edited after A. Bauer's answer) OK, time I mopped up.

I was 1st introduced to the Curry-Howard correspondence back in school days long, loooooong ago; I understood it as s/th along the lines of "Any computer program is a constructive proof that inhabitation of its input type entails inhabitation of its output type"; my very next question was, "OK then, if instead of any program we restrict ourselves to programs that model mathematical proofs in classical logic, what would be the proper type system(s) for them?". I guessed it had to be existential types, guarded subtypes (meaning types restricted by any formula; so that you would write e. g. "let x: {r : Real | !(r : Rational)}" if all you mean is to express that x is irrational), or such like stuff; then I let the matter rest and turned to more pressing ones, to wit, getting a degree.

If I had pressed it further at the time &, instead of the title question, asked "What types are to classical logic as simple types are to constructive logic?", maybe I'd have been answered "There are no such types: there is no need to extend or otherwise modify simple types for classical logic, since it is encompassed in constructive logic. Go get some understanding of type theory, and learn how to do with them. "

If I had asked again at the time the QED manifesto was issued, a plausible answer might have turned to "They're called refinement types. What's wrong with them is, they're a pointless gadget: the problem they solved was not a foundational one, and introducing them did not present type theory with any new challenge. So all the papers they deserve have been written already. "

Returning to it now, it seems to me the natural way to attack the QED challenge would be: 1. to set forth a serious answer to my old question, 2. design the corresponding language, 3. build the proper language tools, including, in the end, a full-fledged proof assistant (probably posing as a type checker), 4. look what happens. In a programming language with refinement types, the C-H correspondence now works as: subprograms returning (refinements of) void model conjectures, their bodies model proof outlines, assertions in the bodies model steps in the proof, Skolem functions arise naturally if handlers for failed assertions are allowed. Then, verified theorems in predicate logic are those subprograms in which the type checker has been able to reduce all assertions to tautologies.

What hopefully would happen if a suitable extension to such a language had become popular is, useful tools could start developing, such as doclets to turn fragments of source code to academic papers; people might get used to writing in it just to convert formulas from .pdf to .ps, or to save themselves the hassle of adjusting to the style guides of every other journal they submit to; later, we might dream of replacing arXiv with a global GitHub repository of their works. This could take place long before any proof assistant worth mentioning existed for the language.

Given Wiedijk's paper though, the real story must have been quite different. It reads like people trying to endow dependent types with refinement soon hit some snag and, instead of developing proof assistants (Edit: read formal languages and tools) for classical logic, they went happily to rewrite classical math for constructive logic. (Edit) With predictable results: mathematicians have been accepting a certain style of proof outline for some time now and non-mathematicians are used to it, so if it is too arcane work to make it understandable by a automated checker, they will rather dispose of the proof checker than of the proof.

Turn away for a minute from what dependent types mean, and look how they would be used in a language purporting to be strongly typed. The user is student X with a major in control systems, a hobby in Java programming, currently at grips with an intro to topological groups. So far, he has managed to translate "pick any dyadic integer " as "let x: Integer(2)" for proof-checking freeware he downloaded a minute ago, then "consider first the case of a rational integer" to "let x1:Integer(2)*Rational"; now attacking "pick some irrational number x and consider the fractional parts of the p.x's, p ranging over Z: obviously, blah blah blah". Not understanding a word of type theory, he first looks for a way to say "let x: Real - Rational", finds none, looks harder, still finds none, then let go & turns back to more pressing matters, to wit, control systems.

Of course, if student X had access to such a language as I sketched, he would have given up long before he got any proof automated. No harm done, though: what he wants is to understand TG's, not that a computer program understand it in his stead, nor to understand type theory. All he needs is to keep his fingers busy while reading, and I advocate giving him a productive way to do just that.

My read of Wiedijk's paper is, if you bar student X from modelling things the way he understands them, he will turn to what he considers more pressing matters, regardless of how pressing your need for computer-checkable proofs, and how deep your understanding of what the modelling language guarantees. It explains how we still lack a free-access, widely-known, low-quality, multi-audience, computer-interpreted codebase of mathematical theories the way we have a free-access, widely-known, low-quality, multi-audience, human-readable textbase of common lore.

Edit Just to clarify: the codebase of mathematical theories in question would still be as far away from being computer-checked, as is WP from auto-generating ontologies for the subject matter of its articles; light-yrs away. The (hopeful) progress lies in the rest of the road being mostly for metamathematicians & software engineers to tread, with the part of "ordinary" mathematicians perceived as non-problematic.

Hence my question: what type systems are the natural ones to express assertions in classical logic? Or maybe I should have titled this post "What types are to dependent types, as refinement types à la Freeman-Pfenning are to simple types?". Anyway, what have they that makes their theory so unsavory?

$\endgroup$
  • 9
    $\begingroup$ I'm confused as to why you think restricting the 'types' under consideration will make the program corresponds to classical proof. In this correspondence type corresponds to propositions, and proposition are the same in classical and constructive mathematics. $\endgroup$ – Simon Henry Feb 20 at 17:31
  • 13
    $\begingroup$ This question combines what seems like a basic misunderstanding of how predicate logic relates to type theory (as per Simon Henry’s comment), a disinterest in learning further about it (“turned to more pressing matters”), and some quite unnecessary inflammatory tone (the suggestion that typical mathematicians “loathe constructive logic with all their guts”). That’s not exactly a good approach for engaging with people who work in the area. $\endgroup$ – Peter LeFanu Lumsdaine Feb 20 at 18:06
  • 1
    $\begingroup$ @PeterLeFanuLumsdaine it is quite possible I misunderstand what type theory is: I come from computer science, not math. You're quite welcome to enlighten me, and it seems to me I'll make it easier for you, if I state right from the start what my (mis)understanding is. You are quite right that turning to more pressing matters shows disinterest in learning further: the pressing matter was to get a degree in mining, & that was 30yrs ago. It seems to me though, that self-teaching in type theory does witness some interest in it. $\endgroup$ – François Jurain Feb 20 at 20:43
  • $\begingroup$ @PeterLeFanuLumsdaine My prose about J. R. Mathgeek was not in earnest, and I am surprised, & sorry, that it could set anyone aflame; I'll edit the post. $\endgroup$ – François Jurain Feb 20 at 20:48
  • 5
    $\begingroup$ Joyal proved that a cartesian-closed category that has double-negation elimination is a preorder, i.e. there is at most one morphism between any two objects. Todd Trimble mentioned this here: mathoverflow.net/a/43285/61785 $\endgroup$ – Robert Furber Feb 21 at 2:12
10
$\begingroup$

A good starting point to learn about type theories for classical logic is the $\lambda\mu$-calculus introduced in 1992 by Parigot in λμ-Calculus: An algorithmic interpretation of classical natural deduction, which extend the $\lambda$-calculus to give a computational interpretation of classical natural deduction.

For the next step, I would recommend reading the research summary on Hugo Herbelin's home page. Chasing some of the references listed there, you will learn how incorporating control operators into type theory yields a computational understanding of excluded middle.

For a modern take on the role of excluded middle in Martin-Löf type theory I recommend reading at least Section 3.4 of the HoTT book. The important bit to take away from there is the fact that excluded middle can coexist with the rest of homotopy type theory quite naturally.

You speak of proving correctness of programs, possibly using classical logic. For that you can use a system based on refinement types, such as F*. Also note that proving correctness of programs is an activity unlike formalization of traditional mathematics, so do not expect a single tool to work equally well for both of them.

In my opinion the presence or lack of excluded middle in a proof assistant has very little to do with it being useful for formalization. Of course, if you want to formalize classical mathematics then you need excluded middle (but much less frequently than most mathematicians expect). Most modern proof assistants let you postulate excluded middle quite directly and use it to your heart's content, so that cannot be the show stopper. One of the most popular proof assistants is Isabelle/HOL, which has excluded middle built in, but that does not make it significantly more successful in comparison with other formalization tools.

It is a bit difficult to understand what precisely you are getting at in your long discussion, but I would venture to say that you've misidentified negation and excluded middle as the culprit. I am not even sure whether you think that Martin-Löf type theory has no notion of negation – of course it does! In fact, the problems faced by your student X has nothing whatsoever to do with type theory. Student X would face essentially the same obstacles if they used any other formal system, such as first-order logic and set theory, or higher-order classical logic. Your student X is quite naive to think that formalization of mathematics is just a simple exercise in translation from English prose. It may be true that usability is decided by the users, but the users' abilities play a role as well.

| cite | improve this answer | |
$\endgroup$
  • $\begingroup$ Thanks for the refs! I agree that my discussion need not be made any clearer by its sheer length; I think you mostly got it right, and if I can compress it to a comment on your answer I'll remove it from my post. $\endgroup$ – François Jurain Feb 23 at 1:41
  • 7
    $\begingroup$ Experience shows that (1) it is possible to formalize proofs written in English, (2) ordinary mathematicians do not know enough formal logic to do it without some amount of training (this is a matter of fact, not a criticism), and (3) large-scale formalization is a software engineering problem that mathematicians have not met before in their work. By the way, your $x : \lbrace z : A \mid \phi(z)\rbrace$ is refinement types that I mentioned above (or dependent sums if you prefer dependent type theory). $\endgroup$ – Andrej Bauer Feb 23 at 11:48
  • 1
    $\begingroup$ your 3 counts summarize my point more clearly than I could do myself. I'll only add to (2): ordinary mathematicians and non-mathematicians, and (4): none of the above is sufficient ground to discourage them before they even tried their hand at it, produced s/th useful for metamathematicians & software engineers to start with, and only then, discovered they lack the training to fully formalize their output al by themselves. $\endgroup$ – François Jurain Feb 26 at 13:01
  • 4
    $\begingroup$ @FrançoisJurain: of course, I am not arguing against formalization. In fact, I work in the area and am trying to promote it. But I also try to have a critical position on what I am doing. $\endgroup$ – Andrej Bauer Feb 26 at 13:58
  • 1
    $\begingroup$ I understand Wiedijk as also critical on what you are doing, whereas I do not deem myself competent as a critic. The way I read his paper, in spite of your best efforts to promote formalization, discouragement is just part of the current landscape. I suggest it comes from the strangeness (to the non-type-theorist eye) of the available languages, not from arguments. $\endgroup$ – François Jurain Mar 4 at 15:41

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.