My Math Forum > Math A formal proof

 Math General Math Forum - For general math related discussion and news

 May 31st, 2014, 03:59 AM #1 Newbie   Joined: May 2014 From: india Posts: 3 Thanks: 0 Math Focus: Algebra A formal proof What is the formal way of writing a proof?Please, Help me out.
May 31st, 2014, 05:02 AM   #2
Senior Member

Joined: Dec 2013
From: Russia

Posts: 327
Thanks: 108

Quote:
 What is the formal way of writing a proof?
The formal way of writing is when you are wearing a suit and tie. Concerning a formal proof, this phrase has two meaning. One is "an extremely detailed proof", and the second is "an object built according to specific rules in a certain logical calculus". The first type of proofs are written by people for people, and "formal" means that it is much more detailed than usually. It is still somewhat arbitrary. The second type of proof is a mathematical object. In practice, it is used mostly when a proof is explained to or constructed by a computer because it is difficult to work with large syntactic objects by hand.

Formal proofs in the second sense require specifying a logical calculus (formal system, or formalism). Just like a program computing a certain mathematical function can be written in different programming languages resulting in different source codes, a proof of the same statement can be written in different logical calculi resulting in different syntactic objects (for example, trees of formulas or sequences of formulas).

For more, you can read these Wikipedia articles: Formal proof (it deals with sequences of formulas, but that's not the only option), Hilbert system and Natural deduction.

 May 31st, 2014, 05:23 AM #3 Math Team   Joined: Dec 2013 From: Colombia Posts: 7,685 Thanks: 2665 Math Focus: Mainly analysis and algebra My idea of the more linguistic formal proof is:clearlly state all assumptions and conditions under which your result applies; clearly state the result that the assumptions and conditions lead to; work through the proof stating at each step what assumptions, conditions, or other theorems you are using for that step. explicity state that you have reached the end of the proof. This could be as simple as 'as required' after the last line of derivation, or it might involve explicitly highlighting a contradiction and stating the assumption that is thus proved false. Thanks from Rishabh
June 7th, 2014, 10:03 AM   #4
Senior Member

Joined: Apr 2014
From: zagreb, croatia

Posts: 234
Thanks: 33

Math Focus: philosophy/found of math, metamath, logic, set/category/order/number theory, algebra, topology
Quote:
 Originally Posted by Evgeny.Makarov The formal way of writing is when you are wearing a suit and tie. Concerning a formal proof, this phrase has two meaning. One is "an extremely detailed proof", and the second is "an object built according to specific rules in a certain logical calculus". The first type of proofs are written by people for people, and "formal" means that it is much more detailed than usually. It is still somewhat arbitrary. The second type of proof is a mathematical object. In practice, it is used mostly when a proof is explained to or constructed by a computer because it is difficult to work with large syntactic objects by hand. Formal proofs in the second sense require specifying a logical calculus (formal system, or formalism). Just like a program computing a certain mathematical function can be written in different programming languages resulting in different source codes, a proof of the same statement can be written in different logical calculi resulting in different syntactic objects (for example, trees of formulas or sequences of formulas). For more, you can read these Wikipedia articles: Formal proof (it deals with sequences of formulas, but that's not the only option), Hilbert system and Natural deduction.

You make a statement. I think for any statement in math, it can be concluded from 8(9) axioms of ZF(C)-Zermelo-Fraenkel axioms in a finite number of steps whether it's true or not. At least Hilbert wanted it. But Godel say no. Gentzen also says something. C marks axiom of choice-it's a crucial one, you get DISASTERS in topology without it.

 June 7th, 2014, 10:32 AM #5 Senior Member   Joined: Dec 2013 From: Russia Posts: 327 Thanks: 108 Raul, what's your point? And who is C?
 June 7th, 2014, 11:06 AM #6 Senior Member     Joined: Apr 2014 From: zagreb, croatia Posts: 234 Thanks: 33 Math Focus: philosophy/found of math, metamath, logic, set/category/order/number theory, algebra, topology Is my 2nd sentence true? C is axiom of choice.
June 7th, 2014, 11:28 AM   #7
Senior Member

Joined: Dec 2013
From: Russia

Posts: 327
Thanks: 108

Quote:
 Originally Posted by raul21 Is my 2nd sentence true?
No, any rich logical calculus has statements that it can neither prove nor refute. But, as far as I know, hunting for new axioms to be able to prove interesting results has not been a problem. Existing axioms are sufficient for almost everything so far. A more interesting problem for me is making work with formal calculi convenient and practical, not requiring significantly more effort than writing and reading paper proofs.

June 7th, 2014, 11:45 AM   #8
Senior Member

Joined: Apr 2014
From: zagreb, croatia

Posts: 234
Thanks: 33

Math Focus: philosophy/found of math, metamath, logic, set/category/order/number theory, algebra, topology
Quote:
 Originally Posted by Evgeny.Makarov No, any rich logical calculus has statements that it can neither prove nor refute. But, as far as I know, hunting for new axioms to be able to prove interesting results has not been a problem. Existing axioms are sufficient for almost everything so far. A more interesting problem for me is making work with formal calculi convenient and practical, not requiring significantly more effort than writing and reading paper proofs.
What was I thinking? Continuum hypothesis! Your 1st sentence is a loose form of Godel's incompleteness theorem?

June 7th, 2014, 11:54 AM   #9
Senior Member

Joined: Dec 2013
From: Russia

Posts: 327
Thanks: 108

Quote:
 Originally Posted by raul21 What was I thinking? Continuum hypothesis!

Quote:
 Originally Posted by raul21 Your 1st sentence is a loose form of Godel's incompleteness theorem?
Yes.

June 7th, 2014, 01:12 PM   #10
Senior Member

Joined: Apr 2014
From: zagreb, croatia

Posts: 234
Thanks: 33

Math Focus: philosophy/found of math, metamath, logic, set/category/order/number theory, algebra, topology
Quote:
 Originally Posted by Evgeny.Makarov What's your point?
CH can't be derived from ZF (Cohen), nor its negation (Godel).

 Tags formal, proof

 Thread Tools Display Modes Linear Mode

 Similar Threads Thread Thread Starter Forum Replies Last Post waqar-27 Applied Math 1 December 3rd, 2013 10:56 AM asifrahman1988 Calculus 1 March 17th, 2013 02:22 AM outsos Applied Math 0 July 29th, 2011 05:44 AM outsos Applied Math 3 May 27th, 2010 05:29 PM outsos Applied Math 2 May 26th, 2010 05:09 PM

 Contact - Home - Forums - Cryptocurrency Forum - Top