Теория (абелевых) групп

Теория групп G — это прикладное исчисление предикатов с равенством, в котором имеются:

1. Предметная константа 0.

2. Двухместный функтор +.

3. Собственные аксиомы (схемы аксиом):

G ₁: х, у, z x+(y+z) = (х+у)+z,

G ₂: х 0 + х = х,

G₃: х у х+у = 0.

Выражение «теория первого порядка с равенством» означает, что подразумевается наличие преди­ката =, аксиом Е ₁ и E ₂ и всех их следствий.

Группа называется абелевой, если имеет место собственная аксиома

G ₄: х, у х+у = у+х.

Абелева группа называется группой конечного порядка п, если выполнена собственная аксиома

G ₅: х k n kx = 0, где kx — это сокращение для х +х + • • • + х (k слагаемых).

Эта формула не является формулой теории G, поскольку содержит «посторонние» предметные предикаты и переменные. Однако для любого конкретного конечного п собственная аксиома мо­жет быть записана в виде допустимой формулы теории G:

: х (x = 0 2 x = 0 ... nx = 0).

Абелева группа называется полной, если выполнена собст­венная аксиома

G ₆: n 1 х y пу = х.

Эта формула не является формулой теории G, поскольку содержит «посторонние» предметные константы и переменные. Однако собственная аксиома может быть записана в виде бесконечного множества допустимых формул теории G:

: х y 2y = х, х y Зу = х

Но любое конечное множество формул, истинное во всех полных абелевых группах, истинно и в некоторой неполной абелевой группе, то есть теория полных абелевых групп не является конечно аксиоматизируемой.

Абелева группа называется периодической, если выполнена собственная аксиома

G ₇: х n 1 пх = 0.

Эта формула не является формулой теории G поскольку содержит «посторонние» предмет­ные константы и переменные. Если попытаться преобразовать формулу G ₇ по образцу фор­мулы G ₅,то получится бесконечная «формула»

: х (х = 0 2 x = 0 ... пх = 0 ...),

которая не является допустимой формулой исчисления предикатов и, тем более, теории G. Таким образом, периодическая абелева группа не является аксиоматизируемой (если не включать в теорию групп и всю формальную арифметику).

Наличие неаксиоматизируемых и конечно неаксиоматизируемых формальных теорий не означает практической неприменимости аксиоматического метода. Это означает, что аксиоматический ме­тод не применим «в чистом виде». На практике формальные теории, описывающие содержатель­ные объекты, задаются с помощью собственных аксиом, которые наряду с собственными предика­тами и функторами содержат «внелогические» предикаты и функторы, свойства которых аксио­мами не описываются, а считаются известными (в данной теории). В рассмотренных примерах подраздела 4.4. внелогическими являются натуральные числа и операции над ними. Аналогич­ное обстоятельство имеет место и в некоторых системах логического программирования (например, Пролог). Реали­зация такой системы всегда снабжается обширной библиотекой внелогических (или встроенных) предикатов и функторов, которые и обеспечивают практическую применимость системы логиче­ского программирования.