[FOM] Feasible consistency--Truth Transfer Policy
V.Sazonov@csc.liv.ac.uk
V.Sazonov at csc.liv.ac.uk
Sat Nov 4 08:31:02 EST 2006
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.
More information about the FOM
mailing list