Originally Posted by HallsofIvy
Once again, we return to the question, "What do you mean by 'formal proof'?"
|
The definition was given in another thread by
tgt and is the following:
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.
.
|
With the only difference that i may add:
each formula could be, apart from axiom, a theorem or definition
Originally Posted by HallsofIvy
I think you are just talking about the kind of proof you would find in a math paper or calculus book- far from what, say, logicians would mean by "formal proof". A true "formal proof" of such a thing would probably require an entire book! How many pages did Russel and Whitehead require to prove "1+ 1= 2"?
|
Go to pages 121 to 139 in ANGELO'S MARGARIS book :
FIRST ORDER MATHEMATICAL LOGIC.There you will find many true "formal proofs" not more than half a page long
You know how
many books you need before you double integrate a function ,or write a proof in analysis??
Originally Posted by HallsofIvy
Another question: what algebraic system are you working in? The proof for an abstract ring or integral domain would be quite different than for the real numbers.
MXSCNT's point is that the only good reason for doing such "fiddly" stuff is practise: homework.
|
On the following axiomatic system i will base any formal or rigorous proofs:
The primitive symbols are:
= for equality
+ for addition
. for multiplication
- for the inverse in addition
0 constant
1 constant
/ for inverse in multiplication

AND the axioms are:
1)
2)
3)
4)
![LaTeX Code: \\forall a[ a+(-a) = 0]..........\\forall a[ a\\neq 0\\Longrightarrow a.\\frac{1}{a} = 1]<BR>](latex_images/22/2228019-4.png)
.
5)
AND now the rigorous proof of (-1)x = -x
(-1)x = (-1)x + 0 =................................................. ............by axiom 3 (for addition)
=(-1)x +[ x + (-x)]=................................................. ............by axiom 4 (for addition)
=[(-1)x +x] + (-x) =................................................. ............by axiom 2 (for addition)
=[(-1)x + 1x] + (-x)=............................................... ..............by axiom 3 (for multiplication)
=[x.1 + x(-1)] + (-x)=............................................... .............by axiom 1 ( for addition and multiplication)
=[ x( 1 + (-1))] + (-x)=............................................... ..........by axiom 5
= x.0 + (-x) = .................................................. ....................by axiom 4 (for addition)
= 0 + (-x) =................................................. ......................by the theorem 0.x = 0
= -x .................................................. ............................by axiom 4 (for addition)
Next post the formal proof