Timeline for Entailment and implication
Current License: CC BY-SA 3.0
23 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Nov 20, 2012 at 8:24 | comment | added | Toby Bartels | I agree with Emil; nontriviality should be part of the definition of ETCS. It goes along with well-pointedness. It is true, of course, that "there is no rational square root of two" is true in the internal logic of the trivial topos, but if we were interested in founding mathematics on what can be proved in the internal logic of every suitable topos, then we wouldn't have well-pointedness either. The point of being well-pointed is to make the internal logic line up with the external logic, and this requires nontriviality too. | |
| Nov 3, 2012 at 3:25 | comment | added | Andrej Bauer | @Emil: the usual proof of "there is no $x \in \mathbb{Q}$ such that $x^2 = 2$" reduces to "$0 \neq 1$". In a setting where non-triviality is not assumed this is as far as we can go. I agree that it would be a bit more practical to be able to conclude that in fact $0 \neq 1$. | |
| Nov 2, 2012 at 22:19 | comment | added | Sridhar Ramesh | It's also worth noting that the trivial topos, like all toposes, internally considers itself to be non-trivial. It just happens to also consider itself to be trivial... | |
| Nov 2, 2012 at 22:17 | comment | added | Sridhar Ramesh | In the internal logic of the trivial topos, "there is no rational square root of two" is true. It's just that "there is a rational square root of two" is also true. The internal logic of the trivial topos happens to validate all statements; that's what makes it so trivial. But it also means it doesn't harm anything, or make any difference to the model-theoretically valid statements, to consider it a legitimate model. | |
| Nov 2, 2012 at 20:09 | comment | added | Emil Jeřábek | That is, I am not worried about insecurity of the system, but on the contrary, that it is too weak for the stated purpose. | |
| Nov 2, 2012 at 20:07 | comment | added | Emil Jeřábek | @Andrej: Restricting attention to a particular model is putting the whole axiomatic method on its head. The goal of axiomatic foundations of mathematics is to have one theory with uncontroversial axioms which is capable of proving all results from general mathematics after appropriate formalization. It is impossible to prove common theorems like “there is no $x\in\mathbb Q$ such that $x^2=2$” in a theory which is consistent with everything being equal to everything else. | |
| Nov 2, 2012 at 18:45 | comment | added | Andrej Bauer | When I said "it is impossible to speak about global points indside a topos" I meant "the internal language of a topos cannot make statements about global points". | |
| Nov 2, 2012 at 18:45 | comment | added | Andrej Bauer | @Todd: I don't see how to make a discussion on nLab so I will post this here. Under the usual interpretation of the internal language of a topos, every topos satisfies the well-pointedness axiom. It is impossible to speak about global points inside a topos, because morphisms are not part of the language, only the internal exponentials are. Where can I discuss this issue on nLab? | |
| Nov 2, 2012 at 18:34 | comment | added | Andrej Bauer | @Emil: what is better about requiring non-triviality, from a foundational point of view? By positing $0 \neq 1$ in the formal theory we have gain no additional "security" as far as foundations are concerned. If you want security you should look for a non-trivial model, not for an axiom which claims that there is one. | |
| Nov 2, 2012 at 18:26 | history | edited | Jacques Carette | CC BY-SA 3.0 |
add info
|
| Mar 22, 2012 at 17:34 | comment | added | Todd Trimble | Emil, the main purpose of the page was to give a formal presentation of ETCS, not (primarily) to discuss foundations of mathematics, which would be a whole other discussion. Note that ETCS can be studied with or without regard to FOM. If one is interested in the FOM aspects, then obviously one is interested in nontrivial models (assuming they exist of course -- if an inconsistency is found in Bounded Zermelo set theory with choice, it would mean that the only model of ETCS is the trivial model). It seems to me that here you're fussing about a pretty obvious point. | |
| Mar 21, 2012 at 16:27 | comment | added | Emil Jeřábek | @Todd: I will (hopefully) reply to your email later, but for now I’d comment here on the nontriviality issue. I wholeheartedly agree that definitions should not exclude trivial cases without a solid reason, and I am happy with the trivial topos being a topos. However, the trivial topos cannot be allowed as a model of a theory which aims to be the foundation of mathematics. The point of FOM is to have an axiomatic system into which one can (by means of natural definitions) embed the bulk of mathematics. It is impossible to simulate the bulk of mathematics inside the trivial topos. | |
| Mar 19, 2012 at 20:54 | comment | added | Todd Trimble | Jacques, that's right, it's a wiki. We try to be respectful of each other's efforts at the nLab; the best public place to discuss nLab entries is the nForum nforum.mathforge.org/discussions/?CategoryID=0, and I am also happy to discuss this Emil there, as well as offline. I appreciate anyone bringing substantive errors to light, of course. | |
| Mar 19, 2012 at 20:50 | comment | added | Todd Trimble | 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... | |
| Mar 19, 2012 at 20:37 | comment | added | Jacques Carette | @Andreas:good point. @Emil: that web page is a wiki, I am sure the community would appreciate it if you improved the axioms. | |
| Mar 19, 2012 at 19:28 | comment | added | Zhen Lin | @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. | |
| Mar 19, 2012 at 19:11 | comment | added | Andreas Blass | 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. | |
| Mar 19, 2012 at 18:58 | comment | added | Emil Jeřábek | ... and to various mistakes: for example, there are a whole bunch of useless axioms defining the predicate $p(f,g,h,k)$ (a pull-back square), but the only important axiom about pull-backs (namely, that they exist) is missing! Another missing axiom is some nontriviality condition, as the theory has a one-element model. I originally came to the page to learn how this categorical-foundations-as-a-formal-theory can work, but I found this presentation impossible to grasp, so I had to figure out a decent axiomatization of the theory myself. Surprizingly, it boils down to ~10 fairly intuitive axioms. | |
| Mar 19, 2012 at 18:49 | comment | added | Emil Jeřábek | Where do I start? I already mentioned that it is presented in a confusing way as a sequent calculus instead of a list of axioms. The language of the theory is chosen in an unsystematic haphazard way: all concepts of the theory are definable from the composition predicate, nevertheless the signature includes a random selection of various defined concepts appearing in the axioms. These concepts are not presented with simple defining axioms, but a list of properties (which would be equivalent to the defining axiom, were it not for errors). This leads to an explosion of the number of axioms, ... | |
| Mar 19, 2012 at 18:12 | comment | added | Todd Trimble | "This fully formal ETCS is quite a mess" -- would you care to amplify, Emil? | |
| Mar 19, 2012 at 17:40 | comment | added | Emil Jeřábek | And you should also read the last conjunction as implication. | |
| Mar 19, 2012 at 17:38 | comment | added | Emil Jeřábek | 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. | |
| Mar 19, 2012 at 17:06 | history | asked | Jacques Carette | CC BY-SA 3.0 |