[FOM] Possible worlds

[Mirco Mannucci]

---- "Timothy Y. Chow" <tchow at alum.mit.edu> wrote:

>
> The suggestion that some have made, of imposing some kind of limit on the
> length or intricacy of the deductive consequences allowed (where the limit
> depends on context, I suppose), also sounds promising.


and, in reply to Joe Shipman's  objection,


> The relevant notion of "feasibility" doesn't have to be a cleanly defined
> mathematical notion that applies uniformly to all utterances; it can vary
>from statement to  statement, encompassing whatever limited set
> of deductions are relevant  for analyzing the meaning of the statement
> of current interest.  For  example, the set of deductions could be just
> the deductions that a particular person finds "obvious" at a given time.


The apparent difficulty with feasibility and its possible use for this
thread's discussion vanishes like fog in the sun by realizing that,
contrary to common interpretations (*), this notion is, and will always
be, a CONTEXTUAL one.

Now, Tim's suggestion is sound: a proof could be defined as feasible if it can be easily
generated from a given knowledge base available to the mathematical community (or to an individual)
at a given point in time.

For instance, the proof could be a variant of a difficult but well-known theorem, or it could be
obtainable in a few steps by combining the proofs of several already established facts.
Indeed, studying the history of mathematics, one immediately observes that, oftentimes, a hard open
question is eventually settled by "shifting paradigm", to borrow Kuhn's
jargon.

One example for all: Post's problem. Many first-class logicians tried to settle it, and failed,
till Friedberg & Muchnick, two young and relatively unexperienced fellows,
introduced a radical new method, finite injury. Subsequent research
in recursion theory incorporated finite injury, creating an unprecedented
chain of new results and insights in the field.

Incidentally, Wiles' result, albeit a monumental tour de force, does NOT appear to be one of
these  paradigm shifts, which (in my mind) leaves open the possibility
that some new and more manageable proof will in due time crop up on the math horizon.

The foregoing observation clearly shows that thinking a proof hard only if its length is enourmous
or if the amount of symbols it utilizes is huge, is unduly restrictive in most cases.

However, I believe that we CAN and we SHOULD turn the informal concept
of feasible proof into a full-fledged chapter of formal proof theory.

Quite simply, two things can be done:



1) study feasible proof theory abstractly, ie. without analyzing the feasibility predicate
(essentially treating it as a  primitive notion), and moving on to define
feasible consequences of a theory, feasible speed-ups of a proof, etc.

2) investigate new measures of complexity for proofs, beyond the familiar ones.
I am no proof theorist, but I know that this program has already started, using geometric
ideas such as logical flow graph, proof nets, etc. My impression is that we
are still in the infancy of Feasible Proof Theory, but I would bet that this
century will witness a LOT of work in this area.



Tim's informal notion could be made rigorous by formalizing RELATIVE FEASIBILITY
of proofs, i.e. feasibility GIVEN an assigned knowledge base of mathematical
techniques, tricks, examples.



John McCarthy wrote:

> I think partial possible worlds are useful, although I didn't formally
> use them in the puzzles article.  I am perfectly willing to use
> partial possible worlds in which FLT is false, and  it is unlikely to
> get me into contradiction, since the proof of FLT is far beyond my
> ability to follow.


Indeed, in a posting of few months ago, I mentioned Partial Finite Term Models
(PFTM) of arithmetics (http://cs.nyu.edu/pipermail/fom/2006-August/010730.html, section 3).

Basically, they are finite fragments of the familiar term model, obtained by considering
only a finite family of closed terms, and when their identification and ordering is
confined to employing only feasible proofs. There is nothing special about
arithmetics here: every FOL theory has its collection of PFTMs (in fact,
the standard term model contruction used in the completeness theorem can be seen as
"passing to the limit" over the lattice of PFTMs).

The PFTMs are precisely constructive partial possible worlds, representing
the de facto mathematical knowledge of a concrete individual or a machine.

It is perfectly conceivable that, for a specific notion of feasibility,
in some of the PFTMs associated to PA FLT is false (in  these worlds
there are no attainable proofs of FLT, and thus the mathematicians living
inside of them will conclude that it is not true).

I wish to point out that PFTMs are in a sense a "possible world semantics" for
FOL theories, but freed from "infinitistic" assumptions that still
underly Kripke's models.


Best to all

Mirco A. Mannucci





(*) people in complexity theory think that feasible = polytime, and
several  ultrafinitists assume that feasible = physically realizable.

Both interpretations make sense and are legitimate WITHIN a particular
framework, however they are by no means absolute.