[FOM] Paraconsistent System

[Mirco Mannucci]

---- Harvey Friedman <friedman at math.ohio-state.edu> wrote:

> Is this within what people have in mind when they use the term
> paraconsistency?
>

Depends whom you ask. Generally people use the term paraconsistency in reference to paraconsistent logics, a kind of substructural
group of logics where "ex falso sequitur quodlibet" is ( directly or indirectly ) banished (thus allowing for some form of  "non-propagating"
inconsistency).

On the other hand, yours looks more like a result further along the lines of Parikh [1971], which Vladimir Sazonov has  quoted a
number of times on this list, in connection with feasibility (it was the first result proving that ultrafinitism is not just wishful thinking).

I believe your "paraconsistent" system is extremely interesting from the FOM perspective, as it shows  that Parikh's "feasibly consistent
theories" could be much more widespread than his original example (and intended usage) would have perhaps suggested.

To me, it tells clearly that is about time to revise BOTH proof theory and model theory, in order  to allow full logical citizenship for these wild
creatures.


> Although the above system is inconsistent, it behaves entirely "normallly"
> when we look only at proofs of any reasonable size.


That is exactly the main point: a "feasibly consistent theory" appears just like a consistent theory, away from its "singularity" (it is a bit like a smooth
manifold with an isolated singularity; it looks perfectly  regular when one is far from it). Thus, as they are perfectly nice and tame animals
most of the time, people should be able to use them.

I am suggesting that THESE THEORIES SHOULD HAVE A MODEL, i.e. a class of structures for their  interpretation.

Of course, they cannot have a model in the Tarskian sense, as they are classically inconsistent. I say, too bad for Tarski:
I envision an emendation of his notion of satisfiability that will allow for genuine  models of feasibly consistent theories.

To this effect, one must reform proof theory FIRST, accounting for the PROGRESSIVE DECAY of credibility of a proof, as its length or
computational complexity increases. What I am saying is that a feasibly consistent theory (like yours) should be a
theory such that any proof of its inconsistency would have a level of credibility below a certain threshold.
After syntax, is the turn of semantics. The goal?

A completeness theorem for feasibly consistent theories in first-order logic.

Mirco Mannucci

P.S.  Incidentally, I do not believe that the paraconsistent logics I mentioned above are enough to deal with feasibly consistent theories:
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. This is, by the way, the same kind of work needed (in my opinion)
to give ultrafinitism a solid mathematical ground.