[FOM] f.o.m. documentary 2

[Michael Lee Finney]

First, I have to say that the very idea of the "cumulative heirarchy"
that is created in "stages" gripes my gut. As I see it, everything
is there all at once, we merely discover the structure within the
axioms. There is no "creating", no "stages", nothing to be "reached"
or anything like that. However, that is merely a philosophical
objection. It doesn't really change the actual structure of set theory.

Otherwise, if you have

   1. A quantified logic which allows incomplete and inconsistent
   statememts without triviality,

   2. Allows arbritary "order" in the logic,

   3. A foundation which is simple, clean and provides for the
   founding of both set theory and category theory in a natural
   manner,

   4. All of the above is just as easy to use, in the same manner, as
   the classical foundations (under classical conditions), allowing
   all of conventional mathematics with effectively no changes,

   5. In addition to containing ZFC (as theorems), the set theory
   allows naive comprehension, non-wellfounded sets, Russell's set
   and other inconsistent structures,

   6. Does NOT satisfy completeness, etc..

Would you consisder the above to be a reasonable replacement for the
current logical foundations? It would appear to me to be what was
needed, but unavailable when classical logic and the various
restricted set theories were formulated. Godel's work essentially says
that either our systems are intrisincally incomplete or there are
inconsistencies in the system. To me, that argues that allowing the
presence of inconsistency is absolutely necessary. Triviality under
those conditions merely shows that the logical foundations are
wanting.

Building such a structure is difficult, but I believe that it is
possible. There have been great strides made already. Just because
fundamental work in foundations is hard does not mean that it is
impossible, unneeded or should be ignored.

As far as incompleteness affects theorem provers, I see the use of
computers as more of an assistant. Perhaps an AI to convert the usual
informal proof to something more formal and a theorem verifier to
ensure that theorems are correct. While some of the technical
difficulties are eliminated for complete logics, and some interesting
theorems have been proven -- they have been around for a while and
haven't replaced mathematicans yet. I would like to see all of
mathematics mechanically verified, in fact, not just as "possible in
theory".

Difficulty in building automated tools is no reason to restrict the
foundations. Otherwise, we would all be speaking Esperanto to make
writing voice recognition software easier.


Michael Lee Finney


CM> Am Feb 18, 2012 um 8:15 PM schrieb Michael Lee Finney:
>> Perhaps the term "resolved" is not quite correct, but neither Cantor's
>> pardaox nor Russell's paradox can be properly handled within the
>> system [of ZF set theory]. The system has simply been made small 
>> enough that, hopefully, they do not occur.

CM> I think this misrepresents the situation rather badly. It is
CM> true that Zermelo himself considered his initial 1908
CM> axiomatization to be a pragmatic solution to the problem of the
CM> paradoxes. But the development of the iterative/cumulative
CM> conception of set culminating in Zermelo's own 1930 paper "Über
CM> Grenzzahlen und Mengenbereiche" yielded a clear and intuitive
CM> picture of the natural models of ZF that provided a compelling
CM> explanation of the paradoxes and a satisfying justification of the
CM> restriction of the Naive Comprehension schema found in the
CM> Separation schema: Sets are collections that are formed at some
CM> stage of the cumulative hierarchy; some conditions on sets
CM> (notably, the conditions "x ? x" and "x is a cardinal" that
CM> generate the Russell and (so-called) Cantor paradoxes) pick out
CM> objects of arbitrarily high rank which, therefore, never jointly
CM> form a set at any stage of the hierarchy.

>> Just as with a set of linear equations, a set of logical equations can
>> be underdetermined, overdetermined or fully determined. So, every set
>> of logical equations must be undetermined, inconsistent, false or true.
>> Since every logical object is described with a set of logical
>> equations, all four possibilies exist. So, if your foundations cannot
>> handle incomplete and inconsistent propositions you are unable to
>> discuss every logical object. So, objects such as Cantor's set cannot
>> be discussed within your system. Refusing to talk about it is not
>> resolving the problem.

CM> That is far from obvious to me. In ZF, you can (arguably)
CM> offer a very satisfying explanation for why certain conditions
CM> simply do not specify a logical object of the requisite sort. That
CM> seems to me to count as a pretty reasonable way to resolve the
CM> problem without having to acknowledge some sort of shadowy
CM> denotation for every conceivable term.

>> The foundations must be revised to resolve the
>> problem which means that the objects can be discussed formmaly 
>> and within the system without destroying the system.


CM> That they *can* be revised is of course an interesting and
CM> important project that a lot of people have been pursuing for
CM> quite some time.  That they *must* be is not quite so clear.

>> When you tell me that a logic is formally "complete" or has
>> "desirable" upward or downward properties, my response is that 
>> it is a "toy" and is incomplete for practical usage.

CM> Seems to me these properties, and stronger ones still,
CM> notably, decidability, are of immense practical importance for,
CM> notably, automated reasoning, where a great deal of research is
CM> still working within the framework of classical logic — notably,
CM> many description logics, which are so fundamental to recent work
CM> in the development of the semantic web. But maybe I don't know
CM> what sort of practical usage you have in mind.

CM> Chris Menzel

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