Reputation
1,069
Top tag
Next privilege 2,000 Rep.
Edit questions and answers
Badges
4 16
Newest
 Cleanup
Impact
~4k people reached

2d
comment Proving $\sum_{i=1}^n 2^i = 2^{n+1} - 2$ using strong induction
Did you mean $2^{n+1}$ on the right side of your first equation?
Jul
30
comment Disequality in Type Theory
@ZhenLin Thank you! The HoTT in the title threw me off.
Jul
30
awarded  Cleanup
Jul
30
revised Disequality in Type Theory
rolled back to a previous revision
Jul
30
comment Disequality in Type Theory
@user122283 I used disequality because inequality risks confusion with inequalities (i.e. $x > y$), which are totally distinct. This term is used for example in the Homotopy Type Theory book, so it is not without precedent.
Jul
30
asked Disequality in Type Theory
Jul
7
comment Is it known whether a hypothetical P-time NP-complete decision procedure has to find a specific solution to the given constraint satisfaction problem?
Yes, it is precisely the opposite. A witness to primality would be a proof of some property that only primes have. The most trivial one would be the results of division by all integers less than the number. AKS almost provides a (different) witness of primality, but its polynomial running time relies on a proof that it (in essence) doesn't have to check all cases of the property.
Jul
7
comment Is it known whether a hypothetical P-time NP-complete decision procedure has to find a specific solution to the given constraint satisfaction problem?
The formal definition of $P$ requires a mere (correct) yes-or-no answer, so the possibility that a problem in $P$ may require more than polynomial time to find a witness of the result is not immediately ruled out. In general, there are algorithms that use such ad-hoc methods to answer decision problems; the AKS primality test provides a yes or no answer without a witness of primality. However primality is not believed to be NP-complete.
Jul
4
revised Proof by reflection and Homotopy Type Theory
edited body
Jul
4
asked Proof by reflection and Homotopy Type Theory
Jul
3
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}$.