Инъективность наследника натуральных чисел в Coq

Question

Меня немного смущает, является ли инъективность функции-преемника, определенной на натуральных числах в Coq, аксиомой? Согласно аксиомам Википедии / Пеано , это аксиома (7). Когда я смотрю на справочную страницу Coq.Init.Peano , я вижу следующее:

Определение eq_add_S n m (H: S n = S m): n = m: = f_equal pred H.

Подсказка Немедленно eq_add_S: core.

и это похоже на аксиому (?), Но меня смутило то, что в верхней части этой страницы написано:

В нем изложены различные леммы и теоремы о натуральных числах, включая аксиомы арифметики Пеано (в Coq это доказуемо)

Это предложение немного двусмысленно, нет?

Answer 1

Команда, которую вы видели, на самом деле является доказательством инъективности конструктора S.Точнее, в нем говорится, что функция-наследник является инъективной, потому что она имеет обратное значение: функция-предшественник (pred).(В Coq аксиомы обычно вводятся с ключевым словом Axiom.)

Вас, кажется, смущает то, что я считаю двумя связанными значениями слова "аксиома".Более широкий смысл в логике - это «отправная точка рассуждения» ( Wikipedia ).Более узкий смысл - это утверждение, которое считается само собой разумеющимся в дедуктивной системе без дополнительных доказательств.В арифметике Пеано аксиомы Пеано являются аксиомами в обоих смыслах слова, поскольку они примитивны.В Coq, теории множеств ZFC и других системах их можно доказать из более элементарных фактов.