[FOM] Certificates are fully practical

[Alan Weir]

"what counts is that whenever someone hands you a putative
certificate for a proof (which therefore necessarily is finite and quite
small compared to the examples you had mentioned"

Arnold Neumaier (original posts below).

For sure: what convinces us (leaving aside taking computer output as authority) is necessarily something quite small. 

But we might be interested in modelling our actual bits of reasoning to try to come to some reflective view on it (though this type of modelling can interact with what is modelled, unlike cosmology, but perhaps like finance) and we do that through formal languages. We can't set bounds on the size of wffs and proofs in such languages which are realistic in the sense of close to the size of informal persuasive proofs. For one thing, wffs and proofs are closed under complexity-forming operations and cut-offs would be arbitrary. 

More importantly, abbreviation and notational innovation abound and generate failures of 'downward closure'. By abbreviating a formula or proof schema by a small symbol, or group of symbols we can quickly create graspable terms such that not all constituents or formally smaller terms can be graspable. This I think, does for strict or ultra-finitism. We can't prove anything systematic about our formal modelling, our idealisations of utterances and inferences, without using techniques such as definition by induction via freely generated sets. But there is no finite bound on what we can concretely realise in such systems such that all and only the wffs or proofs less than that bound are graspable. 

So we have to accept formal idealisation way beyond what is concretely realisable. What I have questioned is whether, once we reject strict finitism,  a finiteness restriction on this idealisation is well-motivated. 

'No mathematician cares (unless they work in mathematical logic or set
theory) what happens with proofs that are significantly longer than
that." (Arnold Neumaier)

But our formal idealisation of mathematical practice can (and has) fed back into mathematical practice, and different views about idealisation can have different implications. Thus I am happy to accept the law of excluded middle for PA because a persuasive informal induction shows that PA using the omega-rule is negation-complete (even using logics lacking LEM as the framework). And this sort of result can be extended using more powerful infinitary logics through simple type theory. (So it should be clear, re Nik Weaver's comment below, that I am definitely not trying to discredit infinitary mathematics!)

However, responding to Timothy Chow's observations below, I'm not aware of infinitary logics which extend finitary logic in a natural way and in which ZFC is a negation-complete theory. Thus in that case, assuming LEM for CH is, I think,  problematic. Of course one can investigate what is classically derivable from ZFC. But I am sympathetic to the view that one shouldn't assume that either CH holds or it doesn't (even in informally investigating what is provable using a given formal logic from ZFC). 

This perspective doesn't make much sense to a hard-core platonist of course. For her, there is the determinate realm of mathematical truths independent of the means feeble humans have for figuring it out. Sometimes, if we somehow or other, despite the divorce between this realm and us,  alight on 'correct' axioms, we can get a handle on it, in other cases not. But if one thinks of mathematical truth as at least closely intertwined with mathematical proof, then how exactly we should idealise our actual practices of proving, practices which can result only in very small structures, can make a difference to how one thinks our actual informal procedures (whether we should use classical dilemma, say) should go.

Best

Alan Weir

PS when I wrote (Vol 129 Issue 26) 

'if k is the highest-order logic which will ever be used by any mathematicians in the universe (so I am presupposing this is finite)'

I meant 'I am presupposing k is finite'; apologies for the ambiguity.


Today's Topics:

   1. Re: Certificates are fully practical (Arnold Neumaier)
   2. Re: Certificates are fully practical (Timothy Y. Chow)
   3. Re: Certificates are fully practical (Nik Weaver)


----------------------------------------------------------------------

Message: 1
Date: Sat, 28 Sep 2013 09:58:37 +0200
From: Arnold Neumaier <Arnold.Neumaier at univie.ac.at>
To: Foundations of Mathematics <fom at cs.nyu.edu>
Subject: Re: [FOM] Certificates are fully practical
Message-ID: <52468C2D.4020107 at univie.ac.at>
Content-Type: text/plain; charset=ISO-8859-1; format=flowed

On 09/27/2013 01:07 AM, Alan Weir wrote:
> In general, I remain to be convinced that there is a sense of 'in principle possible' which is at all helpful in philosophy of mathematics, one in which, for example, all finite proofs are 'in principle' graspable but no countably infinite one is.  And my point is not, of course,  that infinitary proofs are unproblematic, from a naturalistic, anti-platonist standpoint. Rather it is that all but a tiny fragment of finitary proofs are problematic from that perspective; the suggestion is that it is unclear why a satisfactory resolution of that problem (if there is one) will apply only to finitary idealisations and not infinitary ones. Hope that's clearer.

 From a mathematician's point of view, what counts is not whether or not
there is a proof of a statement - there are countless unproved
conjectures in mathematics.

Instead, what counts is that whenever someone hands you a putative
certificate for a proof (which therefore necessarily is finite and quite
small compared to the examples you had mentioned), a mgroup of
athematicians (possibly aided by computers) can verify or disprove the
associatited claim with an algorithm that can be executed by them in a
reasonable time, small enough that they don't lose interest.

No mathematician cares (unless they work in mathematical logic or set
theory) what happens with proofs that are significantly longer than
that. Thus a foundation of mathematics that guarantees this - for the
collection of concepts thaey are using and generating with their
definitions - is fully adequate.


Arnold Neumaier






------------------------------

Message: 2
Date: Sat, 28 Sep 2013 14:49:13 -0400 (EDT)
From: "Timothy Y. Chow" <tchow at alum.mit.edu>
To: fom at cs.nyu.edu
Subject: Re: [FOM] Certificates are fully practical
Message-ID: <alpine.LFD.2.03.1309281435280.26836 at alum.mit.edu>
Content-Type: TEXT/PLAIN; format=flowed; charset=US-ASCII

Alan Weir wrote:

> I prefer the following story: a crazed gunman enters your class and says
> he'll kill you unless you count from one to 10 to the power 35- with no
> gaps- in the next minute. A student helpfully remarks 'well, it could be
> worse: he could be asking you to count to epsilon_0' (and then starts
> whistling 'always look on the bright side of life' from Life of Brian).

