[FOM] Examples of paraconsistent systems

[Joe Shipman]

To clarify: I don’t just want an uninterpreted formal system in which every well-formed formula is derivable but the shortest derivation of some short formulas is infeasible. 

(I could construct one of them myself using the Goodstein game, where the legal operations on a pair consisting of a positive integer “base” and a sequence of smaller integers are either to regard the sequence as a number in that base and subtract 1, or to increment the base, and a sequence of zeroes is regarded as an inconsistency because there is another rule that from it you can derive anything. This exhibits Ackermannic growth in the size of the derivation of a sequence of zeroes.)

Rather, I want it also to have a semantics that allows easily proved statements to be seen as “true”, and also has some feasible size statements which can be seen to be false under this semantics but for which the only known proofs within the system are infeasible in size.

— JS

Sent from my iPhone

> On Jan 29, 2019, at 1:17 AM, Joe Shipman <joeshipman at aol.com> wrote:
> 
> Can anyone provide an example of a formal system for some part of mathematics which is known to be inconsistent but not known to have a feasibly derivable inconsistency? (In other words, it is “known” to be inconsistent according to a proof relying on some other formal system which can formulate the proposition of its consistency, but also has a clear enough semantics that there is *some* statement it can express which is obviously false.)
> 
> — JS
> 
> Sent from my iPhone