Library hydras.Ackermann.NN2PA

NN2PA.v :

Original version by Russel O'Connor

From Coq Require Import Ensembles List Arith.

From hydras.Ackermann
  Require Import folProp folProof subProp folLogic3 folReplace NN
  PAtheory.
From hydras.Ackermann Require Export LNN2LNT.
From hydras.Ackermann Require Import subAll ListExt.
Import NNnotations.

Lemma NN2PA (f : fol.Formula LNN):
  folProof.SysPrf LNN NN f → SysPrf PA (LNN2LNT_formula f).

If F[x\0], F[x\1] ... F[x\m-1] are provable in PA, then v_x <' m → F is also provable (where a <' b is the translation of a < b into PA).

More precisely:

Lemma PAboundedLT :
  ∀ (m : nat) (F : LNT.Formula) (x : nat),
    (∀ n : nat,
        n < m → SysPrf PA (substF F x (natToTerm n))) →
    SysPrf PA (LNN2LNT_formula (v #x < LNN.natToTerm m)%fol → F)%nt.