Library hydras.Ackermann.wConsistent

From hydras.Ackermann Require Import folProof folProp LNN.
From Coq Require Import Arith List.

Import NNnotations.

Definition wConsistent (T : System) :=
  ∀ (f : Formula) (v : nat),
  (∀ x : nat, In x (freeVarF f) → v = x) →
  SysPrf T (existH v (notH f)) →
  ∃ n : nat, ¬ SysPrf T (substF f v (natToTerm n)).

Lemma wCon2Con : ∀ T : System, wConsistent T → Consistent LNN T.

Definition wInconsistent (T : System) :=
  ∃ f : Formula,
    (∃ v : nat,
       (∀ x : nat, In x (freeVarF f) → v = x) ∧
       SysPrf T (existH v (notH f)) ∧
       (∀ n : nat, SysPrf T (substF f v (natToTerm n)))).

Lemma notCon2wNotCon :
 ∀ T : System, Inconsistent LNN T → wInconsistent T.