Beefy Boxes and Bandwidth Generously Provided by pair Networks
Syntactic Confectionery Delight

comment on

( #3333=superdoc: print w/replies, xml ) Need Help??

It need not necessarily be doomed to fail for that reason, if the software involved could be useful enough that from some point an increasing proportion of new maths were produced using it.

Making the technology sufficiently useful is probably the magic part though; fixing existing proofs is also likely to be a big job, since my impression is that even today they are riddled with informal appeals to reason or analogy in a manner that would in many cases be hard to formalise.

Of course any hard step can be left for later, or for someone else, simply by declaring that step as an axiom.

An interesting aspect of this - though also one with the potential to explode the problem space - is that it could make it much easier to see the overlap in accessibility of theorems under different sets of rules of logic.

I think I first started thinking about this way back when I was first reading Godel, Escher, Bach. I spent a lot of time with the Peano axioms described there, and while I could prove things like commutativity and associativity of addition and multiplication easily enough the lack of axioms for handling negatives meant it was impossible to prove something like "every integer is either even or odd":

Ax: (Ey: ((x = (SS0 . y) | (x = S(SS0 . y)))))


In reply to Re^4: What do you know, and how do you know that you know it? by hv
in thread What do you know, and how do you know that you know it? by tilly

Use:  <p> text here (a paragraph) </p>
and:  <code> code here </code>
to format your post; it's "PerlMonks-approved HTML":

  • Posts are HTML formatted. Put <p> </p> tags around your paragraphs. Put <code> </code> tags around your code and data!
  • Titles consisting of a single word are discouraged, and in most cases are disallowed outright.
  • Read Where should I post X? if you're not absolutely sure you're posting in the right place.
  • Please read these before you post! —
  • Posts may use any of the Perl Monks Approved HTML tags:
    a, abbr, b, big, blockquote, br, caption, center, col, colgroup, dd, del, div, dl, dt, em, font, h1, h2, h3, h4, h5, h6, hr, i, ins, li, ol, p, pre, readmore, small, span, spoiler, strike, strong, sub, sup, table, tbody, td, tfoot, th, thead, tr, tt, u, ul, wbr
  • You may need to use entities for some characters, as follows. (Exception: Within code tags, you can put the characters literally.)
            For:     Use:
    & &amp;
    < &lt;
    > &gt;
    [ &#91;
    ] &#93;
  • Link using PerlMonks shortcuts! What shortcuts can I use for linking?
  • See Writeup Formatting Tips and other pages linked from there for more info.
  • Log In?

    What's my password?
    Create A New User
    and the web crawler heard nothing...

    How do I use this? | Other CB clients
    Other Users?
    Others surveying the Monastery: (4)
    As of 2021-03-03 03:23 GMT
    Find Nodes?
      Voting Booth?
      My favorite kind of desktop background is:

      Results (69 votes). Check out past polls.