Построение индуктивных доказательств в формальной арифметике Пеано

Построение индуктивных доказательств в формальной арифметике Пеано

Докажем, что:

ЛЕММ1 (x * y) + x = x * s(y) (вариант 4)

ЛЕММ2 s(x) * y = x + (x * y) (вариант 8)

При

A: x + 0 = x

B: x + s(y) = s(x + y)

C: x * 0 = 0

D: x * s(y) = (x * y) + x

E: d(0) = 0

F: d(s(x)) = s(s(d(x)))

Докажем aссоциативность произведения:

АССП: x * y = y * x

Для этого докажем леммы:

ЛЕММ3: x * 0 = 0 * x

ЛЕММ4: s(0) * x = x

ЛЕММ5: s(x) * y = y + (x * y)

ЛЕММ3: x * 0 = 0 * x

P(0): 0 * 0 = 0 * 0 =[C..C]= 0 : 0

P(s(x)): s(x) * 0 = 0 * s(x)

Левая часть: s(x) * 0 =[c:x=s(x)]= 0

Правая часть: 0 * s(x) =[D:x=0,y=x]= (0 * x) + 0 =[ИП]= (x * 0) + 0 =[A:x=(x * 0)]= x * 0 =[C:x=x] = 0 = ПЧ

ЛЕММ4: s(0) * x = x

P(0) = (s(0) * 0 = 0)

Левая часть: s(0) * 0 =[C:x=s(0)]= 0 = ПЧ

P(s(x)) = (s(0) * s(x) = s(x))

Левая часть: s(0) * s(x) =[D:x=s(0),y=x]= (s(0) * x) + s(0) =[B:x=(s(0) * x),y=0]= s((s(0) * x) + 0) =[A:x=(s(0) * x),y=0]= s(s(0) * x) =[ИП]= s(x) = ПЧ

ЛЕММ5: s(x) * y = y + (x * y)

В качестве подстановочного символа возьмем y

АСС - ассоциативность сложения

P(0): s(x) * 0 = 0 + (x * 0)

Левая часть: s(x) * 0 =[ЛЕММ4]= 0

Правая часть: 0 + (x * 0) =[АСС]= (x * 0) + 0 =[A:x=(x * 0)]= x * 0 =[C:x=x]= 0 = ЛЧ

P(s(y)): s(x) * s(y) = s(y) + (x * s(y))