[FOM] Feasible consistency--Truth Transfer Policy

[V.Sazonov@csc.liv.ac.uk]

Quoting Mirco Mannucci <mmannucc at cs.gmu.edu> Sun, 29 Oct 2006:

Dear Mirco,

Feasible consistency means that the derivation of the contradiction is 
impossible if it has feasible number of symbols. (I would call this 
also the naive or even genuine understanding of formal consistency.) It 
could have some other versions, for example, that any derivation with 
feasible number of symbols in each participating term does not lead to 
a contradiction, or the like. When we discussed some measures like 
complexity of cut elimination or elimination of term abbreviations, I 
understood that this was about whether this measure will be of feasible 
value, just in correspondence with the above simple idea of feasible 
consistency.

Now you suggest rather a measure which is a real number between 0 and 1 
and that some Truth Transfer Principle (TTP) would "govern" this 
measure. This seems to me going far from the very idea of feasible 
consistency. Your examples of using such a TTP are non-convincing to 
me. The first example with the TTP for modus ponens based on taking max 
( 0, min(  p_(A-->B), p_A ) - E) for E=1/100 seems to me just ad hoc. 
Note that the predicate M which I suggested to consider as satisfying

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

was not a primitive one (for any interested reader, it makes sense to 
look at http://cs.nyu.edu/pipermail/fom/2006-February/009746.html for 
the precise definitions). The point was that the trivial proofs of 
M(0), M(1), M(2),..., M(100) by using modus ponens are, in fact too 
complex in the sense of the measure mentioned above (of complexity of 
eliminations of abbreviations of terms), just *impossible*, for 
sufficiently large numbers even smaller than 100.

The problem with your TTP in this case is that it is not related with 
the proof-theoretical measure I am considering. It is, in fact, related 
with my example only very superficially. You simply consider a quite 
different example and idea which I cannot relate with the idea of 
feasible consistency as I understand it. In your case p_M(100) = 0, 
whereas in my case the complexity measure of proving M(100) is 
"feasible infinity", and this is not so adequate in this context to 
consider 0 as 1/"feasible infinity". Say, in your example p_M(99) = 
1/100 is quite different from 0 (this is quite far from to be 
considered as an "infinitesimal") whereas in my case M(99), M(98), etc 
are still "feasibly non-provable". The point is that neither the above 
form of your TTP nor some other its version you hinted at in your 
posting has anything general with (and cannot imitate) the 
proof-theoretic measure I consider. If you have a proof of the length 
like 100 above and apply any version of TTP to each derivation step, 
you will need to accumulate in some way the "credibility values" for 
about 100 times by some, basically, "uniform" and locally applied TTP. 
I do not see how anything like cut elimination can be grasped by such a 
procedure. What you suggest is just a quite different story. It is more 
alike to fuzzy logic theory (dealing with measures like you suggest in 
a local style) than to the idea of feasible consistency or may be posed 
somewhere in between of these two ideas but more close to fuzzy logic. 
As I remember, fuzzy logic deals with a special real number valued 
interpretation in [0,1] of logical operators whereas you suggest doing 
something similar with proof rules. This might be interesting, but, I 
repeat, this is rather not about feasible consistency - even in the 
case if nothing like cut elimination is assumed as a measure of 
(non)feasibility (i.e. just feasible length of proofs is required). Of 
course, you could suggest to consider also natural numbers as the 
measures of complexity instead of [0,1], but I still do not see how TTP 
(applied locally)would imitate the complexity of cut elimination what 
is essential for the effects like in the above example with M and 100 
and for formalising the "true" feasibility.

I repeat, what you suggest is rather a renewed version of fuzzy logic 
with the accent on proof rules instead (or alongside with??) that on 
logical operators. Just quite a different story in comparison with the 
approach via feasible consistency. Any analogy seems to me superficial.


Best wishes,

Vladimir Sazonov


----------------------------------------------------------------
This message was sent using IMP, the Internet Messaging Program.