Came across this recent philosophy of math book that appears

>>7854441
Do Lie-Groups REALLY exist?

File: Tretris.png (352KB, 1170x722px) Image search: [Google]

352KB, 1170x722px

>>7854514
I'll give you a Wittgensteinian shut up

shutup and calculate

>>7855040
That only works if you accepted your foundations or theory already

>>7854441
bumping while I read this, also this is a better thread than most of the shit on the front page right now.

File: 20140830_003.jpg (1MB, 3264x1840px) Image search: [Google]

1MB, 3264x1840px

>>7857014
What's your outlook on the subject?

I've read the beginning and the jumped the history part to the end of the second chapter (see >>7855038) but haven't looked at the end, where he discusses his proposal for the position of logic within the foundations.

If you follow all the business around Voevodsky and friends, their in part public fights about the emphasis of different topics of their collaboration is quite fun. He is essentially mad they wrote that typey book and went on doing more of his own stuff, and writing his own article
https://en.wikipedia.org/wiki/Univalent_foundations
and it reads like it.

>>7854514
No, they Lie.

File: 1376641570408.jpg (48KB, 319x325px) Image search: [Google]

48KB, 319x325px

>>7857168
HoTT/UF is love
HoTT/UF is life

File: Bildschirmfoto 2016-02-13 um 12.12.17.png (142KB, 697x665px) Image search: [Google]

142KB, 697x665px

>>7857168
ad: Mhm... looking at the history parts I skipped, they seem to give a good overview of the development of logic (and set and cats) since 1890.

>>7857187
There is a one week workshop about it at this very moment in Bonn.
If you read the abstract of Voevodsky morning series (pic related), you see his current attempts is to find a good model of it (univalence I guess) in ZFC.
Indeed, it would be very cool if set theories jumped on that wagon and investigate some features of that world within their own playground.

I'd like to have a dependently typed language with simple semantics ready to do some programming right now.
I'm thinking about outlining the syntax of such a language, actually, because I want to implement some physics in it (differential geometry).

If I understand the univalence axiom

[math] ua: (A=B) \to (A \cong B)[/math]

correctly, then it's indeed an important thing for math.
Personally I find the type theory (Martin-Löf) equality extremely tiresome, all the formal substitution rules that you just igonore or just do if you do normal math. Or path induction proofs - I don't know if this stuff can become second nature to any "normal person". The biggest problem with HoTT et al. that I see is that people "like me" don't care about proofs of known mathematical "truths".
Certified programming is cool, and automatic term generation is awesome, but the language must be effective to use.

>>7857194
>There is a one week workshop about it at this very moment in Bonn.
Nice, I didn't know that. There's also one in May at the Fields Insitute and one in Porto in June.
>you see his current attempts is to find a good model of it (univalence I guess) in ZFC.
I first read about this on /sci/ a few weeks back. IIRC, the intent is to create a model of HoTT in ZFC so that the wider mathematical community is more amenable to use and contribute to the programme.
>I'd like to have a dependently typed language with simple semantics ready to do some programming right now.
I've been following some type theory/PL people on Twitter and various mailing lists and there seems to be a lot happening in this area at the moment it seems. We have full-fledged languages like Coq, Agda and Idris, and there are also smaller, two/three-person projects building on MLTT, but also observational and computational theories.
I don't have the links on me right now, but I can hit you up later if you're interested.

>>7857168
>>7857194
I think we're opposites on this. I'm a math student but I'm far more interested in the type theory and proof theory side of things than I am with the math itself. I'm currently in a HoTT course as well and though I'm interested in the foundational aspect of the topic I've found I'm totally not interested in homotopy theory.

I'm pretty sure I'm going to switch over to computer science since their type theory/mathematical logic/proof theory stuff becomes more and more relentlessly formal and rigorous the further up you go while the opposite is true on the math side of things.

>>7857206
Lean is worth checking out as well.

https://leanprover.github.io/

File: Schuhe Matraze.jpg (537KB, 1536x1024px) Image search: [Google]

537KB, 1536x1024px

>>7857210
I'm not interested in homotopy theory porpper either (as in, what is the so and so group of S^7), but categories and sheaves are more native in that language and cool people speak about interesting subjects in terms of those.

The philosophical side is relevant to me too. E.g. I always like to point out that you if you use the standard model for the pair and natural numbers in a set theory like ZFC, namely

[math] (a,b) := \{\{a\}, \{a,b\}\} [/math]

and

