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.
"It’s fine to use a proof by contradiction to show something doesn’t exist. When the assumption that it does exist leads to a contradiction, then that shows it can’t exist.
It’s not so fine to use a proof by contradiction to show something does exist. Here’s the situation. The assumption that it does not exist leads to a contradiction. What can you conclude from that? You would like say “therefore it exists”. But you haven’t got any idea what it is. You may know it’s out there somewhere, but you have no idea how to find it. It would be better to have a proof that tells you what it is.
That’s a difference between what’s called “classical logic” and “intuitionistic logic”. In classical logic, proof by contradiction is perfectly accepted as a method of deductive logic. In intuitionistic logic, proof by contradiction is accepted to show something doesn’t exist, but is not accepted to show something does exist."
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 assistants, and claims to be a mere user.
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 be difficult to fix.
However, Lean's SR is broken in other ways which do show up in practice: definitional proof irrelevance is incompatible with Lean's computation rule for Acc. That one is much harder to fix.
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 sufficiently careful and allowed it to apply for quotients of propositions, where it interferes with the computation rules for proof irrelevance and ends up breaking subject reduction (SR is deeply linked to computation when you have dependent types!) [0]. It is not really a problem in practice though, since there is no point in quotienting a proposition.
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 2-sphere n times around another 2-sphere, but all of them are fairly involved. The simplest proof comes from an analysis of the Hopf fibration, which roughly describes a relation between the 1-sphere, the 2-sphere and the 3-sphere [1]. Other than this, it follows from the theory of degrees for continuous mappings, or from the Freudenthal suspension theorem and some basic homological computations.
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 (x)f instead.
Plus, reverse function application/composition works better with our tendency to write the domain of the function before its range. Given f : A -> B and g : B -> C, the composite function is written as g o f which is mildly annoying.
> Maybe if Euler had been raised in a language with a S-O-V sentence structure, we would write (x)f instead.
This is an interesting question but it's further complicated by how frequently Euler was writing in Latin, which usually prefers (but doesn't require) SOV order.
> Genus autem secundum eiusmodi problemata complectetur, ad quae soluenda coordinatae ad duo curuae puncta pertinentes simul considerari debent; cuiusmodi erat problema de traiectoriis reciprocis, illudque problema catoptricum, quod ante aliquot annos tractavi. Cum enim in his continuo bina curuae puncta inter se conferantur, et coordinatae ad ea pertinentes in computum ingrediantur; per principium continuitatis effici debet, ut bina haec puncta ad eandem lineam curuam referantur, sicque aequatio inter coordinatas unicum punctum spectantes eliciatur.
I put all of the clauses' main verbs in italics. All of them except for "erat" ('was') are at the ends of their respective clauses! So, Euler had quite a lot of experience writing SOV sentences in technical contexts.
Programmers are pretty accustomed to thinking of functions as verbs. In some programming styles, we're even explicitly encouraged to name our functions after verbs describing what they do.
Sometimes mathematicians think of functions more as expressing a complete (and sort of timeless) relationship between a domain and a range. That relationship, considered in its totality, can be thought of as a noun rather than a verb.
Earlier mathematicians might also have tended to think of functional notation as referring to individual specific instances of the result of the calculation that the function refers to, like "the sine of 1/2" being a specific number (the result of computing the sine of one half, or, alternatively, the output of the function given a specific input). So when writing something like sin(1/2) they might not be thinking "please [person or machine] perform this computation on the number 1/2 right now" so much as "[I am here indicating] the specific [timeless and inherent] number that is the sine of 1/2". That's a different way that a function could be seen as a noun, essentially seeing the function as merely a way of referring to its output.
Calculus and real analysis start to give stronger reasons for thinking of functions as abstract objects in their own right (e.g. because we can say something like "d/dx sin(x) = cos(x)" or even "the derivative of sin is cos" without thinking about specific values. Or questions like "can a function exist that is continuous but not differentiable?". Maybe computer science then starts to give reasons for thinking of functions as descriptions of how to perform them (like source code or even machine code punched on punch cards) as opposed to references to their specific results (like a printed book of function tables, which someone else calculated ahead of time so you wouldn't have to).
This is all to say basically that maybe it's more natural for us as programmers to think of functions as verbs, but maybe Euler didn't conceive of them that way at all!
Even in modern mathematics, the postfix notation is used in some places. One example I can recall is permutations.
Consider the following permutation:
f = (1 2 3 4)
(1 4 2 3)
This is typically written in cycle-notation like this:
f = (1)(243)
If we look at the cycle notation, f maps each symbol to the one on the right. For example, it maps 1 to 1, 2 to 4, 4 to 3, and 3 to 2.
Now if we want to find out what happens to the sequence (4 3 2 1) when we apply f to it, we normally write it as
(3 4 2 1)f
The argument comes first. The function name comes next. It makes it quite convenient to work with permutations, composition of permutations, etc. For example, the result for the above application is:
You see it in some treatments of abstract algebra too. (Which are not unrelated to permutations in any case.) I think at least one book used in my undergrad used postfixes for function application, but I can't remember which.
Definitely not. (He may do that, I just hadn't ever heard of that book before today.) I think it was one of Isaacs, Herstein, or Artin, but I'm a bit too lazy to dig through my old books at the moment.
> Definitely not. (He may do that, I just hadn't ever heard of that book before today.) I think it was one of Isaacs, Herstein, or Artin, but I'm a bit too lazy to dig through my old books at the moment.
> 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 (x)f instead.
Herstein's Topics in algebra uses that notation for function application. It's surely not a coincidence that he was Polish, and that that reminds one of RPN.
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/(atan(1/5)-atan(1/239)-pi/4) outputs "Can't calculate".
Well alright, this is a division by zero. But then you can try 1/(atan(1/5)-atan(1/239)-pi/4+10^(-100000)), and the output is still "Can't calculate" even though it should really be 10^100000.
You missed a 4. You are trying to say 1/(4atan(1/5)-atan(1/239)-pi/4) is a division by zero.
On the other hand 1/(atan(1/5)-atan(1/239)-pi/4) is just -1.68866...
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 usefulness of LLMs for research-level mathematics though. I do not think that anyone is hoping to get a decision procedure out of it, but rather something that would imitate human reasoning, which is heavily based on analogies ("we want to solve this problem, which shares some similarities with that other solved problem, can we apply the same proof strategy? if not, can we generalise the strategy so that it becomes applicable?").
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 probably somewhere between Zermelo set theory and ZFC set theory in terms of proof-theoretic strength.
More generally, I think that computer scientists (in particular PL theorists and type theorists) are much more likely to use powerful logics than mathematicians, with the obvious exception of set theorists.
Do you have a reference for the second order induction schema being recursively enumerable? My understanding - I’m not a logician - is that the second order Peano Axioms are categorical. The Incompleteness theorems don’t apply to this system since the axioms are not recursively enumerable. The second order Axioms are different than second order Arithmetic.
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 axiom (in your first mathoverflow link, this is called Z_2):
An other equivalent option would be to use the language of second order logic, where you only need a finite amount of axioms, because the comprehension scheme is already included in the rules of second order logic. This one is PA_2.
Since these definitions do not refer to anything uncomputable such as mathematical truth, both systems are clearly recursively enumerable. This means that Gödel's incompleteness theorem applies to both, in the sense that you can define a sentence in the language of arithmetic that is unprovable in Z_2 or PA_2, and whose negation is also unprovable.
All of these considerations have little to do with models or categoricity, which are semantic notions. I think your confusion stems from the fact that model theorists have the habit of using a different kind of semantics for Z_2 (Henkin semantics) and PA_2 (full semantics). Henkin semantics are just first order semantics with two sorts, which means that Gödel's completeness theorem applies and there are nonstandard models. Full semantics, on the other hand, are categorical (there is only one model), but this has nothing to do with the axioms not being recursively enumerable -- it is just because we use a different notion of model.
PS: I certainly do not consider mathematics to be included in computer science. Even though as a logician, I have been employed in both mathematics departments and computer science departments...
Andreas Blass in the comments says that the Incompleteness results don’t apply to the second order Axioms (tabling about PA_2 here and not Z_2) and that the second order axioms are not computably enumerable. Maybe that’s the correct concept I was remembering from mathematical logic class. Don’t know if computably enumerable is the same as recursively enumerable but given what you’ve said I’m guessing they are different notions.
Consider the standard model of ZFC. Assume ZFC is consistent. Within this model there is one model of PA_2. Collect all true statements in this model of PA_2. Call that Super PA. That’s now my axiomatic system. I now have an axiomatic system that proves all true statements of arithmetic. Surely this set of axioms is not recursively enumerable.
Full semantics, on the other hand, are categorical (there is only one model), but this has nothing to do with the axioms not being recursively enumerable -- it is just because we use a different notion of model.
If those axioms were recursively enumerable then the Incompleteness theorems would apply, right?
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 subscribe to their definition of a proof system, you end up saying that there is no such thing as a proof in PA_2, and thus that incompleteness is meaningless -- which I personally find a bit silly.
On the other hand, proof theorists and computer scientists are perfectly happy to use proof systems for second order logic which are not complete. In that case, there are many effective proof systems, and given that the axioms of PA_2 are recursively enumerable (they are in finite number!), Gödel's incompleteness will apply.
If you are still not convinced, I encourage you to decide on a formal definition of what you call PA_2, and what you call a proof in that system. If your proof system is effective, and your axioms are recursively enumerable, then the incompleteness theorem will apply.
> and that the second order axioms are not computably enumerable
He says that true sentences in second order logic aren't computably enumerable, he's not talking about the axioms.
> Don’t know if computably enumerable is the same as recursively enumerable
I've only ever seen them used as synonyms.
> Collect all true statements in this model of PA_2. Call that Super PA. That’s now my axiomatic system. I now have an axiomatic system that proves all true statements of arithmetic. Surely this set of axioms is not recursively enumerable.
What you call "Super PA" is called "the theory of PA". Its axioms are indeed not computably enumerable. That doesn't mean that the axioms of PA themselves aren't computably enumerable. And this much is true both for first and second order logic.
(edit: in fact, the set of Peano axioms isn't just computably enumerable, it's decidable - otherwise, it would be impossible to decide whether a proof is valid. This is at least true for FOL, but I do think it's also valid for SOL)
...it's decidable - otherwise, it would be impossible to decide whether a proof is valid.
Isn't that the whole issue with PA_2 vs. PA? In PA_2 with "full semantics" there is no effective procedure for determining if a statement is an axiom. In my mind this is what I mean by the incompleteness results not applying to PA_2. They do apply to Z_2 since that is an effective (computable?) system.
But Z2 is usually studied with first-order semantics, and in that context it is an effective theory of arithmetic subject to the incompleteness theorems. In particular, Z2 includes every axiom of PA, and it does include the second-order induction axiom, and it is still incomplete.
Therefore, the well-known categoricity proof must not rely solely on the second-order induction axiom. It also relies on a change to an entirely different semantics, apart from the choice of axioms. It is only in the context of these special "full" semantics that PA with the second-order induction axiom becomes categorical.
> My understanding - I’m not a logician - is that the second order Peano Axioms are categorical. The Incompleteness theorems don’t apply to this system since the axioms are not recursively enumerable
Incompleteness does apply to second order arithmetic (it applies to every logical system that contains first order PA), but due to different reasons: second order logic doesn't have a complete proof calculus. "Second-order PA is categorical" means that there is only one model of second-order PA, that is, for every sentence P, either PA2 |= P or PA2 |= not(P), but you'll still have sentences P such that neither PA2 |- P nor PA2 |- not(P) - and for "practical" purposes, the existence of proofs is what matters.
> Take the collection of all true statements and make that your axiomatic system.
A complete proof system needs to be able to derive Γ |- φ for every pair Γ, φ such that Γ |= φ. Not just when Γ is the complete theory of some structure. Completeness of first-order logic (and its failure for second-order logic) is about the logical system itself, while the incompleteness theorems are about specific theories - people often mix these up, but they talk about very different things.
> Andreas Blass in the comments says that Incompleteness does not apply to PA_2.
He says something rather different, namely that its "meaningless". That's a value judgement. Incomplete proof calculi for second order logic do exist (e.g. any first-order proof calculus) and for those, what I wrote is true. Andreas Blass would probably just think of this as an empty or obvious statement.
However, my understanding is that the incompleteness results apply to only recursively enumerable axiomatic systems. I can find references for this. If I take the standard model of ZFC and collect all true statements in the one model of PA_2 and make that my axiomatic system then I have an axiomatic system that is not recursively enumerable and contains PA_1. It’s not a nice set of axioms. It’s not computable. But it shows that one can have an axiomatic system that contains PA_1 for which the Incompleteness theorems don’t apply.
Andreas wrote “meaningless” not “nonsensical”. I’m not a pedant but the former term evokes in me the idea of “does not apply in this situation becausethe hypotheses of the incompleteness theorem are not satisfied”.
From a mathematical logic book is the following. It’s the set up for the Incompleteness theorems.
Suppose that A is a collection of axioms in the language of number theory such that A is consistent and is simple enough so that we can decide whether or not a given formula is an element of A.
PA_2 is not such a system and as such the Incompleteness Theorems don’t apply. Maybe we are talking past each other. You know more than me.
> However, my understanding is that the incompleteness results apply to only recursively enumerable axiomatic systems. I can find references for this.
That's a matter of semantics as to what you consider the first incompleteness theorem to be precisely (of which there are several variants). Gödel's proof itself doesn't directly work for second-order logic. But the statement "if Γ is some axiomatic system that satisfies certain conditions, then for any sound proof calculus there is a sentence that isn't provable from Γ in this calculus" is true in second order logic too, it's just that the "failure" happens much "earlier" (and is in some sense obvious) than in the case of FOL.
> PA_2 is not such a system and as such the Incompleteness Theorems don’t apply.
I'm really not all that familiar with second-order PA, but it is my understanding that the set of its axioms is decidable. It consists of a finite collection of axioms plus one schema (comprehension axiom) which is valid when it's instantiated by any given sentence - but deciding whether something is a valid sentence is easy. Therefore, what you quoted applies to second-order PA too.
From what you and the other person on this thread has said and from what I've read it appears that perhaps the following is true:
1. The axioms of PA_2 are recursively enumerable.
2. The full semantics of PA_2 are what cause categoricity.
It seems to me then that the crux of the matter is that the full semantics of PA_2 prevent there being an effective deductive system. I think Z_2 is constructed to get around the non effectiveness of the full semantics of PA_2 and is a weaker theory.
With the caveat that I don't really understand second order logic well enough to say all that much about it, there's a debate in the philosophy of mathematics as to whether second-order logic should count as the foundational logic, since on the one hand most first-order theories aren't categorical (due to Löwenheim-Skolem) and on the other hand, second order logic (with full semantics) already presupposes set theory.
In any case, the reason why PA_2 is categorical is because the second-order axiom of induction allows quantification over arbitrary sets which allows you to say that "0 and adding the successor function to 0 arbitrarily often already gives you all natural numbers".
