Can Proof Technology Even Do this?

[Harvey Friedman]

On Sun, Feb 28, 2021 at 9:08 PM <dennis at logicalphalluses.net> wrote:
>
>
> > a formal system S and a sentence phi, and the problem is to prove phi from S
>

DENNIS

> 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.

ME

I tried to make clear what I was trying to do by seeing what can be
done with the proof technology AS PURE AUTOMATED UNAIDED DEDUCTION.

The reason I am trying to do this is to UNDERSTAND THE JUMPS THAT THE
TECH IS ABLE TO MAKE.

In a real situation, one has vast libraries and special decision
procedures and the kitchen sink to use in order for the tech to prove
something new.

BUT if the tech is going to do ANYTHING LIKE what people who think
(wrongly I think) that Proof Assistants are really going to make a
difference with Garden Variety Professional State of the Art
Mathematical Advances - other than LIMITED SPECIAL THINGS WE ALL SEE
THE TECH DO, the Tech is going to have to make SERIOUS JUMPS.

So I was trying to find UNCLUTTERED situations where it is a matter of
PURE JUMPS.

Of course I am aware that any Library has for decades had those PA
examples as an integral part. AND the most elemental of what I was
looking at is in the language of PRESBURGER and so decision packages
are available for them. Also there are extended decision packages
which certainly cover NO SQRT(2). BUT what is the most general kind of
statement that they cover?

DIGRESSION. What is the most powerful decision procedure we have for
arithmetic statements that goes into ring statements (i.e., beyond
Presburger) and covers things like NO SQRT(2)? I.e., what are some of
the really powerful and understandable decision procedures out there
for fragments of arithmetic?
>
For my own work, I pretty much know when Tech is going to be useful.

I have from time to time made the following move: IS THE FOLLOWING
TRUE FOR ALL *SMALL* CASES?, whatever I am looking at. However, that
is not the typical thing that I do although I plan to do more of it.

FOR EXAMPLE, I had a project which got some traction, but has since
FALLEN THROUGH THE CRACKS.

QUESTION. ARE ALL SMALL DIOPHANTINE EQUATIONS PROVABLE OR REFUTABLE IN
(FRAGMENTS OF) PA?

FIrst of all, some simple TECH is useful to organize and compile these
small equations. But it would be useful for the TECH to automatically
search for solutions to get rid of the easy ones so I can concentrate
on the interesting ones.

But how about this problem?:

FIND A FUNDAMENTALLY BASIC SIMPLE QUESTION AT THE LEVEL OF GIFTED HIGH
SCHOOL STUDENTS, IN THE INTEGERS OR RATIONAL NUMBERS, THAT CANNOT BE
ANSWERED IN THE USUAL ZFC AXIOMS.

I submit to you that TECH is not going to help with this. Of course
TECH can be used to formally verify my work on this, but WAY WAY WAY
WAY after I have very polished complete manuscripts with my personal
proofs.

Harvey Friedman