[FOM] Inconsistent Systems

[Alan Weir]

Regarding Harvey Friedman's sketch of the triviality of a form of naive set theory- FOM Digest, Vol 129, Issue 17- it is well known that Curry's paradox trivialises naive set theory even in quite weak relevant logics without any appeal to the logic of negation. Those who seek to maintain that naive set theory is nonetheless still consistent or (this is the more usual line) at least non-trivial, often see the culprit as that principle of contraction which in rule form (sequent form) natural deduction goes:

>From X : A -> (A -> B) conclude

X : A -> B

This would block the usual way to derive Prof. Friedman's Lemma 1 (below). Even if we get (as we surely should)

(1) A in A <-> (A in A -> Alpha) so

(2) A in A -> (A in A -> Alpha)

we don't get A in A -> Alpha in a contraction-free system. 

Various ways of ensuring that the contraction rule is not a derived rule of the system whilst, ideally, retaining a full complement of classical "operational" rules have been developed. (I scare-quote "operational" because the structural/operational distinction is not clear-cut, is architecture dependent.)  For example dropping the contraction principle in sequent architectures in which sequents are not pairs of sets of wffs X:Y (or X:A for single conclusion) but sequences of wffs, and so dropping:

>From X,A,A,Y: B conclude X,A,Y:B. 

However it is not  a simple matter to ensure that a contraction-like derived rule (and thereby triviality via Curry) will not surface in the system, even if not for the operator ->, as Greg Restall has shown (‘How to be Really Contraction-Free’ Studia Logica 52, pp. 381-391.) More recently Curry-style trivialisation via validity or entailment predicates in the object-language has been investigated.

A more radical move, at least on the face of it, is to restrict in some limited way transitivity of entailment (Geach, Smiley, Tennant, Weir, Zardini, Ripley and others have investigated non-transitive entailment.)

Of course producing a non-classical framework in which naive set theory is consistent (or at least non-trivial) is one thing, and certainly can be done. Producing a framework which is not so restricted that it cripples standard mathematics is another, much more challenging, thing.

(I note also that Prof. Friedman's system CA(no) might perhaps be more naturally called a theory of naive properties, since there is no extensionality axiom. Hartry Field has given a consistency proof for such a system in quite a strong non-classical logic.) 

Alan Weir
Roinn na Feallsanachd/Philosophy
Sgoil nan Daonnachdan/School of Humanities
Oilthigh Ghlaschu/University of Glasgow
GLASGOW G12 8QQ
SCOTLAND

Message: 2
Date: Thu, 12 Sep 2013 08:57:26 -0400
From: Harvey Friedman <hmflogic at gmail.com>
To: Foundations of Mathematics <fom at cs.nyu.edu>
Subject: [FOM] Inconsistent Systems
Message-ID:
        <CACWi-GUdJg0yXvyxAkT6b28ARZKdq-c74N_=nj-a_12XegNsug at mail.gmail.com>
Content-Type: text/plain; charset="iso-8859-1"

I have never seen a cogent case made for the interest of inconsistent
systems for foundations of mathematics. Yet I still think that there is
much more to be said against them, and something new and interesting will
likely emerge in arguing against them.

I am new to this topic, so I will start with exploratory stuff, and expect
experts to further the discussion. At some point, if new results emerge,
then I will move them to my numbered postings.

Perhaps the most historically important inconsistent system developed for
f.o.m. is the full comprehension axiom scheme, which I will take in its
form with epsilon only (no equality), absurdity, and the connectives and,
or, if then, iff.

With the usual axioms and rules of classical logic, not only do we get a
contradiction, but we also derive all formulas. This is also true if we use
the axioms and rules of intuitionistic logic.

However, we can weaken the logic to avoid the rule that from absurdity we
can derive everything. Then it is not clear that CA = full comprehension
axiom scheme derives all formulas.

What axioms and rules of classical logic are appropriate here to use with
CA so that we don't derive all formulas?

To address this question, it seems best to first remove absurdity entirely
from CA and understand what is going on. CA without any absurdity will be
denoted by CA(no). We will use the usual classical introduction and
elimination rules for and, or, if then, and construe iff as an
abbreviation.

Let alpha be the sentence (forall x,y)(x in y).

We argue in CA(no). Let A = {x: x in x implies alpha).

LEMMA 1. CA(no) proves: A in A implies alpha.

LEMMA 2. CA(no) proves: A in A.

LEMMA 3. CA(no) proves: alpha.

LEMMA 4. CA(no) proves every formula in the language of CA(no).

I leave it to the experts whether this is convincing, whether this is new,
and what implications it has for various foundational and philosophical
enterprises? And what are the next things to look at?

Harvey Friedman
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20130912/63cfc5ef/attachment-0001.html>

------------------------------

_______________________________________________
FOM mailing list
FOM at cs.nyu.edu
http://www.cs.nyu.edu/mailman/listinfo/fom


End of FOM Digest, Vol 129, Issue 17
************************************