# How to construct a proof for 0x1 = 0

• May 21st 2011, 04:57 PM
ikurwae89
How to construct a proof for 0x1 = 0
i want to construct a proof for 0 x 1 = 0 in first order system.

i know i need to prove first 0x1 = ((0x0)+0) and (((0x0)+0)=(0x0) but how?

can you show me the proof with reasons?

thanks
• May 21st 2011, 06:21 PM
emakarov
Quote:

i want to construct a proof for 0 x 1 = 0 in first order system.
Are you talking about first order Peano Arithmetic? If so, this is usually a special case of one of the axioms.

If your axioms have recursion on the second argument, as in the link above, then

0 x S(0) = 0 x 0 + 0 (by the second multiplication axiom)
= 0 + 0 (since 0 x 0 = 0 by the first multiplication axiom)
= 0 (by the first addition axiom)
• May 21st 2011, 07:46 PM
ikurwae89
no we dont have that. we normally prove it via intital sequents and rules of inference. yes its peano arithmetic.
• May 22nd 2011, 02:32 AM
HallsofIvy
Then what is the definition of multiplication in your system?

What I am used to is that
1) 0(b)= 0 for all b
2) if a is not 0 then there exist c such that a= s(c) and then a(b)= c(b)+ b

Obviously 0(1)= 0 is just an application of the first rule. Apparently you are not using that definition and obviously we cannot suggest any proof involving multiplication until we know what definition you are using.
• May 22nd 2011, 09:36 AM
emakarov
Quote:

Originally Posted by ikurwae89
no we dont have that. we normally prove it via intital sequents and rules of inference. yes its peano arithmetic.

I agree with HallsofIvy that you need the definition of multiplication somehow (such as Peano axioms). After that, the proof depends on the proof calculus (sequent calculus, natural deduction, etc). Strictly speaking, it is probably not a sequence of equations but a tree, say, of sequents, but the only inference rules that are needed here seem to be the rule of equality and universal elimination (to get specific instances of axioms).

• May 23rd 2011, 03:00 AM
ikurwae89
well i need to construct the proof for the theorem (( 0 x 1 = 0 ) using first order peano arithmetic.

i normally start the proof with an initial sequent i.e

{ (v1 x v2) } : (v1 x v2) and so on.. until i arrive at 0 x 1 = 0..

hmm the link u gave me are axioms that we are using.
• May 23rd 2011, 03:17 AM
emakarov
Quote:

{ (v1 x v2) } : (v1 x v2)
Do you mean that { (v1 x v2) } is the set of premises of the sequent and v1 x v2 is the conclusion of the sequent? And does x denote multiplication? If yes, then v1 x v2 is not a formula, but a term.

What proof calculus are you using: natural deduction, sequent calculus, or something else? What is the inference rule dealing with equality?