Formalising Mathematics: An Introduction • Hacker News Board

Re: Formalising Mathematics: An Introduction

#121

Post by rssoconnor » Mon, Feb 22, 2021, 10:34 PM UTC

auggierose wrote: post #116

rssoconnor wrote: post #115

Earlier quoted context omitted.

Fermat's last theorem holds constructively. This is because we can take the entire proof an rewrite it using the "classical fragment" of constructive logic[1]. I don't know if the proof of FLT (appears) to use the axiom of choice or not, but if it does we use Shoenfield's absoluteness theorem to remove any uses of the axiom of choice from the proof. And we are done, because the statement of the theorem in the "classi…

Hi Russell, thank you for clarifying this! So what you are saying is, if the algorithm and its correctness theorem have a certain form (which is usually the case), we can rewrite any non-constructive proof of it in a constructive way? That is very cool! So, even less reason to demand a constructive proof, a non-constructive one is then often good enough even for hard-core constructivists. Do you know if this has been…

I should mention that constructive mathematics, at least when done in dependent type theory, really starts to shine when things that normal mathematicians think of as propositions, are viewed as data. For example, normal mathematicians think of list membership as a predicate, but in dependent type theory, list membership is a value of an inductive family that is effectively an index of where that value occurs in that list (and in particular there could be multiple different values if that item occurs in the list at multiple different locations).

And dependent type theory is gleaming when things that normal mathematicians think of as propositions are not only values, but functions! For example a list l1 being a subset of a list l2 is a function from memberships of l1 (which, remember is data) to memberships of l2. Now you get partial evaluation when working on your proofs and things just magically unify.

I write about these examples in experience I had in "Taking Propositions as Types seriously" @ http://r6.ca/blog/20171008T222703Z.html>.

There is a practical difference between Principia Mathematica taking 370 pages to prove 1 + 1 = 2 versus dependent type theory's proof `refl_equal 2`. (I'm exaggerating, but only a little).

Re: Formalising Mathematics: An Introduction

#122

Post by auggierose » Tue, Feb 23, 2021, 4:14 AM UTC

rssoconnor wrote: post #121

auggierose wrote: post #116

Earlier quoted context omitted.

Hi Russell, thank you for clarifying this! So what you are saying is, if the algorithm and its correctness theorem have a certain form (which is usually the case), we can rewrite any non-constructive proof of it in a constructive way? That is very cool! So, even less reason to demand a constructive proof, a non-constructive one is then often good enough even for hard-core constructivists. Do you know if this has been…

I should mention that constructive mathematics, at least when done in dependent type theory, really starts to shine when things that normal mathematicians think of as propositions, are viewed as data. For example, normal mathematicians think of list membership as a predicate, but in dependent type theory, list membership is a value of an inductive family that is effectively an index of where that value occurs in that…

Personally, dependent types never worked for me the way I thought they would when I first learnt about them (I was quite enthusiastic about them and about constructive mathematics initially). I found them too verbose, and too nitpicky. Your list membership is a great example: Usually, I am not concerned with where in the list does the element occur, list membership as a predicate is perfectly natural and usually adequate (but admittedly, if that's the only use case, better use a set than a list). I think an elegant mathematical argument wins not only by what is said, but also by what can be left unsaid.

But yes, being able to work with functions as data is also very important! That's why I am pursuing a combination of simple type theory and set theory as the foundation of a theorem prover, as I have outlined here: http://www.practal.com

Re: Formalising Mathematics: An Introduction

#123

Post by vcdimension » Tue, Feb 23, 2021, 2:07 PM UTC

rssoconnor wrote: post #118

auggierose wrote: post #116

Earlier quoted context omitted.

Hi Russell, thank you for clarifying this! So what you are saying is, if the algorithm and its correctness theorem have a certain form (which is usually the case), we can rewrite any non-constructive proof of it in a constructive way? That is very cool! So, even less reason to demand a constructive proof, a non-constructive one is then often good enough even for hard-core constructivists. Do you know if this has been…

Yes, I realize this arguments cuts both ways. One way is that you can write all these theorems in constructive logic, so there is no need for classical axioms. And the other way, is that users should freely use classical axioms because they can be mechanically removed. Myself, I've never seen an automated theorem prover that will perform this sort of translation automatically. I have, on rare occasion, gone through b…

How difficult would it be to write a Coq plugin to perform these translations? The thing I like about Coq is that it appears to have better tooling than the other theorem provers (coqtop, proof-general for emacs), and you can extract code for other programming languages. I haven't looked in great detail at the alternatives though.

Re: Formalising Mathematics: An Introduction

#124

Post by auggierose » Tue, Feb 23, 2021, 3:28 PM UTC

vcdimension wrote: post #123

rssoconnor wrote: post #118

Earlier quoted context omitted.

Yes, I realize this arguments cuts both ways. One way is that you can write all these theorems in constructive logic, so there is no need for classical axioms. And the other way, is that users should freely use classical axioms because they can be mechanically removed. Myself, I've never seen an automated theorem prover that will perform this sort of translation automatically. I have, on rare occasion, gone through b…

How difficult would it be to write a Coq plugin to perform these translations? The thing I like about Coq is that it appears to have better tooling than the other theorem provers (coqtop, proof-general for emacs), and you can extract code for other programming languages. I haven't looked in great detail at the alternatives though.

Isabelle also has code generation facilities and very good tooling, and uses classical logic.

Re: Formalising Mathematics: An Introduction

#125

Post by vcdimension » Tue, Feb 23, 2021, 4:38 PM UTC

auggierose wrote: post #124

vcdimension wrote: post #123

Earlier quoted context omitted.

How difficult would it be to write a Coq plugin to perform these translations? The thing I like about Coq is that it appears to have better tooling than the other theorem provers (coqtop, proof-general for emacs), and you can extract code for other programming languages. I haven't looked in great detail at the alternatives though.

Isabelle also has code generation facilities and very good tooling, and uses classical logic.

Thankyou, I'll have a look.