- #1
tgt
- 522
- 2
formal proofs, where...?
In which fields of maths are formal proofs used often?
In which fields of maths are formal proofs used often?
CRGreathouse said:Foundations of mathematics (logic). They're really not used elsewhere!
HallsofIvy said:Precisely what do you mean by "formal" proofs? The responders here may not mean the same thing you do.
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".tgt said: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 said:So you think all other mathematics is unrigorous and doesn't follow these rules?
tgt said:All others are incomplete (non technical word). Incomplete might mean not giving derivations when it should.
matt grime said:Of course a writer may omit 'obvious' steps.
False.matt grime said: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.
Of course they do. For example, the powerset of N is uncountable, because P(X) is always larger than X.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).
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.matt grime said:Oh boy. Did you even look up Skolem's paradox?
Yes, that's what uncountability means.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.
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.Note that this requires you to define the power set (ZFC doesn't say what it is)
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.and also note that all we can say is that there is no bijective function from P(N) into N in that model.
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?That is not the same as stating that there is no bijection in any model at all.
"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."Larger" is also a completely undefined term in your post too.
In which fields of maths are formal proofs used often?
slawekk said: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.
Why would analysis recquire the most amount of formal proofs?
matt grime said:Of course a writer may omit 'obvious' steps.
tgt said:In which fields of maths are formal proofs used often?
tgt said: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.
tgt said: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.
A formal proof is a rigorous and systematic method of demonstrating the validity of a mathematical argument. It involves using a set of predefined rules and axioms to logically deduce the truth of a statement.
Formal proofs ensure the correctness of mathematical arguments by using a structured and logical approach, which eliminates any possibility of error or ambiguity. By following a set of rules and axioms, each step of the proof is carefully checked and verified, leading to a logically sound conclusion.
Using formal proofs provides several benefits, such as ensuring the validity of mathematical arguments, allowing for a clear and concise presentation of complex ideas, and providing a foundation for further mathematical research and discoveries.
Yes, formal proofs can be used in all areas of mathematics, from basic arithmetic to advanced topics such as abstract algebra and topology. In fact, formal proofs are essential in many branches of mathematics to prove theorems and establish new results.
No, there are other methods of ensuring the correctness of mathematical arguments, such as using empirical evidence or making intuitive arguments. However, formal proofs are considered the most rigorous and reliable method, especially in more complex mathematical concepts.