Примеры описания содержательных проблем в РА

Аксиоматика натуральных чисел Пeaнo.

(формальная арифметика РА)

Алфавит.

А={0, S, +, , =, …} – конечное множество

0 – константа

S – одноместныйфункциональный символ; S(x) означает число, «следующее за x».

Функциональные +(x,y) x+y

символы (x,y) x y

Предикатный символ =(x,y) x=y

Математические аксиомы (содержательные) РА.

А1 → S(x)=0

A2 → S(x)=S(y) x=y (перед каждым числом одно предыдущее)

А3 → x+0=x

А4 → x+S(y)=S(x+y)

А5 → x 0 = 0

А6 → x S(y) = x y + x

А7 → x=x

А8 → x=y y=x

А9 → x=y (x=z y=z)

А10 → x₁=y₁& x₂=y₂&... &x_n=y_n f(x₁,..., x_n)=f(y₁,..., y_n)

А11 → x₁=y₁& x₂=y₂&... &x_n=y_n P(x₁,..., x_n)=P(y₁,..., y_n)

f - произвольный функциональный n-местный символ,

P- произвольный предикатный n-местный символ.

3. Содержательное правило вывода в РА: правило индукции

где y не входит свободно в Г и Δ

Примеры описания содержательных проблем в РА.

1). Теорема Евклида: для любых двух чисел существует НОД

"х"у (),

"х"у"z ( & ),

"х"у "z"u ( & ),