No subject

[Vaughan Pratt]

From: Soren Riis <sriis at fields.utoronto.ca>
>The lack of ontological commitment and relativism helps making 
>Category theory more general than set theory - in a similar
>sense as predicate logic is more general than set theory. 

I see the picture as more balanced than this.  Category theory has its
own commitments, e.g. structure.  The closer set theory gets to home,
the more it neglects structure.  In particular posets are customarily
transformed by order-preserving (i.e. monotone) functions whether you
are a set theorist or a category theorist, but when have you ever seen
sets of sets transformed by membership-preserving homomorphisms?

Category theory is also much more committed to adjunctions and closed
structure than set theory, which barely gives them the time of day.

You may see these commitments as qualitatively different from the
commitments of set theory, and you'd be right to the extent that category
theory itself is qualitatively different from set theory.  They're
certainly disturbingly different viewpoints.

I find the commitments of both set theory and category theory sometimes
beneficial and sometimes a hindrance.  This variability results in
my preferring set theoretic foundations for some situations, category
theoretic for others, and more often than not a suitable blend of the two.

>Topos theory cannot serve as fom (like predicate logic 
>cannot). Its virtue (its generality) leave most foundational 
>questions to the "user". This is completely unacceptable from a 
>fom perspective. 

Strongly disagree, for the above reasons.  I'll get to your
singleton-topos concern at the end.

------

>John Mayberry wrote:
>
>>"a proof is a valid argument to establish that its conclusion is a true 
>>proposition. If there is no such thing as truth, then there is no such 
>>thing as proof".
>
>To which we got the following post-modern reply from Vaughan Pratt:

It's tough being a post-modern, Cantor took it particularly badly. :)

>To which we got the following post-modern reply from Vaughan Pratt:
>>"Your premise seems to be that every axiom of every proof system is
>>absolutely true.  For if not you would have proofs of theorems with no
>>basis for inferring that the proved theorems were absolutely true".
>
>For John Mayberry a valid argument is MUCH more than a logical valid
>argument. It has to be in agreement with reality. We do not make up
>the facts of mathematics. John Mayberry believes Wiles proved FLT.

You seem to have mixed us up.  What John Mayberry said (5 Feb 9:47 am) was

>If you prove that A follows from the axioms B,C,...,D, then you prove,
>not that A is true, but that if B,C,...,D are true then A is true.

I disagreed with Mayberry on this, saying (5 Feb 7:56 pm)

>what has been formally proved is A, not the hypothetical statement
>"B&C&...&D -> A"

But then you say

>If it (against expectations) should turn out that Wiles proof contain
>an argument which cannot be formalised in ZFC, Wiles proof would be in
>serious trouble - not ZFC.

I.e. Wiles (had better have) proved "ZFC -> FLT", which seems to put you
on Mayberry's side.  But that was the side you were on to begin with so
perhaps the above mixup was only in what you wrote and not what you meant.

-----

>Simpsons challenge was to provide axioms for a Topos which does not
>leave any judgments to the user. If there is a one element topos
>satisfying the axioms, its not the user who have to tell the
>program there is more than one real number.  The challenge was
>to present a system where the user just have to press to button.

Ah, I see why you're having trouble with the singleton topos, you're
identifying its objects with elements of its objects.  This off-by-one
error in type makes all the difference.

Working in the singleton topos does not mean your universe has only one
element, it means that you are not drawing the customary distinctions.
The result is not to lose theorems as you seem to be assuming but to gain
them: the singleton topos is inconsistent, not theorem-free.  What saves
topos theory itself from inconsistency is that, while it does not forbid
the singleton topos, it does not insist on it.

Ruling out the singleton topos should be like adding an axiom to ZFC
asserting its consistency (but don't push me on that analogy because
I'm not sure how far it goes).

Vaughan Pratt