[math] 0 := \{\} [/math]
[math] 1 := \{0\} [/math]
[math] 2 := \{0,1\} [/math]
[math] 3 := \{0,1,2\} [/math]
etc.

https://en.wikipedia.org/wiki/Ordered_pair#Kuratowski_definition
https://en.wikipedia.org/wiki/Ordinal_number#Von_Neumann_definition_of_ordinals

then your foundations prove

[math] 1 \in (0,7) [/math]

THANK YOU ZERMELO.

>>7857206
I am, plz post them.

I use Haskell rudimentary and if there comes along a statically typed language with [math]\Pi[/math] and [math]\Sigma[/math], I'd totally start taking informal notes in those terms too more, because then the step to make something computationally out of it would be so small. Cooler, as I said, if someone would write a super strong compiler that generates terms of such a type for you. That's where we should go. Haskell already does this sometimes, when some type has a unique term (e.g. some functor actions on arrows in C are fully determined just by specifying you want to consider a functor from C to D that maps objects in this and that way. The arrow maps are then sometimes unique and haskell ghc is clever enough to infer the code for you)

>>7857248

What's wrong with that?

>>7857248
>if someone would write a super strong compiler that generates terms of such a type for you
I'm not sure I understand. Do you have something like Wadler's "Theorems for free" in mind?

File: Bildschirmfoto 2016-02-13 um 13.48.37.png (124KB, 735x732px) Image search: [Google]

124KB, 735x732px

>>7857251
It's philsophically ugly, for one.

If that's not enough for you, if you were to enumerate theorems of your language, you'd produce such mathematically meaningless shizzle. This can't happen in typed or categorical foundations - that's why the latter are better. Set theory should just be a theory expressible in your world imho, not be at the core. Not material set theory at least.

>>7857259
Yes.
https://byorgey.wordpress.com/2010/03/03/deriving-pleasure-from-ghc-6-12-1/

>>7857248
There's many weird things in the way the basic data structures in set theory work. You define an n-tuple using ordered pairs. So you have (n-tuples on the left, ordered pairs on the right).

[math](1)=(\emptyset,1)[/math]
[math](1,2)=((\emptyset,1),2)[/math]
[math](1,2.3)=(((\emptyset,1),2),3)[/math]
[math](1,2.3,\ldots)=(\cdots(((\emptyset,1),2),3),\cdots)[/math]

Now note that functions are using ordered pairs as well.

That is [math]f\colon A\to B[/math] can be restated [math]f\subset A\times B[/math] together with a couple other properties (satisfying well defined-ness).

So consider a projection function from the infinite product of sets. An element in this function will look like

[math]((1,2.3,\ldots)=(\cdots(((\emptyset,1),2),3),\cdots),3)[/math]

Which is a very weird dubious construction in my opinion. No less weird than saying something like

[math]0.999\ldots 91[/math]

I don't particularly mind the issue you pointed out since it comes up in many other theories as well. For instance in lambda calculus your "numbers" are just special terms (read: functions) dubbed "church numerals" and you end up with all sorts of computations being "equal" to a number.

http://arxiv.org/find/math/1/au:+Rodin_A/0/1/0/all/0/1

>The standard Hilbert-style formal axiomatic method serves us as a
tool for studying a logical structure of mathematical theories but
not as a tool for presentation and logical justification of these
theories (as Hilbert and his followers wanted). The requirement
according to which a given theory T must be formalizable in
principle constitutes a very weak necessary (but not sufficient)
condition for saying that T well-standing. Notice that a
contradictory theory can be well formalizable.

just read his talks instead of the big books

>>7857276
>Tree as a data structure deriving a whole bunch of stuff.

Why not just use a Comonad?

>>7857280
http://philomatica.org/my-stuff/my-talks/

do you guys have faith in type theory ?

i find it really gross and pointless, since we are left with a forest of types and the job is just to see what types are constructed from what other types.

>>7857290
From the PL side of things it seems super sensible imo.

So yes.

>>7857194
do you know on what bas spitter works ?

>>7857282
Me again. I had only skimmed the article and had missed the point. The derive functionality has been around since as long as I've been using Haskell so I didn't even realize it was trying to show it off as a new feature.

>>7857276
I don't mean any offense but perhaps this was not the article you meant to link (or I am missing the point completely)?

also, let's recall that the german from nlab, following Lawere, is formalizing what he retains from Hegel

https://ncatlab.org/nlab/show/adjoint+modality

>>7857278
>For instance in lambda calculus your "numbers" are just special terms (read: functions) dubbed "church numerals" and you end up with all sorts of computations being "equal" to a number.
There are many ways to represent numbers (natural, integers, rational, algebraic reals and complex) in lambda calculi. For instance, in Calculus of Inductive Constructions, you would define an inductive data type like

