John Colanduoni
Reputation
1,069
Top tag
Next privilege 2,000 Rep.
 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? Jul30 comment Disequality in Type Theory @ZhenLin Thank you! The HoTT in the title threw me off. Jul30 awarded Cleanup Jul30 revised Disequality in Type Theory rolled back to a previous revision Jul30 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. Jul30 asked Disequality in Type Theory Jul7 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. Jul7 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. Jul4 revised Proof by reflection and Homotopy Type Theory edited body Jul4 asked Proof by reflection and Homotopy Type Theory Jul3 awarded Civic Duty Jun26 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. Jun26 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. Jun26 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. Jun24 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. Jun24 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. Jun24 answered Reference request for Zermelo's construction of natural numbers Jun24 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. Jun22 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. Jun22 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}$.