formal proofs, where....?

**tgt** · May30-09, 06:57 PM

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!

**mXSCNT** · May30-09, 08:59 PM

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.

**tgt** · May30-09, 10:37 PM

Originally Posted by CRGreathouse

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/

**tgt** · May31-09, 10:05 AM

Originally Posted by HallsofIvy

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

Originally Posted by tgt

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".

**mXSCNT** · May31-09, 10:51 PM

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."

**tgt** · Jun1-09, 01:06 AM

Originally Posted by matt grime

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

Originally Posted by tgt

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.

**tgt** · Jun1-09, 05:41 AM

Originally Posted by matt grime

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.

**Preno** · Jun1-09, 02:14 PM

Originally Posted by matt grime

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.