[FOM] Current issue of Philosophia Mathematica devoted to mathematical depth

[Josef Urban]

As for abbreviation power, we wrote a system for automated compression of
FOL (TPTP) proofs by introduction of definitions some time ago, but there
are tradeoffs between its efficiency and generality. The extreme definition
of "shortest proof" likely leads to very inefficient notions like
Kolmogorov complexity.
Josef
On Jul 15, 2015 10:32 PM, "Timothy Y. Chow" <tchow at alum.mit.edu> wrote:

> I read some of the papers in this issues and they were interesting, but I
> agree with what some contributors and cited authors said, which is that
> it's not clear if anything deep can be said about mathematical depth.
>
> If one is interested in constructing some kind of mathematical model of
> depth (or of something like depth), then my feeling is that the most
> promising approach is to define depth in terms of a *prover*.  That is,
> depth shouldn't be a property of a theorem, or even a property that is
> relative to a particular proof of a theorem, but should be a property that
> is relative to a particular general-purpose theorem-prover.  I envisage
> some definition of a prover that has severe time and space constraints but
> has a lot of abbreviation power, and that a theorem would be deep *relative
> to the prover* if
>
> 1. the prover cannot find a proof of the theorem within its computational
>    constraints, but
>
> 2. the theorem admits a proof that the prover can verify, but any such
>    proof heavily uses the abbreviation capability.
>
> Unfortunately I don't really see a good way of making precise all the
> vague parts of this proposal.
>
> Tim
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20150722/ba30e49b/attachment.html>