Inductive nat := O | S (n : nat).

and work with that.

so, from i gather from here
http://philomatica.org/wp-content/uploads/2015/04/rodin.pdf

this is his claim
>In Mathematics the constructive approach is already proved
effective: the proof of 4-colors theorem is formalized through Coq
(based on MLTT, which is the logical base of HoTT). Given the
prominence of model-building in Physics there is a reasonable hope
that this method will also work more successfully in Physics.


>IF HoTT proves to be a full-fledged foundation of mathematics it
will also serve as a mathematical foundation for the mathematized
Physics. Then it will covert physical theories into constructive
axiomatic theories automatically. Unlike Set Theory the Homotopy
(Type) Theory has some natural physical interpretations. That
makes HoTT a strong candidate to the role of basic “constructor”
out of which one may build physical (interpreted) theories. Theories
built with HoTT are computable ) unless one adds to MLTT new
axioms such as Univalence, which may be indeed strongly motivated
by logical, geometric and perhaps also specific physical reasons.
so apparently, it is just another attempt to formalize discourses, up to physics

File: Bildschirmfoto 2016-02-13 um 14.17.43.png (91KB, 674x502px) Image search: [Google]

91KB, 674x502px

>>7857296
pic related, could have googled that yourself

>>7857278
>and you end up with all sorts of computations being "equal" to a number.
Yes, but what your primary notion of equality is really is and what it's not can be internalized (Martin Löf-type theory) and forced to be equal to the structual notion you deem relevant (univalence)! That's exactly what the fuzz is about

ua:(A=B)→(A≅B)

being required to be an equivalence (an ≅ one level up). Like in category theory where things defined by a universal property are equivalent.
So ≅, and in turn =, is, for every structure, only what you make it it to.

>>7857290
Given Curry Howard, to my ears, that's like asking if you I have faith in predicate logic.

If you ask some guy to write
>a function that maps a number to a list of it's prime factors,
e.g.

70 to (2,5,7)

then in C or Java you can start a scrip specifying in one line that the input is an integer,
"int"
in Haskell you can demand that the code is a function mapping an integer to some list of integers
"Int -> [Int]"
in Idris you can can already specify that the list can't possibly be longer than the number itself (70 can't have over 70 prime factors)
and in a neat future dependently typed language language you can specify that he writes
>a function that maps a number to a list of it's prime factors
and the compiler (type checker) will say fuck you if his code doesn't do what it should be. If your type theory is as strong as (higher) order logic, coding is just about coming up with one of the extensionally equivalent terms of that type that captures all non-meta (e.g. runtime) specifications (you come up with a proof)

>>7857282
It's more ad hoc and doable with less brain effort, I guess.
(I take your claim that three gives rise to a Comonad as a given, not that you make fun of me by putting up a trap here)
>>7857305
The article is also 6 years old now, but the derive tool is what I meant.

File: Bildschirmfoto 2016-02-13 um 14.29.45.png (144KB, 647x652px) Image search: [Google]

144KB, 647x652px

>>7857308
He was getting ideas out of Hegels science of logic last year (because Laywere did it some decades ago) and I was reading along on the nforum. My understanding of the point in pic related.

Urs did his PhD thesis on classical field theory in stacks (using the tools of algebgraic topology, i.e. sheaves on topological spaces, but not using sets but groupoids) and there the groupoids have things like gauge transformations between fields (e.g. electrical fields) natively build into them.
As the HoTT bandwagon is going on and everything becomes a synthetic theory within a type theory, he's looking at the axiomatization of those (higher) stacks in terms of adding some functors to HoTT.

For the first level:
The comonad-monad graph
FGa -> a -> GFa
is also what you find if 'a' is a space and FGa, GFa are the two trivial topologies (the thing itself is the only open set vs. every element of the set is open (discrete topology)).

This is sets -> topology, differential structure comes later, bosons and fermionic structure even later. And apparently he can force the axioms for those in terms of (co-)monads too.

>>7857210
>I think we're opposites on this.
Yes I guess the above is not exactly the theorem proving side of HoTT ^^

>>7857322
This is so cool

>>7857329
>and the compiler (type checker) will say fuck you if his code doesn't do what it should be. If your type theory is as strong as (higher) order logic, coding is just about coming up with one of the extensionally equivalent terms of that type that captures all non-meta (e.g. runtime) specifications (you come up with a proof)
This too