Library hydras.Ackermann.PA

From Coq Require Import Arith Lia Ensembles Decidable.
From hydras.Ackermann Require Import folProp subAll folLogic3.
From hydras.Ackermann Require Export Languages LNT.
From hydras.Ackermann Require Import NewNotations.

Section PA.

Definition PA1 := (allH 0, Succ v#0 ≠ Zero)%nt.

Definition PA2 := (allH 1 0, Succ v#0 = Succ v#1 → v#0 = v#1)%nt.

Definition PA3 := (allH 0, v#0 + Zero = v#0)%nt.

Definition PA4 := (allH 1 0, v#0 + Succ v#1 = Succ (v#0 + v#1))%nt.

Definition PA5 := (allH 0, v#0 × Zero = Zero)%nt.

Definition PA6 := (allH 1 0, v#0 × Succ v#1 = v#0 × v#1 + v#0)%nt.

Definition PA7 (f : Formula) (v : nat) : Formula :=
   let f_0 := substF f v Zero%nt in
   let f_Sv := substF f v (Succ v#v)%nt in
   close _ (f_0 → (allH v, f → f_Sv) → allH v, f)%nt.

Definition InductionSchema (f : Formula) : Prop :=
  ∃ g : Formula, (∃ v : nat, f = PA7 g v).

Definition PA := SetAdds InductionSchema PA1 PA2 PA3 PA4 PA5 PA6.

Definition open :=
  Formula_rec LNT (fun _ ⇒ Formula) (fun t t0 : Term ⇒ (t = t0)%nt)
    (fun (r : Relations LNT)
         (ts : Terms (arityR LNT r)) ⇒ atomic r ts)
    (fun (f : Formula) _ (f0 : Formula) _ ⇒ (f → f0)%nt)
    (fun (f : Formula) _ ⇒ (¬ f)%nt)
    (fun (n : nat) _ (recf : Formula) ⇒ recf).

Lemma PAdec : ∀ x : Formula, decidable (In _ PA x).

Lemma closedPA1 : ClosedSystem LNT PA.

Lemma closedPA : ∀ v : nat, ¬ In_freeVarSys LNT v PA.

Lemma pa1 (a : Term): SysPrf PA (Succ a ≠ Zero)%nt.

Lemma pa2 (a b : Term): SysPrf PA (Succ a = Succ b → a = b)%nt.

Lemma pa3 (a : Term): SysPrf PA (a + Zero = a)%nt.

Lemma pa4 ( a b : Term) : SysPrf PA (a + Succ b = Succ (a + b))%nt.

Lemma pa5 (a : Term): SysPrf PA (a × Zero = Zero)%nt.

Lemma pa6 (a b : Term) : SysPrf PA (a × Succ b = a × b + a)%nt.

Lemma induct (f : Formula) (v : nat):
  let f_0 := substF f v Zero
  in let f_Sv := substF f v (Succ (v#v))%nt
     in SysPrf PA f_0 →
         SysPrf PA (allH v, f → f_Sv)%nt
         → SysPrf PA (allH v, f)%nt.

End PA.