Thread: 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

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)

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

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.

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

In any case, more details about your setting are needed.

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.

{ (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?