4 ms·

Synthetic differential geometry formalizes calculus in a way that precludes most monsters. Quite nicely, it allows you to use infinitesimal reasoning. The price

Synthetic differential geometry formalizes calculus in a way that precludes most monsters. Quite nicely, it allows you to use infinitesimal reasoning. The price to pay is the law of excluded middle. If you're a programmer, you're probably fine giving that up. The wiki page has good references: https://en.m.wikipedia.org/wiki/Synthetic_differential_geometry https://en.m.wikipedia.org/wiki/Synthetic_differential_geome...

xelxebar 9y ago
Oh. I'm happy someone brought this up! For anyone interested, Anders Kock has a nice slim-but-dense book on the subject entitled "Synthetic Differential Geometry" [0]. Kock even offers a PDF of an older version [1] on his site. [0] http://a.co/717X9pE http://a.co/717X9pE [1] http://home.imf.au.dk/kock/sdg99.pdf http://home.imf.au.dk/kock/sdg99.pdf
adrianratnapala 9y ago
Only if you are that exceedingly queer kind of programmer who thinks that which is not within reach of Coq can never be truth. I am a programmer, but I like C better, and assert(A && !A) looks like a monster to me.
- irishsultan 9y ago
  Well, you probably meant assert(A || !A), but even so that will of course never be an issue if A is a value, it becomes only a problem if A is replaced by something like a() (which I assume to be a pure function for the purpose of this comment). Of course a() || !a() is never going to be false either, so assert(a() || !a()) will never abort your program, but that doesn't mean a() || !a() will ever be true (if a() never finishes calculating then neither will a() || !a()).
- danharaj 9y ago
  (A && !A) is always false even if (A || !A) isn't justified . In other words, !!(A || !A). When we reject excluded middle we are no longer talking about truth, but evidence.
maxiepoo 9y ago
Yeah this kind of nullifies the pull quote > If Newton had known about such functions, he would have never created calculus. since Newton did use infinitesimals in his reasoning.
mcguire 9y ago
"The first is that most of the analytic data for describing the class of smooth manifolds can be encoded into certain fibre bundles on manifolds: namely bundles of jets (see also jet bundle)." Oh, mathematics, you are crazy.
- danharaj 9y ago
  This is a technically precise, compact way of saying "most of what we care about of smooth manifolds is how differential equations on them behave locally and how that local information can be glued together".

xelxebar 9y ago

Oh. I'm happy someone brought this up! For anyone interested, Anders Kock has a nice slim-but-dense book on the subject entitled "Synthetic Differential Geometry" [0]. Kock even offers a PDF of an older version [1] on his site. [0] http://a.co/717X9pE http://a.co/717X9pE [1] http://home.imf.au.dk/kock/sdg99.pdf http://home.imf.au.dk/kock/sdg99.pdf

adrianratnapala 9y ago

Only if you are that exceedingly queer kind of programmer who thinks that which is not within reach of Coq can never be truth. I am a programmer, but I like C better, and assert(A && !A) looks like a monster to me.

irishsultan 9y ago
Well, you probably meant assert(A || !A), but even so that will of course never be an issue if A is a value, it becomes only a problem if A is replaced by something like a() (which I assume to be a pure function for the purpose of this comment). Of course a() || !a() is never going to be false either, so assert(a() || !a()) will never abort your program, but that doesn't mean a() || !a() will ever be true (if a() never finishes calculating then neither will a() || !a()).
danharaj 9y ago
(A && !A) is always false even if (A || !A) isn't justified . In other words, !!(A || !A). When we reject excluded middle we are no longer talking about truth, but evidence.

maxiepoo 9y ago

Yeah this kind of nullifies the pull quote > If Newton had known about such functions, he would have never created calculus. since Newton did use infinitesimals in his reasoning.

mcguire 9y ago

"The first is that most of the analytic data for describing the class of smooth manifolds can be encoded into certain fibre bundles on manifolds: namely bundles of jets (see also jet bundle)." Oh, mathematics, you are crazy.

danharaj 9y ago
This is a technically precise, compact way of saying "most of what we care about of smooth manifolds is how differential equations on them behave locally and how that local information can be glued together".