У Барвайса на с.49 [СКпМЛ,т.I] сказано так "Многие логики считают, что нет логики, кроме логики первого порядка, в том смысле, что если попытаться сделать все математические (внелогические) предположения явными, то эти аксиомы могли бы быть выражены в логике первого порядка и что неформальное понятие доказуемости, используемое в математике, в точности превратилось бы в формальное понятие доказуемости в логике первого порядка."
Однако на с.15 в разделе "Теория групп" читаем: "Понятия (d) [полная группа] и (e) [группа без кручения] требуют бесконечного списка аксиом. Последнее понятие (f) [периодическая группа] не является понятием логики первого порядка. Посмотрим почему."
А мы посмотрим более простой вопрос: как же так?
На примере полной [абелевой] группы (ПАГ).
Чтобы записать аксиому ПАГ там же с.15 в язык вводятся натуральные числа и операция не удостоившаяся даже значка: nx, разъясняемая как чисто синтаксическая: x+...+x (n раз x), т.е. имеется в виду что формула (6) может быть записана и без квантора по натуральным числам и натуральной переменной n, правда тогда (6) превратится в "схему" аксиом (порождающую счётное множество конкретных аксиом) либо в бесконечную формулу.
И появляется аксиома:
∀n≥1∀x∃y ny=x. (6)
Если (6) понимать как схему аксиом, то (см. с.16) для каждого n>1 надо породить аксиому
∀x∃y ny=x. (6n)
где n уже однозначно трактуется "синтаксически": ny = y+...n+y (сложить n y).
На с.16 Предложение 2.1. звучит так "Любое конечное множество предложений [ЛПП], истинное во всех полных абелевых группах (d), истинно и в некоторой неполной абелевой группе."
И далее "Другими словами, понятие полной абелевой группы не является конечно аксиоматизируемым в логике первого порядка."! На с.18 приводится доказательство Предложения 2.1.
Чтобы понять что имеется в виду надо начать строить аксиоматическую теорию групп (АТГ). Группа G как описано на с.15 есть тройка: G - непустое множество, 0 - элемент G, + - функция отображающая любую пару элементов из G в G. Язык АТГ (само собой первого порядка) будет естественным образом содержать:
- 0 - константный символ;
- + - бинарная (инфиксная) операция.
Всего одна константа и одна функция и можно записать 4 главных аксиомы АТГ (предикат "=" является у Барвайса логическим символом и имеется в языке всегда):
(свободные переменные считаются связанными квантором ∀)
x+(y+z)=(x+y)+z (1)
x+0=x (2)
∃y x+y=0 (3)
x+y=y+x (4) коммутативная или абелева
Важно что язык для записи формул фиксирован и можно сказать родной самому понятию группы: 0 и само собой +:-)
Именно об этом конкретном языке первого порядка и идёт речь в Предложении 2.1.: именно в теории АТГ нельзя найти, подобрать... такое конечное множество формул чтобы они были эквивалентны (6)!
Но где-то есть такой вариант FOL (ну ЛПП) в котором - за милую душу! Неужели надо идти в ТМ (великую и могучую Теорию Множеств)?
По идее можно записать аксиому (6) в ТМ имея в виду что там есть конечные кардинальные числа - модель для натуральных чисел.
Понятие алгебраической системы (АС) целиком и полностью из теории множеств. Так и группа G как и всякая АС [АС], с.46 есть <G,ΩF,ΩP>, т.е. состоит из основного множества, множества операций и множества предикатов. В случае группы ΩF={Zero0, Add2}, где индекс указывает арность операции, а "Значения главных нульарных операций системы называются главными или выделенными элементами этом системы". Ну а ΩP для группы пусто. При этом В ТМ Add есть конечно множество - график функции, т.е. подмножество декартова произведения GxGxG, полное по первым двум компонентам и функциональное по третьей (эти требования можно записать в ТМ, а для применения такого графика есть ТМ функция - ‘ (будем считать что это английская одинарная кавычка - Alt+0145) [Менд], с.187).
Замечание. Немного проще но в духе ТМ и АС можно считать, что группа G есть 3-ка <G,Zero,Add>, где
- Zero∈G,
- Add ⊆ GxGxG, такое что: полно по первым двум местам (проекция даёт GxG), функционально по 3-ему месту. Главное показать что G задаваемо в ТМ.
И мы можем писать что-то вроде:
∀n∀x∃y ω≥n≥1 ∧ x∈G ∧ y∈G → n*y=x. (6)
...
Лучше считать естественное (непринуждённое;-) появление натуральных чисел в языке АТГ приглашением/необходимостью перейти к многосортным языкам, что кстати с точки зрения АС как моделей для аксиом соответствующих теорий приводит к многоосновным АС (МАС) в которых одной из основ будет множество натуральных чисел.
Итак вводим два сорта: G для элементов группы и N для натуральных чисел. Теперь 0 - константа сорта G, а сортность "+" будет G G:G. Для примера аксиома (2) теперь будет так
∀x:G x+0=x (2мс)
А (6) так
∀n:N∀x:G∃y:G n≥1 → n*y=x. (6мс)
Важно (и очень:-) что это вполне себе формула первого порядка так что мы в FOL, просто она многосортная;-)
Правда нам ещё надо определить функцию "*", коя оказывается рекурсивной:
Сначала мы её объявляем и добавляем ей инфикс.
Declaration Mult N G:G. Add infix "*" to Mult.
Затем определяем.
Definition Mult(n y) if(n=1 return(y)) ; return(Mult(n-1 y)+y).
Функция определяется рекурсивно операторным выражением довольно простого типа. И это выражение вычисляется на модели аналогично тому как вычисляется значение терма, т.е. операторное выражение требует доопределения функции интерпретации:
- оператор ";" подразумевает: выполни левый операнд, а за тем правый.
- оператор if от двух параметров - выполни второй параметр если выполнено условие иначе просто верни управление.
- оператор return - вычисли терм и верни его результат как результат всего операторного выражения.
Отдельный вопрос - что нам понадобилось от натуральных чисел? Возможно это куда меньше чем полная арифметика и может быть аксиоматизировано отдельно?
А понадобилось: 1, ≥, -1.
Замечание. Последнее понадобившееся (-1) можно считать унарной операцией взятия предыдущего. И на вскидку мы имеем/используем структуру полного порядка с минимальным элементом (1), предикатом ≥, и унарной (частичной;-) операцией -1.
[СКпМЛ] Справочная книга по математической логике. Тт. I-IV. М., Наука, ГР Ф-МЛ, 1982-83.
[АС] А.И. Мальцев. Алгебраические системы. М., Наука, ГР Ф-МЛ, 1970.
[Менд] Э. Мендельсон. Ввведение в математическую логику. М., Наука, ГР Ф-МЛ, 1976.