You could just contract equivalent theorems to a point. Maybe also the implications could be coded (colored?) by reverse mathematical strength (EFA, RCA0, WKL0, etc.), though there will be lots of "don't know"s. Charles Greathouse Analyst/Programmer Case Western Reserve University On Tue, Mar 24, 2015 at 11:31 AM, Andy Latto <andy.latto@pobox.com> wrote:
The tricky thing is dealing with the not-uncommon situation where there are a bunch of "equivalent" but difficult theorems. Showing that any one of them implies any other is easy, showing that any of them are true is hard, but you can prove any of them as the "hard" one with minor modifications of the difficult proof.
If you omit all the "can be proved from" between all of them, you hide the important fact of their essential equivalence. But if you include all the equivalences, someone looking for the difficult proof will bounce back and forth seeing all the trivialities, with the difficult proof as one possibility in some of the theorem's database entries, hiding like a needle in a haystack.
Andy
On Tue, Mar 24, 2015 at 10:45 AM, Allan Wechsler <acwacw@gmail.com> wrote:
Guy, have you looked at http://us.metamath.org ? Look, for example, at http://us.metamath.org/mpegif/2p2e4.html.
On Tue, Mar 24, 2015 at 1:38 AM, Guy Haworth <g.haworth@reading.ac.uk> wrote:
Thanks to previous responses and to Dan, Mark, Mike and Tom ... a good set of contributions.
I was asking the question because I was thinking about a database of theorems, showing
- individual theorems as a set of initial 'constraints' leading to a 'result', but also
- showing how other theorems are used to produce the new theorem.
The 'graph' of these theorems is not a hierarchy or even a lattice ... but theorem-equivalences show that it is a more general graph.
Has anyone produced this kind of database of theorems on a computer - with access-software, GUI etc?!
I guess 'Principia Mathematica' was a first demonstration, pre computer.
Somewhere well downstream, we get to '1 + 1 = 2' with the footnote "The above proposition is occasionally useful."
Thank again - Guy
_______________________________________________ math-fun mailing list math-fun@mailman.xmission.com https://mailman.xmission.com/cgi-bin/mailman/listinfo/math-fun
_______________________________________________ math-fun mailing list math-fun@mailman.xmission.com https://mailman.xmission.com/cgi-bin/mailman/listinfo/math-fun
-- Andy.Latto@pobox.com
_______________________________________________ math-fun mailing list math-fun@mailman.xmission.com https://mailman.xmission.com/cgi-bin/mailman/listinfo/math-fun