/sci/ - Science & Math

[Anonymous No.5411832]

How far have we taken math from first principles? Is Principia Mathematica the only major undertaking? Wikipedia says it never made it to analysis.

[Anonymous No.5411861]

two value logic is essentially dead after godel's incompleteness theorems

[Anonymous No.5411877]

>>5411861
> tfw first order logic is friendzoned

[Anonymous No.5411883]

whatever's on your arm looks like it hurt

[Anonymous No.5411902]

>>5411877
yes first order logic included

[Anonymous No.5412053]

anti-/x/ anti-/b/ anti-/a/ pro-/sci/ bump

[Anonymous No.5412070]

I don't understand what the big deal is. Math is nothing but a bunch of rules that we created because they were useful. We could create any of an infinite number of rules and see what interesting things logically come out from those axioms, but we don't. We only use the ones that are useful, and that is what defines mathematics.

[Anonymous No.5412107]

>>5412070
Matheticians use the rules they consider interesting, however useful they may be. It turns out some of the weirdest are surprinsingly useful, but it is not what mathematicians were seeking for in the first place.

[Anonymous No.5412112]

>>5412070
>>5412070
These rules are not arbitrary, they reflect reality, if you fail to see this then you don't understand mathematics.

[Anonymous No.5412113]

Principia Mathematica is pretty dated; I don't think anyone uses it as a foundation for mathematics anymore.

Bourbaki takes mathematics from first principles, and they're very rigorous about it. They do include algebra, topology, and analysis. However, the Bourbaki approach isn't truly modern in some ways — in particular, it doesn't cover category theory, which is now a conceptual framework of central importance in much of mathematics. For this and other reasons, the Bourbaki program has diminished in influence in recent decades.

There are plenty of formalizations of mathematics from a more modern standpoint. It's now common to use category theory as an alternate foundation for mathematics, for instance.

Anyway, the foundations are well-studied and formalized enough that there doesn't seem to be much of an issue of rigor at this point. So, in a sense, almost all of mathematics has been taken from first principles, since each field has its own works that formalize things given the foundations.

Computer verification is an additional degree of rigor and formality, and that's being carried out for many theorems, but certainly doesn't cover many things yet.

[Anonymous No.5412121]

>>5412112
Of course they reflect reality. If they didn't then they wouldn't be useful. If we lived in a very different universe with different physical laws then we would call some other list of rules mathematics.

[Anonymous No.5412127]

>>5412070
Im pretty sure maths is the universal language, understood by any intelligent species.

The basic concepts of mathematics apply to all parts of the known universe and these concepts can be extracted and understood by anyone at any time, they dont change (as far as we know). Maths is used to describe and explore the relationships between everything. So we didnt really make it up, we just found it and use it in our own way.

Maths could literally be used to communicate with an intelligent alien, it would just be a case of explaining that we use base 10 or binary or whatever. If someone could post that lifehack on what to do if you make first contact that would be nice.

[Anonymous No.5412142]

>>5412112
No. Modern axiomatcs have freed us to the need of setting rules that refer to experience. Mathematicians choose rules as they please, only in using those rules to reflect some disposition of their faculties do they connect in some way to reality.

This is speaking in the broadest sense. Of course MOST mathematicians use the usual axiomatic, which was built as an attempt to formalize our empirical understanding of the world. But still, that doesn't address the very deep problem of what is reality in mathematics. That's why your statement, though rather sensible in its intent, seems a bit bold to me.

Also, and to paraphrase Von Neumann, "you never actually understand mathematics". So, fuck yeah, I don't understand mathematics.

[Anonymous No.5412155]

