# [FOM] Paraconsistent System

V.Sazonov@csc.liv.ac.uk V.Sazonov at csc.liv.ac.uk
Sun Oct 22 16:22:24 EDT 2006

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

> 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
\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.