What I believe your parable shows is the following: We know already that
the continuum hypothesis is neither provable nor disprovable in ZFC.  It
would be interesting to strengthen this result by showing that there is no
infinitary proof or disproof either, in some suitable sense of "infinitary
proof."

That is, "infinite" is not a perfect stand-in for "infeasible"; perhaps a
stronger notion of infinity is a better one.  But this doesn't contradict
my point that "infinite" is a worse stand-in for "feasible" than "finite"
is.

> In general, I remain to be convinced that there is a sense of 'in
> principle possible' which is at all helpful in philosophy of
> mathematics, one in which, for example, all finite proofs are 'in
> principle' graspable but no countably infinite one is.

Like most radically skeptical positions, yours is unassailable if you
insist on digging in your heels.  I guess you would also argue for the
following positions:

1. "Polynomial time" is a problematic model of feasible computation.
So hypercomputation is a better model.

2. "Natural numbers" are a problematic model of ordinary counting.
So infinite ordinals are a better model.

Tim


------------------------------

Message: 3
Date: Sat, 28 Sep 2013 14:57:28 -0500 (CDT)
From: Nik Weaver <nweaver at math.wustl.edu>
To: fom at cs.nyu.edu
Cc: Alan Weir <Alan.Weir at glasgow.ac.uk>
Subject: Re: [FOM] Certificates are fully practical
Message-ID: <alpine.LRH.2.00.1309281428100.10507 at troi.wustl.edu>
Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed


Alan Weir wrote:

> In general, I remain to be convinced that there is a sense of 'in
> principle possible' which is at all helpful in philosophy of
> mathematics, one in which, for example, all finite proofs are 'in
> principle' graspable but no countably infinite one is.

Alan, this passage makes it seem like you feel the goal of the
philosophy of mathematics is to justify finitary mathematics and
discredit infinitary mathematics ... and the notion of "possibility
in principle" is not helpful toward that goal.  Surely this is not
what you meant?

It seems to me that if we don't begin with a preferred outcome in
mind, then the notion of possibility in principle could be very
valuable in helping us to answer foundational questions.

For instance, E. B. Davies has described a persuasive scenario in which
a machine performs one step of a computation, then builds a smaller,
faster version of itself and instructs it to perform the next step.
The envisioned result is a cascade of ever-smaller and -faster machines
which collectively perform an infinite computation in a finite amount
of time.  Thought experiments like this could help convince us that
countable computations are mathematically legitimate, regardless of
whether or not they are physically possible in our universe.
(E. B. Davies, Br J Philos Sci (2001) 52 (4): 671-682.)

Nik Weaver
Math Dept.
Washington University
St. Louis, MO 63130 USA
nweaver at math.wustl.edu


------------------------------

_______________________________________________
FOM mailing list
FOM at cs.nyu.edu
http://www.cs.nyu.edu/mailman/listinfo/fom


End of FOM Digest, Vol 129, Issue 27
************************************