1
$\begingroup$

Over on the nlab, I was looking at the page for fully formal ETCS and one clause stood out, namely the one for "well-pointedness", namely:

$$(s(f) = s(g) \wedge t(f) = t(g)) \vdash \forall_h (s(h) = 1 \wedge t(h) = s(f) \wedge f \circ h = g \circ h) \Rightarrow f = g$$

My question: what is the meta-logic which is used here? This is the first time where I see entailment so internalized in the logic that it can be used at the left hand side of a logical implication.

Edit: I was recently rereading this, and I finally spotted my error: I simply misread where the parentheses belonged! So there is no foundational issue here at all.

Improve this question
$\endgroup$
21
  • $\begingroup$ This “fully formal ETCS” is quite a mess, but from what I recall, they intend to formulate the theory in a sequent calculus and use $\vdash$ instead of a sequent arrow. That is, you should read it as a plain implication. $\endgroup$
    – Emil Jeřábek
    Commented Mar 19, 2012 at 17:38
  • 2
    $\begingroup$ I conjecture that Jacques merely guessed the "wrong" rule for associating the parts of the displayed formula. The main "connective" is intended to be the $\vdash$, and it has an implication ($\implies$) within its right side. Jacques seems to have assumed that the main connective is $\implies$, with $\vdash$ in its antecedent. $\endgroup$
    – Andreas Blass
    Commented Mar 19, 2012 at 19:11
  • 1
    $\begingroup$ @Emil: There's a reason for presenting in sequent form: if I remember correctly, a large fragment of ETCS is supposed to be an essentially algebraic theory, so the logical connective $\Rightarrow$ should be avoided in its axiomatisation. $\endgroup$
    – Zhen Lin
    Commented Mar 19, 2012 at 19:28
  • 1
    $\begingroup$ @Andreas:good point. @Emil: that web page is a wiki, I am sure the community would appreciate it if you improved the axioms. $\endgroup$
    – Jacques Carette
    Commented Mar 19, 2012 at 20:37
  • 2
    $\begingroup$ Emil, thanks for the feedback. A non-triviality axiom is left out on purpose, because it is the belief of many that the trivial topos is useful to consider on occasion, just as the trivial (= empty) set is useful to consider. In the past some mathematicians (such as R.L. Moore) refused to consider that there was an empty set, but that sort of prohibition is now considered a bit old-fashioned. I think I could respond to some of the other criticisms, but it might be more seemly to pursue that off-line. I have sent you an email... $\endgroup$
    – Todd Trimble
    Commented Mar 19, 2012 at 20:50

0

Reset to default

You must log in to answer this question.

Browse other questions tagged .