# Formal proofs, where ?

1. May 30, 2009

### tgt

formal proofs, where....?

In which fields of maths are formal proofs used often?

2. May 30, 2009

### CRGreathouse

Re: formal proofs, where....?

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

3. May 30, 2009

### mXSCNT

Re: formal proofs, where....?

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. May 30, 2009

### tgt

Re: formal proofs, where....?

But not in all of mathematical logic? They are used in proof theory. Where else?

5. May 31, 2009

### HallsofIvy

Re: formal proofs, where....?

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

6. May 31, 2009

### Edgardo

7. May 31, 2009

### tgt

Re: formal proofs, where....?

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. May 31, 2009

### matt grime

Re: formal proofs, where....?

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

9. May 31, 2009

### HallsofIvy

Re: formal proofs, where....?

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. May 31, 2009

### mXSCNT

Re: formal proofs, where....?

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. Jun 1, 2009

### tgt

Re: formal proofs, where....?

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. Jun 1, 2009

### matt grime

Re: formal proofs, where....?

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. Jun 1, 2009

### tgt

Re: formal proofs, where....?

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. Jun 1, 2009

### matt grime

Re: formal proofs, where....?

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. Jun 1, 2009

### Preno

Re: formal proofs, where....?

False.
Of course they do. For example, the powerset of N is uncountable, because P(X) is always larger than X.

16. Jun 1, 2009

### matt grime

Re: formal proofs, where....?

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. Jun 1, 2009

### Preno

Re: formal proofs, where....?

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.
Yes, that's what uncountability means.
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.
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.
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" 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: Jun 1, 2009
18. Jun 1, 2009

### matt grime

Re: formal proofs, where....?

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: Jun 1, 2009
19. Jun 1, 2009

### Preno

Re: formal proofs, where....?

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. Jun 2, 2009

### slawekk

Re: formal proofs, where....?

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.

Know someone interested in this topic? Share this thread via Reddit, Google+, Twitter, or Facebook