Library hydras.Ackermann.prLogic

prLogic.v

Original script by Russel O'Connor

Although this module doesn't depend on FOL, the following lemmas are JUST helpers to prove that the encoding of basic FOL connectives are PR

From hydras.Ackermann Require Import primRec code cPair.
From Coq Require Import Arith.

Lemma codeForallIsPR : isPR 2 (fun a b : nat ⇒ cPair 3 (cPair a b)).

#[export] Instance codeNotIsPR : isPR 1 codeNot.

#[export] Instance codeImpIsPR : isPR 2 codeImp.