[FOM] Paraconsistent System

Harvey Friedman friedman at math.ohio-state.edu
Sat Oct 21 05:05:59 EDT 2006

On 10/20/06 3:27 PM, "Erik Douglas" <erik at temporality.org> wrote:

> I do not have a paraconsistent rabbit in my hat at the moment,

Consider my Exotic Case statement E in Boolean relation theory. If we fix
the dimension in E to be rather low, we get a special case, say E[6]. This
statement can be proved by exhaustion in ZFC, as it becomes Sigma-0-1.  So
the system 

ZFC + not(E[6])

is inconsistent. However, we should be able to prove that the least size of
an inconsistency is unspeakably enormous - even far more enormous than
anything obtained by playing around with sequences of finite trees and
graphs as I reported on the FOM some months ago.

The inconsistency of this system is rather elusive. E.g., any proof in ZFC
that it is inconsistent must use an unspeakably enormous number of symbols.

If you want an understandable or physically realizable proof that it is
inconsistent, you need to use large cardinals.

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

Although the above system is inconsistent, it behaves entirely "normallly"
when we look only at proofs of any reasonable size. This is in sharp
contrast to what happens when we take, say,

ZFC + not(A) 

for some theorem A of ZFC that has a reasonably short proof in ZFC.

EXPECTED THEOREM. Suppose ZFC + not(E[6]) proves a Sigma-0-1 sentence with a
reasonable sized proof. Then ZFC proves it also with a reasonable sized

Harvey Friedman  

More information about the FOM mailing list