[FOM] Feasible consistency--Truth Transfer Policy

[Mirco Mannucci]

---- V.Sazonov at csc.liv.ac.uk wrote:


> I have doubts in such an approach which, as you want, does not restrict
> logic, but only introduces a credibility values *via TTP*.
>
> You know, the following is formally (in fact, feasibly) consistent:
>
> M(0), forall x (M(x) => M(x+1)) and not M(100).
>
> (A kind of solution of Heap Paradox.) Here M (meaning intuitively
> 'medium number') is a formally definable predicate in an appropriately
> formalised theory of feasible numbers in a suitably restricted logic.
> In fact closure under successor also means that it is impossible to
> show which exactly is the borderline x where M(x) & not M(x+1) holds.
> (There is some other unusual effect. The details, which are quite
> rigorous, are omitted.)
>
> Which should be TTP for Modus Ponens which would guarantee such a
> consistency in terms of credibility in the case of classical logic
> without restrictions?


Dear Vladimir,


Assume we are in a Hilbert system, so the only logical rules are modus ponens
and generalization/specialization. Also, for the sake of simplicity, assume for
the time being that the TTP for generalization/specialization is trivial
(no loss of credibility there).

As for modus ponens, there are infinitely many TTPs that would do the job, but
I shall stick (again, for making things as plain as possible) to the simplest one:

the decrease of credibility will be at a constant rate (this is what I call
constant credibility erosion)

if I have a proof of A of credibility p_A and I have a proof of A--> B of
credibility p_(A-->B), where p_A and P_(A--> B) are in [0  1],
then application of modus ponens will lead to a proof of B of credibility


   TTP(modus ponens) =   f: [0 1]^2 --> [0 1]

   where f =   max ( 0, min(  p_(A-->B), p_A ) - E)


    0< E < 1 is the "constant credibility erosion factor" and
   E =1/N with N is your "unfeasible middle number" (in your story, 100)


Now,  can we derive a contradiction from

M(0), forall x (M(x) => M(x+1)) and not M(100) ?


Easy (apparently):


M(0) ^ M(0) --> M(1)

M(1) ^ M(1) ---> M(2)


....

M(100)

M(100) ^ NOT M(100) : contradiction!

BUT:

according to the TTP above, there is a trivial proof of M(0) of
length 0 (it is an axiom !), so with credibility 1 (same applies
to forall x (M(x) => M(x+1)) )


proof of M(1) has credibility 1-1/100

proof of M(2) has credibility 1-2/100

...

proof of M(100) has credibility 1-100/100 = 0!!!



Notice that the infamous axiom of induction  is a free-lunch ticket:
if I add induction on M(), then of course I can get M(100) for cheap
(almost no credibility erosion, with the same TTP as above).

Here is the mantra:

      induction = free-lunch ticket in resource-aware proof theory


That is  why, unlike Nelson, Buss, and many others, I think one
ought to be wary of ANY type of induction (not just for exp).

I am NOT suggesting to banish it; I am just saying that there can be
examples of feasible arithmetics where even ADDITION is not
total (induction-free arithmetics).

Getting too many free lunches makes us unaware that there is a cost
behind EVERY lunch (PA is the Great FOM  Party's theory: free
lunch for ALL the formulae!!!!!).


---->  A friendly note "en passant" for Arnon Avron:

you think (erroneously, I believe) that any feasibility notion is inconsistent,
by allowing yourself the LUXURY to use induction at the META-LEVEL.
But, here is the rub: there is NO reason to treat meta-arithmetics any
different than arithmetics. This is a subtle and yet a big mistake,
frequently made when talking about  FOM, and expecially about N:

imagining that meta-mathematics is somehow "above" math.

----> End of the friendly note for AA.


> As I wrote in a previous posting, credibility values can be introduced,
> but in a different way (via complexity of cut elimination or, more
> properly speaking, complexity of elimination of abbreviations for
> terms) which does not seem to be definable in terms of TTP.
>

Dealing with your more sophisticated measures (number of symbols,
etc.) or Carbone's (number of cycles in the flow graph of a proof) is
admittedly harder. I make no bones about it.

However, I think my TTP can in principle handle ALL of them. I cannot
enter details here, but:

how do you increase number of symbols in a proof? A typical example
is creating "fresh witnessing terms" for existential statements:

  Exists x A(x)
--------------
   A(t)   (where t is new)


or similar steps. All right, those "expensive" steps can be assigned a TTP that measures
the one-step decrement of credibility each time I add a new symbol using the rule
above (or variants thereof). After all, proofs are finite objects, built from
basic steps: if I can keep track of the credibility's erosion at EACH building block,
I can gauge the overall credibility status of the whole proof.



Best wishes
MM




P.S. Actually, paraconsistent would be a good term. Unfortunately, it is already taken
by the paraconsistent logic community, as well as others (non-monotonics, etc.).
So I agree with you: let us call this topic feasible consistency and let us hope that
others in this list (aside you and I) will find it to their taste.

P.S.1 The Tennenbaum preprint that I said would be ready by the end of
September will be available on the Los Alamos  archives by November 15th
(some other personal and professional priorities "dampened" it). The last
two sections will contains some more details on TTP and why I need this
notion in the first place.