View Full Version : formal proofs, where....?
In which fields of maths are formal proofs used often?
CRGreathouse
May30-09, 07:05 PM
Foundations of mathematics (logic). They're really not used elsewhere!
Outside of mathematics, they are used in computer science in the formal verification of computer programs, automatic theorem proving/checking, and in the AI field of expert systems.
Foundations of mathematics (logic). They're really not used elsewhere!
But not in all of mathematical logic? They are used in proof theory. Where else?
HallsofIvy
May31-09, 03:44 AM
Precisely what do you mean by "formal" proofs? The responders here may not mean the same thing you do.
Edgardo
May31-09, 04:47 AM
The December issue of Notices of the American Mathematical Society may be interesting for you:
http://www.ams.org/notices/200811/
Precisely what do you mean by "formal" proofs? The responders here may not mean the same thing you do.
I would mean the kind that most people (at least all the logicians) would regard as formal.
A formal proof or derivation is a finite sequence of sentences (called well-formed formulas in the case of a formal language) each of which is an axiom or follows from the preceding sentences in the sequence by a rule of inference. The last sentence in the sequence is a theorem of a formal system.
In other words where everything in the proof is 100% rigorous.
matt grime
May31-09, 10:27 AM
So you think all other mathematics is unrigorous and doesn't follow these rules?
HallsofIvy
May31-09, 11:00 AM
I would mean the kind that most people (at least all the logicians) would regard as formal.
A formal proof or derivation is a finite sequence of sentences (called well-formed formulas in the case of a formal language) each of which is an axiom or follows from the preceding sentences in the sequence by a rule of inference. The last sentence in the sequence is a theorem of a formal system.
In other words where everything in the proof is 100% rigorous.
That is NOT what "most people (at least all the logicians)" would consider "formal". For a logician, certainly, a "formal proof" would require much more than it be "100% rigorous".
A proof can be considered rigorous if all the reasoning used in it is justified, so that its conclusions necessarily follow from its assumptions--even if it is not a fully formal derivation. In an informal proof, a mathematician might use shortcuts like "so by X, we get..." and give the result, omitting some calculation. So long as a competent reader could do the calculation himself and get the same result without too much trouble, the proof can be considered "rigorous."
So you think all other mathematics is unrigorous and doesn't follow these rules?
All others are incomplete (non technical word). Incomplete might mean not giving derivations when it should.
I've mixed this notion of completeness into the word rigour. In fact this mixing is allowed if one is to add the word formal:
Formal rigour is the introduction of high degrees of completeness by means of a formal language where such proofs can be codified using set theories such as ZFC (see automated theorem proving).
http://en.wikipedia.org/wiki/Rigour
matt grime
Jun1-09, 02:17 AM
All others are incomplete (non technical word). Incomplete might mean not giving derivations when it should.
No (correct) proofs are incomplete, or they are not proofs. The proof of the theorem will follow from the hypotheses of the theorem. Whether or not the hypotheses are ever satisfied is essentially unimportant to whether or not the proof is rigorous.
Of course a writer may omit 'obvious' steps.
If you're going to assign personal meanings to words that are already quite flexible who knows what kind of answer you're going to get.
No one is going to prove much from the axioms of ZFC, since one only ever does maths in a model of ZFC (unless one is doing abstract set theory) where many theorems are true and can't be proven from the axioms, either because they do not follow from the axioms or because they're so far removed as to make its deduction practically impossible.
Of course a writer may omit 'obvious' steps.
That's what I meant by saying a proof is incomplete.
I assume that when you say some theorem cannot be proven from ZFC it's because extra axioms are needed.
matt grime
Jun1-09, 01:42 PM
The proof is not incomplete - the reader is supposed to do the steps to verify it.
The axioms of ZFC are very weak, in some sense. You cannot prove a lot directly from them: they don't even assert that the real numbers exist, so you're not going to deduce any analysis from them even. ZFC doesn't even imply the existence of an uncountable set (Skolem's paradox states something like any finitely axiomatized system has a countable model). You must know of Goedel's theorem as well.
The proof is not incomplete - the reader is supposed to do the steps to verify it.
The axioms of ZFC are very weak, in some sense. You cannot prove a lot directly from them: they don't even assert that the real numbers exist, so you're not going to deduce any analysis from them even.False.
ZFC doesn't even imply the existence of an uncountable set (Skolem's paradox states something like any finitely axiomatized system has a countable model).Of course they do. For example, the powerset of N is uncountable, because P(X) is always larger than X.
matt grime
Jun1-09, 03:49 PM
Oh boy. Did you even look up Skolem's paradox? All that ZFC implies is that there is no bijection between P(N) and N, where we take N to be the inductive set that ZFC states exists. Note that this requires you to define the power set (ZFC doesn't say what it is) and also note that all we can say is that there is no bijective function from P(N) into N in that model. That is not the same as stating that there is no bijection in any model at all. "Larger" is also a completely undefined term in your post too.
Oh boy. Did you even look up Skolem's paradox?No, I didn't, because I am familiar with it. It is a theorem of ZFC that there are uncountable sets. What Skolem's paradox is about is the fact that countability is not absolute, not about the fact that ZFC doesn't prove the existence of an uncountable set. It basically says that given any model A of ZFC, you can (within A) find a model B of ZFC which is countable (within A, i.e. there is a bijection in A between B and N). The paradox lies in the fact that B is nonetheless not countable with respect to itself, i.e. there is no bijection in B between B and the set N' of naturals in B. It doesn't say that ZFC doesn't prove the existence of uncountable sets. On the contrary, it is inconsistent with ZFC to assume that there are no uncountable sets.
You very directly and explicitly said that "ZFC doesn't even imply the existence of an uncountable set". That's unambiguously false, it is a theorem of ZFC that there is an uncountable set.
All that ZFC implies is that there is no bijection between P(N) and N, where we take N to be the inductive set that ZFC states exists.Yes, that's what uncountability means.
Note that this requires you to define the power set (ZFC doesn't say what it is)The power set of X is a set P such that for every Y, Y is a member of P iff Y is a subset of X, i.e. iff every member of Y is a member of X. That's the definition used in the axiom of the power set.
and also note that all we can say is that there is no bijective function from P(N) into N in that model.Yes. Once again, that's what uncountability means. If by the uncountability of a set x you mean something other than the existence of a set f such that f is a bijection between x and omega, the intersection of all inductive sets, you're misusing the term.
That is not the same as stating that there is no bijection in any model at all.Yes, if one model, A, is embedded in another, B, it may happen that A is B-countable. How does that demonstrate that ZFC doesn't prove the existence of uncountable sets?
"Larger" is also a completely undefined term in your post too."Larger" means the same thing it means anywhere in set theory, i.e. there is an injection from x to y but not from y to x.
matt grime
Jun1-09, 04:23 PM
I think we have different ideas of what counts as 'countable'. Mine, not being a set theorist and therefore probably being the completely wrong one, is not one intrinsic to the model, but to the 'standard' model that everyone uses. I am not denying there is no bijection between N and P(N) within a model, clearly. However, my point was really about the real numbers - there will be some model without something that looks like what we consider to be the real numbers.
I see. Well, as long as we understand each other...
(Actually, even if you pick a particular model, or rather class of models, as standard and by "countability" you mean countability-in-the-standard-model, you're still forced to conclude that there are uncountable sets in that sense. From this POV the most you can say is that there are non-standard models which are standardly countable, not that there are no standardly countable sets - but I think if one has the perspective that set theory is about "the" standard model, then they probably wouldn't be worried about the non-standard models, anyway. You get the counter-intuitive results only if you mix the two perspectives.)
In which fields of maths are formal proofs used often?
What do you mean exactly by the word "used" in your question?
There are tens of thousands of proofs in various areas of mathematics written in various formal proof languages. Is your question about which area of mathematics those proofs belong to most often? Is such case the answer is probably Analysis.
Or maybe you are asking this question:
"If I was to specialize in certain field of mathematics, in which field I have the greatest chance to learn and be required to write formal proofs?"
In such case there is no good answer because this chance is practically zero no matter which field of mathematics you choose (except perhaps proof theory or logic). Math departments don't teach writing formal proofs (if you know a class that is offered regularly that teaches a formal proof language please let me know). Classes on formalized mathematics are offered by computing science and philosophy departments.
What do you mean exactly by the word "used" in your question?
There are tens of thousands of proofs in various areas of mathematics written in various formal proof languages. Is your question about which area of mathematics those proofs belong to most often? Is such case the answer is probably Analysis.
Or maybe you are asking this question:
"If I was to specialize in certain field of mathematics, in which field I have the greatest chance to learn and be required to write formal proofs?"
In such case there is no good answer because this chance is practically zero no matter which field of mathematics you choose (except perhaps proof theory or logic). Math departments don't teach writing formal proofs (if you know a class that is offered regularly that teaches a formal proof language please let me know). Classes on formalized mathematics are offered by computing science and philosophy departments.
Probably 'used' in the latter sense. Formal proofs would be used extensively in proof theory since they would be the main object of study. But which other logic area would use proof theory.
Why would analysis recquire the most amount of formal proofs?
Why would analysis recquire the most amount of formal proofs?
It's not that analysis requires formal proofs in any sense, rather it is close enough to foundations and popular and known enough that people doing mathematics in formalized form tend to choose it as the subject for their work (hobby?).
Subjects that are close to foundations are easier to formalize. For example, general topology is much easier than, say, calculus, or differential equations. So which subjects tend to be formalized is a balance of ease and popularity, or perceived importance.
Of course a writer may omit 'obvious' steps.
What is obvious to one isn't to another. So the next time I don't understand a proof, I can just say that not enough steps were filled. So the blame is on the author and not myself.
evagelos
Jun6-09, 09:28 PM
In which fields of maths are formal proofs used often?
IN every mathematical field provided you know how to do it
evagelos
Jun6-09, 09:30 PM
i would mean the kind that most people (at least all the logicians) would regard as formal.
A formal proof or derivation is a finite sequence of sentences (called well-formed formulas in the case of a formal language) each of which is an axiom or follows from the preceding sentences in the sequence by a rule of inference. The last sentence in the sequence is a theorem of a formal system.
In other words where everything in the proof is 100% rigorous.
correct
Dragonfall
Jun7-09, 12:17 AM
Like others have said, in practice, formal proofs (in the sense of a proof verifiable by an automatic proof checker) are not used anywhere, except possibly in the subject of automated theorem proving and foundations.
What is obvious to one isn't to another. So the next time I don't understand a proof, I can just say that not enough steps were filled. So the blame is on the author and not myself.
The author isn't there to spoon-feed the readers. If the reader is unable to fill in the steps, the blame lies with her. The author is mainly concerned with the correctness of a proof. Usually experience will determine where a gap in logic is considered "trivial" and where it is not.
vBulletin® v3.7.6, Copyright ©2000-2009, Jelsoft Enterprises Ltd.