semolinapudding

12 ms·

1.
by semolinapudding 1y ago
FLT is a negative statement ("there are no nonzero integers x, y, z such that..."), and proofs by contradiction are constructively valid for proving negative statements.
2.
by semolinapudding 1y ago
For what it's worth, I don't think that Kevin Buzzard is the person you should talk to if you are interested in proof assistant design. As far as I know, Buzzard does not consider himself to be an expert in type theory or in proof
3.
by semolinapudding 1y ago
AFAICT, this issue only comes up if you form the quotient of a proposition by a relation. But there is no point in doing that (all the proofs of a proposition are already equal!) so it's not an issue in practice and it wouldn't
4.
by semolinapudding 1y ago
Computation is the difference. In Lean, applying the universal property of the quotient (`Quotient.lift f Hf`) to an element that is of the form `Quotient.mk a` reduces to `f a`. This rule is fine in itself, but the Lean developers were not
5.
by semolinapudding 1y ago
There is a nice illustration of a 2-sphere wrapped twice around another 2-sphere on the Wikipedia article for the homotopy groups of spheres [0]. Now, there are many ways of proving that there is only one way (up to homotopy) of wrapping a
6.
by semolinapudding 2y ago
This makes me wonder whether the usual order for function application is an artifact of the S-V-O sentence structure in western European languages. Maybe if Euler had been raised in a language with a S-O-V sentence structure, we would write
7.
by semolinapudding 2y ago
Good catch, thank you.
8.
by semolinapudding 2y ago
That's pretty cool, but the downsides of switching to RRA are not only about user experience. When the result is 0.0000000..., the calculator cannot decide whether it's fine to compute the inverse of that number. For instance, 1&#
9.
by semolinapudding 2y ago
ZFC is way worse than Presburger arithmetic -- since it is undecidable, we know that the length of the minimal proof of a statement cannot be bounded by a computable function of the length of the statement. This has little to do with the us
10.
by semolinapudding 2y ago
There's a bit of a definition issue at play here. When Andreas Blass and Noah Schweber say that there is no proof system for PA_2, they mean that there is no effective proof system that is complete for the full semantics. If you subscr
11.
by semolinapudding 2y ago
If you look at the Wikipedia page for second order arithmetic, there is a definition in the language of first order logic as a two-sorted theory comprising a handful of basic axioms, the comprehension scheme, and the second-order induction
12.
by semolinapudding 2y ago
The axioms of second order Peano arithmetic are certainly recursively enumerable, in fact you can pick a formulation that only uses a finite number of axioms. And second order arithmetic is much weaker than the type system of Lean, which is