Can Proof Technology Even Do this?
dennis at logicalphalluses.net
dennis at logicalphalluses.net
Sun Feb 28 03:18:35 EST 2021
> a formal system S and a sentence phi, and the problem is to prove phi from S
You seem to equate "proof assistants" (ITPs) with "automated theorem
provers" (ATPs). Proof assistants assist with proving, they don't do the
proving (entirely) for you. Almost every proof assistant contains some
or several ATPs for convenience, but some don't (e.g. metamath).
I think you're making a mistake by measuring the success of ITPs merely
by how powerful they are as ATPs.
> A. Start with the axioms of Peano Arithmetic in the language of
> 0,S,+,x, the usual with finitely many axioms and the induction scheme.
> Prove: every number is of the form n+n or n+n+1 but not both.
> B. Same start as A. Prove: commutative, associate laws for +,x, and
> the distributive law, and also the monotonicities.
I'm pretty sure there isn't a single ITP that does *not* have proofs for
these, so I would consider that challenge to be solved by every ITP. If
your challenge is that the system should be able to prove them
automatically entirely with no or only few hints, then there will be
failures. But that's not what ITPs are for.
The value of ITPs lies in lots of small conveniences that allow to
express proofs in such a way that they can be *checked* to be correct,
and to help with filling in gaps via ATPs and other means. By doing so,
they allow you to find gaps or flaws in your reasoning, structure your
proofs more clearly and refine your understanding of one. The value also
lies in making any notion, notation, definition, statement etc.
unambiguous by design, rather than relying on a reader having to know
(or, rather often, assume to know or guess) what they mean. They make
the *semantics* of statements accessible for e.g. search.
ITPs have other problems in my opinion, e.g. that the conveniences they
bring currently don't outweigh the enormous cost of familiarizing
oneself well enough with a system and its library to survive a
cost-benefit-analysis, and the result looks nothing like math looks on
paper. But those are ultimately problems with the surface languages, not
with the systems themselves as they operate on internal abstract syntax
trees (which is why I'm currently working on a system that uses
unrestricted plain latex as input). But "they don't find proofs
automatically for arbitrarily complicated statements and in the same way
as a human would do it" is not a problem I would measure ITPs on (alone).
Cheers
-- Dr. Dennis M. Müller
"To do mathematics is to be, at once, touched by fire and bound by
reason. This is no contradiction. Logic forms a narrow channel through
which intuition flows with vastly augmented force"
- Jordan Ellenberg (How Not to Be Wrong)
More information about the FOM
mailing list