My Math Forum  

Go Back   My Math Forum > Math Forums > Math

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


Thanks Tree3Thanks
Reply
 
LinkBack Thread Tools Display Modes
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.
RohitRanjan is offline  
 
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.
Thanks from Rishabh
Evgeny.Makarov is offline  
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:
  1. clearlly state all assumptions and conditions under which your result applies;
  2. clearly state the result that the assumptions and conditions lead to;
  3. work through the proof stating at each step what assumptions, conditions, or other theorems you are using for that step.
  4. 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
v8archie is offline  
June 7th, 2014, 10:03 AM   #4
Senior Member
 
raul21's Avatar
 
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 View Post
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.
raul21 is offline  
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?
Evgeny.Makarov is offline  
June 7th, 2014, 11:06 AM   #6
Senior Member
 
raul21's Avatar
 
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.
raul21 is offline  
June 7th, 2014, 11:28 AM   #7
Senior Member
 
Joined: Dec 2013
From: Russia

Posts: 327
Thanks: 108

Quote:
Originally Posted by raul21 View Post
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.
Thanks from raul21
Evgeny.Makarov is offline  
June 7th, 2014, 11:45 AM   #8
Senior Member
 
raul21's Avatar
 
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 View Post
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?
raul21 is offline  
June 7th, 2014, 11:54 AM   #9
Senior Member
 
Joined: Dec 2013
From: Russia

Posts: 327
Thanks: 108

Quote:
Originally Posted by raul21 View Post
What was I thinking? Continuum hypothesis!
What's your point?

Quote:
Originally Posted by raul21 View Post
Your 1st sentence is a loose form of Godel's incompleteness theorem?
Yes.
Evgeny.Makarov is offline  
June 7th, 2014, 01:12 PM   #10
Senior Member
 
raul21's Avatar
 
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 View Post
What's your point?
CH can't be derived from ZF (Cohen), nor its negation (Godel).
raul21 is offline  
Reply

  My Math Forum > Math Forums > Math

Tags
formal, proof



Thread Tools
Display Modes


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





Copyright © 2019 My Math Forum. All rights reserved.