Reputation
1,054
Top tag
Next privilege 2,000 Rep.
Edit questions and answers
Badges
4 15
Newest
 Civic Duty
Impact
~3k people reached

1d
revised Proof by reflection and Homotopy Type Theory
edited body
1d
asked Proof by reflection and Homotopy Type Theory
2d
awarded  Civic Duty
Jun
26
comment anyone can help me with solving this $x^{x^{3}}=3$?
@EulCan $\sqrt[3]{3}$ is in fact a solution to the latter form.
Jun
26
comment Can one differentiate a series after taking its limit?
@DanielLittlewood His error in fact was not the interaction between the limit and the derivative, so no it doesn't show anything of the sort.
Jun
26
comment Can one differentiate a series after taking its limit?
You are not taking a limit of the variable you are differentiating with respect to, so it is still a free variable in the resulting expression. If you tried to differentiate with respect to $n$ after taking the limit of partial sums, then yes that would be an issue. However you are ignoring the radius of convergence of the series, which is why you are able to prove a false conclusion.
Jun
24
comment Reference request for Zermelo's construction of natural numbers
@user170039 I have detailed the parts of the construction that vary from the von Neumann naturals, for which you can turn up many presentations of the proofs of the Peano axioms. I suggest you look at those if you have difficulty understanding the construction, because as I said only the very beginning of the development (i.e. proving Peano's axioms) has any differences. I would be surprised if you could find a reference on this, because even number theorists and mathematical logicians don't particularly care since nobody writes out the natural numbers as sets.
Jun
24
comment Reference request for Zermelo's construction of natural numbers
@user170039 They are isomorphic in the sense that the two sets can be placed in bijection with each other in such a way that the successor (and by extension all other natural number operations) is preserved. So the only thing that is different is the truth value of statements like $1 \in 2$ which are not used in number theory.
Jun
24
answered Reference request for Zermelo's construction of natural numbers
Jun
24
comment A sheet of formulas for practical application of Integration?
You'll need to be more specific, in the current scope of your question your whole binder will be filled, even if we stick to the basics.
Jun
22
comment Logic vs. type system
@goblin I would be very surprised if it were. These aspects are the burden of proof relevant mathematics. However, we regain classical logic if we stick to mere propositions. In homotopy type theory, this is actually possible for general propositions (including those you listed above). For each type $A$, one can define a type called a 0-truncation which satisfies $A \to \left | A \right |$ and $\forall x,y : \left | A \right | \; x = y$. Essentially it is a quotient over the type $A$. The price you pay is that you can only use it to prove other mere propositions.
Jun
22
comment Does mathematics become circular at the bottom? What is at the bottom of mathematics?
As far as your concern with equality, it depends on the theory. The most common foundation in ZFC, where $x = y$ is shorthand for '$x$ and $y$ have the same elements'. In ZFC, everything is a set (such theories are called material set theories), even $1$, $i$, and $\sqrt{2}$.
Jun
22
comment Logic vs. type system
Let us continue this discussion in chat.
Jun
22
comment Logic vs. type system
@goblin You are confusing $(A \wedge A \to A) \wedge (A \to A \wedge A)$ with $A \wedge A = A$. The former is of course always true; but it does not imply the later. For $A \wedge A = A$ we need a bijection, which clearly does not exist if $A$ has more than one inhabitant. In essence, the classical iff is not the same as equality in type theory.
Jun
22
comment Logic vs. type system
@goblin Thats the whole point. Such an $A$ is not a mere proposition. $A \times A = A$ only holds if $A$ has no more than one proof. Otherwise they won't be equal, because there will not be a bijection between them.
Jun
22
comment Logic vs. type system
@goblin That is only true if $A$ is what homotopy type theorists call a "mere proposition". Such a type has the property that all inhabitants are equal (but note there may be no inhabitants). If a set contains 0 or 1 elements, then we do have $A \times A \cong A$. However, if we have a type with multiple inhabitants, then they are not isomorphic, just as in the set case.
Jun
20
revised Lebesgue integration
Inserted latex
Jun
20
suggested approved edit on Lebesgue integration
Jun
16
comment Showing that $\Bbb R^3$ is not homeomorphic to $S^3$.
@SkiesBurn Compactness is a topologically invariant property of a space, independent of any space it may be embedded in. So if a subspace is compact anywhere (where we of course need to be consistent about the topologies), it is compact.
Jun
15
comment How to compute the derivative of $x^x$ using the definition
@Christopher The final limit in the above answer is tantalizingly close; if you switch variables from $h$ to $n = 1/h$, the limit becomes $\lim_{n \to \infty} n (e^{1/n} \sqrt[n]{x + 1/n} - 1)$. If not for the $+ 1/n$ under the square root, we would already be done; as it would equal $\log(e x) = \log x + 1$.