[FOM] Paraconsistent System

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

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

> P.S.  Incidentally, I do not believe that the paraconsistent logics I 
> mentioned above are enough to deal with feasibly consistent theories:

Yes, as I understand, people working on paraconsistent logics assume 
something of a quite different character than feasible consistency (no 
contradiction of feasible length).

> the reform needed is much deeper than merely changing  logical rules. 
> It must not reduce the logic, but on the contrary enrich the notion
> of proof, by adding to it a measure (or measures) of its credibility.

Whether it restricts logics or extends it depends perhaps on the point 
of view. Anyway, taking into account a measure of credibility means 
imposing a restriction on derivations. For example, the formalisation 
of feasibility I have suggested was, in fact, based on the measure of 
complexity of cut elimination (or, more properly speaking, elimination 
of abbreviations of terms). Say, for a predicate M (definable from F - 
the semiset of feasible numbers) which was shown to be (i) closed under 
successor but (ii) bounded by 1000, the derivations of M(O), 
M(1),...,M(1000) were possible with the cut rule, but only for some 
proper initial part of this sequence the cut rule was possible 
*practically* to eliminate (the harder and  harder,..., and eventually 
practically impossible even for numbers less much than 1000).

In Parikh's approach (JSL, 1971) to a weaker (longer) version of F the 
(unified) measure of complexity was just the length of proof. The same 
holds, as I understand, in the posting of Friedman. This can be treated 
that the underlying logic is not changed both by Parikh and Friedman, 
whereas in my case (to have the effects "resolving" the heap paradox as 
above) the cut rule (or the like) should be 
forbidden/restricted/eliminated. Thus, the measures required have here 
rather different proof theoretic character.

But I still prefer to think in terms of restricted (or unrestricted) 
logic with the measure preferrably just the number of symbols in the 
proof. (However, in my case with the restricted cut rule the measure is 
rather the maximum number of symbols in terms occurring in the proof).

> This is, by the way, the same kind of work needed (in my opinion)
> to give ultrafinitism a solid mathematical ground.

As to model theory of feasibility concept, F can be added in a way to, 
for example, ZFC extending it by semisets with F among them. Like 
postulating \omega adds all infinity power to ZFC, adding F \subset 
\omega should probably add a lot of semisets along with with F, the 
latter serving as a model for feasible numbers like \omega serves as 
the "standard" model for PA.

But the problem is not only in formulating and developing such a 
feasible semiset theory. By the way, this is not a very good term; is 
the ordinary \omega from the universe of such a theory based on ZFC 
also feasible? But the "proper" feasible set theory could also be 
developed. I am actually working now on a version of feasible set 
theory, more precisely, "polynomial" set theory (based on the ideas of 
Bounded Set Theory for HF whose provably recursive set theoretic 
operations = explicitly definable in the Delta language of BST = 
polynomial time computable).

Such a formalisation should be made so convenient and intuitive that we 
could make the derivations desirably as easy and semiformally as in the 
ordinary ZFC. It is, indeed, rather inconvenient to work in the logic 
with suitably restricted cut rule (or the like). A request on such a 
convenient, psichologically comfortable formalisation of feasibility 
theory allowing to think model-theoretically without paying much 
attention to the formalism and in particularly to the cut rule was 
stated in my paper On Feasible Numbers, 
http://www.csc.liv.ac.uk/~sazonov/papers/lcc.ps, page 21. Some tricky 
"more liberal" approach allowing to avoid in a sense the restriction on 
the cut rule is also presented in Section 5. There is also a 
possibility to formalise feasibility concept in a "relaxed" way with 
allowing cuts only by formulas with bounded quantifiers.


Vladimir Sazonov


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