How do formal proofs ensure the correctness of mathematical arguments?

  • Thread starter tgt
  • Start date
  • Tags
    Proofs
In summary: 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.In summary, formal proofs are used in the fields of mathematics where they are considered to be 100% rigorous. They are also used in the fields of computer science, where they are used to verify computer programs, and in the AI field, where they are used to create expert systems.
  • #1
tgt
522
2
formal proofs, where...?

In which fields of maths are formal proofs used often?
 
Physics news on Phys.org
  • #2


Foundations of mathematics (logic). They're really not used elsewhere!
 
  • #3


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.
 
  • #4


CRGreathouse said:
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?
 
  • #5


Precisely what do you mean by "formal" proofs? The responders here may not mean the same thing you do.
 
  • #7


HallsofIvy said:
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.
 
  • #8


So you think all other mathematics is unrigorous and doesn't follow these rules?
 
  • #9


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.
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".
 
  • #10


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."
 
  • #11


matt grime said:
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
 
  • #12


tgt said:
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.
 
  • #13


matt grime said:
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.
 
  • #14


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.
 
  • #15


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.
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.
 
  • #16


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.
 
  • #17


matt grime said:
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.
 
Last edited:
  • #18


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.
 
Last edited:
  • #19


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.)
 
  • #20


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.
 
  • #21


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.

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?
 
  • #22


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.
 
  • #23


matt grime said:
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.
 
  • #24


tgt said:
In which fields of maths are formal proofs used often?

IN every mathematical field provided you know how to do it
 
  • #25


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.


correct
 
  • #26


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.

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.

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.
 
Last edited:

1. What is a formal proof?

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.

2. How do formal proofs ensure the correctness of mathematical arguments?

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.

3. What are the benefits of using formal proofs?

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.

4. Can formal proofs be used in all areas of mathematics?

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.

5. Are formal proofs the only way to ensure the correctness of mathematical arguments?

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.

Similar threads

  • Set Theory, Logic, Probability, Statistics
Replies
4
Views
435
  • Set Theory, Logic, Probability, Statistics
Replies
11
Views
394
  • Set Theory, Logic, Probability, Statistics
2
Replies
40
Views
6K
  • Set Theory, Logic, Probability, Statistics
Replies
3
Views
1K
  • Set Theory, Logic, Probability, Statistics
Replies
10
Views
1K
  • Set Theory, Logic, Probability, Statistics
Replies
4
Views
2K
  • Set Theory, Logic, Probability, Statistics
Replies
3
Views
2K
  • Set Theory, Logic, Probability, Statistics
Replies
1
Views
706
  • Set Theory, Logic, Probability, Statistics
Replies
5
Views
111
  • Set Theory, Logic, Probability, Statistics
Replies
1
Views
1K
Back
Top