<div dir="ltr"><div>If I use many postulates, they can't be put as assumptions in the type. I will try to only use postulates when they are trivial or are not in an important path of the theory. <br></div><div>And we'll see if it works.<br></div><div><br></div><div>> One thing I find *very* useful is to have holes in the *formulations* </div>
> of definitions and theorems, rather than just the proofs of theorems. In <br>> particular, this happens when you have a vague idea of what you want to <br>
> prove, with perhaps a clearer idea of how you want to prove what you <br><div>
> don't know yet you want to prove.</div><div><br></div><div>With refinement , I do something similar.</div><div>Here you know what you want to prove but you do not know how to prove it. You have a degree of freedom that you can use to determine the refining protocol.</div><div>For example, to prove that a number is factored by 3, you can choose to have numbers that are factored by 6.</div><div><br></div><div><br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Fri, Jan 18, 2019 at 9:44 PM Martin Escardo <<a href="mailto:m.escardo@cs.bham.ac.uk">m.escardo@cs.bham.ac.uk</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">Let me go to the beginning of this thread.<br>
<br>
I meant to answer earlier but I didn't have time.<br>
<br>
The answer is that this heavily depends on what you want to do.<br>
<br>
1. Suppose you want to formalize all of known mathematics, or, more <br>
modestly, all mathematics is currently taught in undergraduate and <br>
graduate degrees, or even more modestly, some existing mathematics you like.<br>
<br>
I would suggest that, in this case, it makes a lot of sense to adopt a <br>
"top down" approach, and go from what we teach down to the axioms.<br>
<br>
The formal-abstracts project seems to adopt this approach.<br>
<br>
<br>
<a href="https://jiggerwit.wordpress.com/2018/04/09/formal-abstracts-a-long-term-vision/" rel="noreferrer" target="_blank">https://jiggerwit.wordpress.com/2018/04/09/formal-abstracts-a-long-term-vision/</a><br>
<br>
<a href="http://florisvandoorn.com/talks/formalabstracts2018.pdf" rel="noreferrer" target="_blank">http://florisvandoorn.com/talks/formalabstracts2018.pdf</a><br>
<br>
<a href="https://fl60.sciencesconf.org/data/program/T_Hales_1.pdf" rel="noreferrer" target="_blank">https://fl60.sciencesconf.org/data/program/T_Hales_1.pdf</a><br>
<br>
What you haven't proved yet is a postulate or axiom. But perhaps you <br>
want to formulate it as an assumption (to a module or to a <br>
definition/construction/theorem). Otherwise you may end up with 2000 <br>
postulates without knowing which parts of your mathematical development <br>
depends on which fragment of the unformalized mathematical knowledge.<br>
<br>
2. Suppose you want to use a proof assistant such as Agda as a helpful <br>
blackboard to do *new* mathematics. This is something I do often. Many <br>
times I start with a piece of paper and a pencil, and I work until the <br>
moment I need help (to do routine reductions, to test definitions before <br>
I find their definitive form, to test proof approaches that worked on <br>
paper but then reached many cases to test, or many possible induction <br>
hypothesis, or what-you-have in the practice of doing mathematics).<br>
<br>
Then the top-down approach (probably combined with a bottom-up one) <br>
works very well again, using holes rather than postulates as the <br>
preferred mechanism.<br>
<br>
One thing I find *very* useful is to have holes in the *formulations* <br>
of definitions and theorems, rather than just the proofs of theorems. In <br>
particular, this happens when you have a vague idea of what you want to <br>
prove, with perhaps a clearer idea of how you want to prove what you <br>
don't know yet you want to prove.<br>
<br>
Whenever you see 1000 lines of my Agda code, there are 5000 garbage <br>
lines or more needed to get them that I don't show you, just like in <br>
pencil-and-paper mathematics when it reaches the publication status.<br>
<br>
I think Agda and all proof assistants in the world need more of this <br>
kind of black-board / notepad support.<br>
<br>
3. Suppose the only reason you want to use Agda (or something <br>
equivalent) is that you have constructive theorems. You don't care about <br>
formal correctness per se (you trust yourself). Then you may formalize <br>
your theorems so that you can run them. I do this often, particularly <br>
for (what I regard to be) surprising constructive results.<br>
<br>
<br>
4. Suppose you want to experiment with non-standard axioms or axioms <br>
that just don't hold in type theory but are consistent (such as "all <br>
functions are continuous", bar induction, Markov principle, function <br>
extensionality, univalence, etc.). Then you may be tempted to postulate <br>
them. Or maybe to use them as assumptions in modules or <br>
definitions/constructions.<br>
<br>
In general, mathematics (constructive or not) is *all about* going from <br>
assumptions to conclusions/constructions. But I don't think the <br>
postulate mechanism is the best one for this purpose from an engineering <br>
point of view of the development of mathematics. In any case, we are in <br>
early days, and people (developers and users) are experimenting with <br>
this new tool.<br>
<br>
Martin<br>
PS. 5. All this will be used in ways we didn't plan or anticipate, in <br>
any case, like with everything in science and mathematics and human <br>
knowedge and technology in general.<br>
<br>
<br>
<br>
<br>
On 15/01/2019 23:56, <a href="mailto:apostolis.xekoukoulotakis@gmail.com" target="_blank">apostolis.xekoukoulotakis@gmail.com</a> wrote:<br>
> Since now, I have spent days proving trivial mathematical propositions <br>
> without knowing if the general theory/idea is correct.<br>
> <br>
> This, of course, means that the theory is developed while programming in <br>
> Agda. It is not developed before using Agda.<br>
> <br>
> I am thinking of using postulates extensively and prove things on paper <br>
> instead of doing it in Agda.<br>
> It is less safe but much faster. Then check the validity of the main <br>
> Idea with the use of the postulates. Only then try to prove some of the <br>
> postulates that might be a bit tricky.<br>
> <br>
> At least for me, proofs that do not take part in the computation of a <br>
> program can remain postulates.<br>
> <br>
> What is your strategy? Do you use postulates extensively? In my opinion <br>
> this is important enough that it needs to be put in the documentation. I <br>
> have wasted too much time proving trivial propositions and we do not <br>
> have to do that.<br>
> <br>
> _______________________________________________<br>
> Agda mailing list<br>
> <a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
> <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
> <br>
<br>
-- <br>
Martin Escardo<br>
<a href="http://www.cs.bham.ac.uk/~mhe" rel="noreferrer" target="_blank">http://www.cs.bham.ac.uk/~mhe</a><br>
</blockquote></div>