>>5412127
You're making assumptions about things nobody know much of. Mathematics in general don't "apply" to the known universe, as applying mathematics to the understanding of the observable universe is the job of physicist who, for instance, rely on empirical evidences that are not recognized by most mathematicians (if you're using a labo measurement to prove a theorem, it is clearly not a mathematical proof even if it might be a hint). There are some very consistent mathematics system that don't apply to our universe, we should rather say that they reflect our ability to think abstractly. To which extent is this ability derived to the physical reality of our universe is a problem still defying human reason.

[Anonymous No.5412159]

>>5412113
oh I knew it was dated but that didn't mean anyone had taken up the mantle, so to speak

thanks for your post

[Anonymous No.5412178]

>>5412127
They would be useful to any species within our universe because the usefulness of mathematics is defined by physical law. You can create any arbitrary arrangement of rules, but it wouldn't be part of mathematics unless it was deemed useful.

[Anonymous No.5412187]

>>5412113
Do you know of a set of books in which a modern attempt as formalizing mathematics is done (like the guys of Bourbaki did in their time) ? I'd like to read something about that. I'm particularly interested about category theory, which I have heard about but don't know much of.

[Anonymous No.5412214]

>>5412142
I'm sorry but I don't understand your post, I do find it interesting though and would like to know more, can you recommend some literature on the subject? And saying mathematics doesn't reflect reality sounds odd to me, these rules are not chosen as mathematicians please, reality is perceived and rules are established from perception, which I assume on some level is connected to reality?

[Anonymous No.5412270]

>>5412187
Bourbaki's style was pretty influential, and all graduate level mathematical texts use an similar style and equal level of rigor (that is the maximum level of rigor reasonable for humans).

As >>5412113 pointed out, the only way to take things further in terms of rigor, is to use computer verification of proofs. I very much doubt this would change most of the core results in mathematics, since any proof in them would already have been discovered, but it would probably yield many mistakes in newer or more esoteric work.

As far as I know we are not, however, very close to being able to verify real proofs of modern mathematics with computers using a reasonable amount of effort.

[Anonymous No.5412276]

>>5412187
Things are generally done more piecemeal now; like I said, the foundations are solid (barring the off-chance of an inconsistency), so there's not as much need for one big work that formalizes everything. It'd be a huge undertaking, and there wouldn't be much of a benefit, since things are standardized and formalized enough already that it's easy to translate between different frameworks and conventions.

If you want to read more about category theory, MacLane's "Categories for the Working Mathematician" is the classic text. It's definitely graduate-level, though, and assumes a lot of background knowledge; MacLane freely draws on examples from algebraic topology and abstract algebra, so it's very difficult to read if you don't have enough familiarity with those.

Also, Lang's "Algebra" has some nice introductory material on category theory, too, so it might be worth taking a look. The first chapter has a section introducing the basics of category theory — including a very good explanation of universal properties — and another chapter near the beginning (I forget which one) has a section on abelian categories. At least for a start, this might be a better way to learn the concepts, since they're presented in a motivating context (group theory and module theory, namely) rather than purely in the abstract.

[Anonymous No.5413022]

>>5412270
> a reasonable amount of effort
What use is it as a foundation if it is tossed aside because it is too cumbersome in practice? If this isn't how people "do math" then it hardly constitutes a foundation.

[Anonymous No.5413336]

>>5412187
>>5412270
>>5412276
>>5413022
>As --- pointed out, the only way to take things further in terms of rigor, is to use computer verification of proofs. I very much doubt this would change most of the core results in mathematics, since any proof in them would already have been discovered, but it would probably yield many mistakes in newer or more esoteric work.

>As far as I know we are not, however, very close to being able to verify real proofs of modern mathematics with computers using a reasonable amount of effort.

Ha!
That's what you'd think.
But dem crazy polish formalists do it since thirty years.

http://en.wikipedia.org/wiki/Mizar_system

The library is freely available online, here is an overview
http://mizar.org/library/strnet.html

Looks e.g. like this
http://mizar.org/JFM/Vol1/binop_1.abs.html
(that's the article specifying binary operations etc.)

It's based, as I understand, around a version of the generous Grothendieck axioms. Seems like a reasonable thing to do.

http://en.wikipedia.org/wiki/Tarski%E2%80%93Grothendieck_set_theory

[Anonymous No.5413347]

>>5413336
nice

[Anonymous No.5413481]

how come logic is talked about so much on /sci/ recently?

[Anonymous No.5413485]

>>5413481
Because /sci/ is full of low IQ faggots who can't into logic. Most of the posters here don't know what a logical implication is.

[Anonymous No.5413487]

>>5413336
Time to give it this to test its mettle:
http://tachyos.org/godel/Godel_statement.html

[Anonymous No.5413489]

>>5413485
> ->

[Anonymous No.5413575]

http://homotopytypetheory.org/

[Anonymous No.5413697]

>>5413575
http://en.wikipedia.org/wiki/HoTT
lol freaky.

Appearently these people just reinterpret the synatcical structure of homotopy theory like a logical calculus - hence there is a Curry–Howard correspondence from the theory to (types of) functional computation.
I'd really like to see if one can abstractly study the syntactical properties of general mathematical theories (like differential geometry, say) and in this way math totally different mathematical fields together, but pointing out in what sense they differ and in what sense they don't.
Well, it might well be that topos theory is just that, to some extend.

[Anonymous No.5413702]

>>5413575
http://en.wikipedia.org/wiki/HoTT

lol, freaky.

Appearently these people just reinterpret the synatcical structure of homotopy theory like a logical calculus - hence there is a Curry–Howard correspondence from the theory to (types of) functional computation.
I'd really like to see if one can abstractly study the syntactical properties of general mathematical theories (like differential geometry, say) and in this way match totally different mathematical fields together. I mean By pointing out in what sense they differ and in what sense they don't.
Well, it might well be that topos theory is just that, to some extend.

[Anonymous No.5413826]

>>5413702
They reinterpret intensional dependent type theory as homotopy theory/(infinity,1)-category theory. This gives you foundations that respect isomorphisms by default, has a geometric interpretation, can compute, and subsumes logic and set theory since propositions are defined as (-1)-types and sets as 0-types. Everybody's a winner.

>I'd really like to see if one can abstractly study the syntactical properties of general mathematical theories (like differential geometry, say)
http://ncatlab.org/nlab/show/differential+homotopy+type+theory
If you're interested and can get past the generalized abstract nonsense, there's lots of material about HoTT on nLab.

[Anonymous No.5413842]

>>5413336
That's cool. I had high hopes when I started reading it. For example, using computer proof verification for math Olympiad style problems. But according to the tutorial (see link)
>A proof that takes five minutes to explain... takes about a week to formalize.

http://web.cs.ualberta.ca/~piotr/Mizar/MiniTut/New

[Anonymous No.5413850]

>>5412214
mathematic rules are taken from logic, the purest of sciences

[Anonymous No.5414423]

>>5413826
Sounds cool, but unlearnable in finite time :/

[Anonymous No.5416265]

>>5414423
It's easier than it seems (especially if you know some type theory already), it's evil homotopy theorists that make it seem difficult with their funny terminology.

[Anonymous No.5416294]

>>5416265
I was thinking about it again today (about how to get a grasp of the minimal syntax of a general mathematical theory) and thought (again) that to skim it off it might really be best to take a look at the category theoretical formulations of these things. My argumentation would be that there you have already implemented the features of associativity of function (as well as the "up to isomorphism" thing). It would be a nice project to get a hold of the axiomatizations of several subjects that way. You know, not just "we take numbers from aritmetic, and we understand tensors from the general algebraic theory", not in this top down "everything is a model if we start with first order logic and sets", but in a way which highlights only the necessary axioms/syntax of different fields.
My plan would really not be to give computation a geometry meaning, but the other direction: reduce all math to formalist gameplay, representations of algorithms.
</rant about ideas of an uninformed physicist>

[Anonymous No.5416387]

>>5416294
HoTT IS looking at the category theoretical formulations.
The idea is that categories, languages and logic are three sides of the same coin (don't ask me how a three sided coin would look like), whenever you have one you have the others, insights on one transfer to the other two which leads to more insights and so on.
An example is coinduction in TT (and thus logic), which come from the dualization of induction in CT;
or the realization that logics don't have to be (-1)-truncated from TT, and that mathematicians don't even use them as such, the axiom of choice is usually used to extract a choice function, you can easily prove the proof relevant axiom of choice in intensional type theory;
or the interpretation of types as topological spaces (or as higher groupoids), "propositions" as (-1)-types and sets as 0-types in HoTT itself, which comes from the fact that homotopy theory is basically (infinity,1)-category theory with different terminology.
Having all mathematics built from sufficiently expressive foundations (like, not set theory) shows more clearly all kinds of different relations between various seemingly unrelated fields. Heck, category theory exists almost only to formalize those relations.
Separating everything again is definitely the wrong way to go.

[Anonymous No.5417284]

sadly, (-1)-truncation and and (infinity,1)-categories are beyond me, nLab doesn't help too much.

[Anonymous No.5417508]

>>5417284
My bad, I got used to the terminology and sometimes assume everyone will know what I'm talking about
An (-1)-truncated object is a truth value (either true/inhabitated or false/empty). The actual definition is "A is (-1)-truncated iff any two objects of A are equal", or "isProp(A) := ∀x,y:A.x=y". This is obviously true for the singleton set/unit type, and vacuously true for the empty set/type.
Therefore, propositions in usual logics are (-1)-truncated, because if they are provable, they're either false (and equivalent to the empty type) or true (and equivalent to the unit type) without carrying information of how it's true
0-truncated objects are sets. The singleton set and empty set are sets too, so you can think of sets as more general propositions. The simplest non-propositional set is the two-element set (the Bool type).
Bool has two elements: "true" and "false", both of which are valid PROOFS of Bool, thus proofs of Bool carry more information (one bit) than a proof of the unit type (which must be always the same, as the unit type has one element). This is why the propositional version of the axiom of choice is unprovable, but the type theoretic version is provable
The definition of set is "all proofs of equality between two elements of A are the equal", or "isSet(A) := ∀x,y:A.∀p,q:(x=y).p=q", or even better "the type of equality proofs between two elements of A is a proposition", "∀x,y:A.isProp(x=y)". All type theories until HoTT postulated that all types are sets.
HoTT goes even further and lets you define types that are groupoids ("∀x,y:A.isSet(x=y)") and higher groupoids
Also, n-truncated object, n-groupoid and homotopy n-type are synonyms. The count starts at -2 because of hysterical raisins
(infinity,1)-categories are the categories where homotopy theory takes place, only because the category of all infinity-groupoids is an (infinity,1)-category and higher homotopies form higher groupoids

[Anonymous No.5418545]

>>5417508
thanks for the response.

- on the category side:
Okay, I read up on the higher category concepts a little.
Should I foremostly think of the 'objects and their elements' as 'sets and subsets' (as in topos theory) or as 'types and "things of that type" '?

Are "things of that type" equal to functions? Or should I think of them as the proofs? Or what?
Because you say
> This is why the propositional version of the axiom of choice is unprovable, but the type theoretic version is provable
You mean this is right simply because the (-1)-truncated thing has nothing in it, do I understand that correctly?

Also, how do the higher types relate to the n-morphisms?

- to find out what we're dealing with and why we are doing this stuff:
I don't understand what is new to HoTT. Isn't the language of the "geometric theory" (homotopy theory) just as valid as any syntactical construction. What kind of things are we dealing here, how do I think of these things if they are not sets of sets etc. and what difference does it make?

[Anonymous No.5419293]

>>5418545
My post length grows exponentially. This is going to be a wall of text, sorry.

>Should I foremostly think of the 'objects and their elements' as 'sets and subsets' (as in topos theory) or as 'types and "things of that type" '?
Types and their elements. (Non-higher) types are kind of like sets (and 0-types actually are sets), but with a simpler structure. Imagine sets without the ∈ predicate and extensional equality.
Elements of a type are, well, elements of that type. If the type is Nat, the elements are natural numbers, if the type is A -> B, the elements are functions from A to B, and so on. You don't define types as types of types of types/functions of functions of functions in modern type theory, you define them structurally. For example, you define the type of natural numbers Nat as (pseudo-Agda code):

data Nat : Type where
Zero : Nat
Succ : Nat -> Nat

Which says: Nat is an inductive type, Zero is a Nat, for any n that's a Nat, Succ n is a Nat. That, and the induction principle:

nat-induction : (P : Nat -> Type) -> P Zero -> ((n : Nat) -> P n -> P (Succ n)) -> (n : Nat) -> P n
nat-induction P pzero psucc Zero = pzero
nat-induction P pzero psucc (Succ n) = psucc n (nat-induction P pzero psucc n)

are the only structure that the type Nat has.
Type theory is the simplest thing on earth, but the problem is that it looks too much like set theory to people used to set theory, but it really isn't. If you're interested you should try reading a book on Martin Lof type theory with a blank state of mind, 4chan isn't the best place to seriously learn about anything. I started with type theory first, so I don't know what to suggest, maybe "Programming in Martin Lof type theory", which also draws analogies with sets and shows how they're different.
http://www.cse.chalmers.se/research/group/logic/book/book.pdf

(cont)

[Anonymous No.5419294]

>>5419293
>You mean this is right simply because the (-1)-truncated thing has nothing in it, do I understand that correctly?
Yes. The axiom of choice is equivalent to "every surjection has a right inverse": ∀A,B:Type.∀R:(A,B)→Type. (∀x:A.∃y:B.R(x,y)) → (∃f:A→B. ∀x:A. R(x,f(x)))

Martin Lof Type theory's "existential" quantifier (called "strong Sigma" or just "Sigma") is stronger than the classical existential (which is kind of (-1)-truncated), if you have y:(Σx:A.P(x)), y is a pair (x,p) of an x such that P(x) holds, and p is a proof of P(x). Since the (∀x:A.∃y.R(x,y)) term gives you for any x an y such that R holds, you can extract f from it. If (y:A) × (P y) is the notation for Σy:A.P(y), then the axiom of choice is:

AC : (A B : Type) -> (R : A -> B -> Type) -> ((x : A) -> ((y : B) × (R x y))) -> ((f : A -> B) × ((x : A) -> R x (f x)))
AC A B R g = (λx.fst (g x), λx.snd (g x))

Where fst (x,p) = x and snd (x,p) = p. If the existential were (-1)-truncated, we would be able to prove it.

>Also, how do the higher types relate to the n-morphisms?
The n-isomorphisms, in the context of HoTT, since higher types are regarded as higher groupoids, are the type of equality between two elements of a type Id(A,x,y) (morphism), equality between equalities Id(Id(A,x,y),p,q) (2-morphism), equality between equalities between equalities (3-morphism) Id(Id(Id(A,x,y),p,q),α,β) and so on.
When you look at types as topological spaces, identity types become paths (= continuous deformations) between points of the type. Paths between paths are homotopies, paths between paths between paths ... are higher homotopies.

(cont)

[Anonymous No.5419297]

>>5419294
The HoTT I talked about up until now is a boring one, although you can't prove all types are sets, the only path you'll ever see is the trivial reflexivity path, you can't construct any type higher than a set, and as such you can't construct interesting topological spaces such as the interval or the circle. To do that, you must somehow add paths to the definition of the type, that's called higher induction. For example, the interval is defined as two points and a path between them:

data Interval : Type where
zero : Interval
one : Interval
segment : zero = one

Functions on the interval now MUST respect the equality zero = one, and thus they must return "equal" results for zero and one (and prove they're equal). Of course, when your notion of "equality" isn't restricted to be (-1)-truncated, you can actually construct less boring functions on the interval.
Also, note that the Interval qualifies as (-1)-truncated (all points are connected by paths: refl(zero) : zero = zero, refl(one) : one = one, segment : zero = one, and it's actually (-2)-truncated (= contractible space/type) since it's also inhabitated). That means (-1)-types are not merely just the unit type and the empty type. In fact, you can define (-1)-truncation, which, as the name suggests, truncates any n-type to a (-1)-type.

data Inhabitated (A : Type) : Type where
Inhab : A -> Inhabitated A
Inhab_path : (x y : A) -> Inhab x = Inhab y

(cont)

[Anonymous No.5419300]

>>5419297
If A is empty, Inhabitated is going to be empty too. If A is inhabitated, Inhab_path forces all Inhabs to have a path between them, making Inhabitated A (-1)-truncated. Also, all functions must provably respect that equality as always.
But now (-1)-truncated types are not completely devoid of content: consider the type of isomorphisms, to which you must provide a function, its inverse, and proofs that they are indeed inverses. You obviously don't care how the inverse was written, or what the proofs of inverseness are, you only care that the inverse inverses, and the proofs are valid. So, if you write a function on the (-1)-truncated type of isomorphisms, you can freely use the inverse as they all do the same thing.

(cont)

[Anonymous No.5419302]

>>5419300
>I don't understand what is new to HoTT.
For category theory:
- nothing really new, interesting categories have interesting type theories as internal logic.
For type theory and logic:
- A better interpretation of types.
- Higher inductive types.
- Univalence (isomorphic types are equal).
- From the last two: provable functional extensionality and usable quotient types.
For homotopy theory:
- For the first time it computes.
- Everything respects homotopies and behaves nicely.
- Probably something else, I'm not an homotopy theorist.
For foundations of mathematics:
- It focuses on structure, everything respects isomorphisms, homotopies and equivalences. Isomorphic things are treated as equal like in ordinary mathematics.
- It's not set theory (seriously, axiomatic set theory is ugly at low level and unintuitive at high level)
- But sets and propositions are defined in the theory, as are higher groupoids.
- It's constructive, which means it computes. You can recover classical logic by working in the double negation monad.
- Even though it's meant to be the foundations, it's pretty nice to work with, it's easier to formalize things.

>Isn't the language of the "geometric theory" (homotopy theory) just as valid as any syntactical construction.
It is, HoTT the internal language of homotopy theory. You get it naturally from homotopy theory/(inf,1)-cats. HoTT provides the syntax, (inf,1)-category theory provides the semantics.

[Anonymous No.5419323]

>>5419294
> disgracing he aims of Betrand by posting shitty agda code
so disappointed

[Anonymous No.5419334]

>>5419323
But Coq is the Java of theorem provers!

[Anonymous No.5419341]

>>5419334
* Agda: the surface language is intertwined with the ridiculously complicated ad-hoc moving target that they call the internal theory
* Coq: mature well developed system based on the de bruijn principle of having a simple internal theory which more complicated constructions are expressed in terms of

[Anonymous No.5419364]

>>5419341
Tell me that when your coinductive types don't break type preservation.
And Agda is meant to be experimental (but handles coinductive types better than Coq)

[Anonymous No.5419374]

>>5419364
>bringing up the coinductive types thing
lel I could list about 10 times false has been proved in agda.

[Anonymous No.5419392]

>>5419374
Last time it was April 18th 2012 with https://lists.chalmers.se/pipermail/agda/2012/003904.html, which isn't even a failure in the type theory, but a silly bug with pragmas that's now fixed. Again, as Agda is experimental, and the bugs are fixed, it is acceptable. But Coq is an "industrial strength theorem prover", yet its coinductive types still don't preserve types, am I wrong?

My "Agda" code wasn't even real Agda, Type is called Set, λx.E is written λx → E, and dependent pairs are written Σ[ x : A ] P x, don't get so butthurt over syntax. Just think it's CiC with a more presentable syntax.

[Anonymous No.5419436]

I'm very skeptic of these recent developments in foundational mathematics. Not that they're quackery, but it seems that what the Russians feared when the French introduced more abstract formalisms has finally come to be: useless over-abstraction. Sure, it's a neat idea to use the syntax of homotopy theory as a possible basis for mathematics, but all this talk of it being constructible and hence computable is just misdirecting bullshit. Too often it just turn out that explicit realizations of these objects are either trivial or forced to be complex rendering them uninteresting in regards to any sane applications. The only applications of higher category theory I can see so far is possibly a new foundation for algebraic topology, but even then no one has yet computed higher homotopy groups of spheres. Classical category theory hasn't done much besides giving us a formalism that saves us from repeating arguments; there's basically no result that couldn't have been proven without the language of category theory (and don't come with Brown representability or Yoneda, these types of arguments have been used since Cayley's theorem). So I really don't see how higher category theory could be interesting in any way at this point. Even I would call this pure mental masturbation, and I mostly do work on homological algebra.

[Anonymous No.5419438]

>>5419392
just depresses me that all you people interested in formal computer proof don't even care about things like de bruijn criterion

[Anonymous No.5419497]

>>5419302
k, thanks I'm going to save that and maybe thing about it more at a later point where I understand more.
Btw. do you have any means to contact you, or a blog or something?

Lastly, you list "it does compute" as a strength. I guess I know in what sense you mean that, namely that the theories syntax gives you computable functions or proves via the Curry-Howard Correspondence.
But what "nice fact" do you actually think aboout when you say the theory computes? Like do you ever actually use any of the "algorithms abstractly given via the correspondence"? I see that correspondence more as a means to abstract away from theories with their intended meaning.

[Anonymous No.5419540]

Obviously, I tried to do a quick google search. Maybe I'm not using the correct terms. A short note before I begin, I'm talking about Canadian taxes/pay.

I've been wondering this for a while; how do you calculate how much taxes, E.I., should be taken from your pay? A friend claimed that if he worked simply 2 more hours a week, he would make LESS money for working more hours. As for myself, I am considering taking another job... it would be much less pay than my current job, so I want to weigh the tax implications of this.

Is there any gov't web page that explains how this works?

[Anonymous No.5419564]

>>5419436
Mhm, set membershit vial \in is natural. I wouldn't dismiss it. But then, as a physicist, I kind of see the mere "existence" of cardinal numbers of all sorts as acciendent of set theory, merely emerging from it's structure. On the other hand, I really how associativity (of function like objects) is implemented in the axioms of a category. This makes me somehow feel that some version of a category-like approach might be well suited for an introduction to higher mathematics.
I also think with investigations model theory*, we are long beyond the level of hyper-abstraction, of which the Kolmogorovs and Arnolds of this world were afraid of.

*I love how algebraic logic
http://en.wikipedia.org/wiki/Algebraic_logic

must really be a hands on subject, given the fact that there is abstract algebraic logic

http://en.wikipedia.org/wiki/Abstract_algebraic_logic


:D

[Anonymous No.5419576]

>>5419436
I know what you mean, I'm excited about HoTT because it lets me decypher the abstract nonsense using something I'm familiar with (and because it's an improvement over current type theories). To me, the correspondences with homotopy theory, category theory and whatever are just happy coincidences I get for free for using the better thing. Your mileage may vary, of course.

>>5419438
I am, and surely I'm not the only one, but I also don't expect an experimental theorem prover's internal theory to be the simplest tarpit on which you can build everything.

>>5419497
I'm on /sci/'s IRC channel on Rizon, nickname's DT`.
I don't think having a theory that computes will be of much use after the fact, but it does comes in handy when writing verified software.

[Anonymous No.5421653]

I think this is the most high level thread 4chan has seen to date.

[Anonymous No.5421701]

>>5413842
I've done some of the easier PPotD in Coq. It was a lot closer to a day than a week, but then again, the human versions of the proofs could be explained in a lot less than 5 minutes.

[Anonymous No.5422121]

It a type is to be understood as a proposition or a specification, and its elements as proofs or function, ...
how to read Bool?
I mean how are its elements 0,1 to be considered as eighter proves or functions?
And in what sense do they both prove the type?

And if elements of a type are functions and are at the same time like elements of sets, what does equality mean in terms of functions? Does it mean that there is a reduction which equalizes the functions?

[Anonymous No.5422153]

>>5422121
okay, maybe I say the elements are intensionally different.
But this still doesn't explain one thing;:
A proofs entails what proposition in proves and equally, I can read of the type of a function. But how then does the type as set identification make sense:
Given one proof / function I know the proposition / type. But an element of a set can be contained in many sets and so if I tell you just an element, you can't reconstruct the set!?

[Anonymous No.5422215]

>>5422121
>>5422153
Think of it as a type.
Elements of a type are not functions, elements of types have no more structure than their introduction and elimination rules, which also determine how they compute. For Bool, you introduce it either with 0 or 1, you elimine it by specifying what to do when it's 1 and when it's 0 (i.e., "if then else"). Nat, Bool, and other "concrete" types are not interesting as "propositions" (I don't restrict propositions to mean (-1)-truncated objects here), more interesting propositions come up when talking about dependent types. For example, the type of a proof of associativity of + is:
plus_comm : (x y z : Nat) -> x + y = y + x
(insert proof by induction here)
When you want to think them as sets, they're not ZF-sets. ZF-sets have extensional equality and the ∈ predicate, just sets don't. In type theory, sets equipped with an equality are called setoids. Since elements of types don't have an intrinsic notion of identity, it doesn't make sense to ask whether x ∈ A, which is also how everything respects isomorphisms by default (even without HoTT, but you can't prove it IN the theory). You can recover the notions of subset and superset with injections and surjections.