From Undecidability Require Import Shared.ListAutomation.
Import ListAutomationNotations.
From Undecidability Require Import FOL.Syntax.Core.
Import FullSyntax.
Export FullSyntax.

Local Set Implicit Arguments.

Section ND_def.

  Context {Σ_funcs : funcs_signature}.
  Context {Σ_preds : preds_signature}.

  Reserved Notation "A ⊢ phi" (at level 61).


  Implicit Type p : peirce.
  Implicit Type ff : falsity_flag.

  Inductive prv : (ff : falsity_flag) (p : peirce), list form form Prop :=
  | II {ff} {p} A phi psi : ::A A
  | IE {ff} {p} A phi psi : A A A
  | AllI {ff} {p} A phi : map (subst_form ) A A
  | AllE {ff} {p} A t phi : A A [t..]
  | ExI {ff} {p} A t phi : A [t..] A
  | ExE {ff} {p} A phi psi : A ::(map (subst_form ) A) [] A
  | Exp {p} A phi : prv p A falsity prv p A
  | Ctx {ff} {p} A phi : A A
  | CI {ff} {p} A phi psi : A A A
  | CE1 {ff} {p} A phi psi : A A
  | CE2 {ff} {p} A phi psi : A A
  | DI1 {ff} {p} A phi psi : A A
  | DI2 {ff} {p} A phi psi : A A
  | DE {ff} {p} A phi psi theta : A ::A ::A A
  | Pc {ff} A phi psi : prv class A ((( ) ) )
  where "A ⊢ phi" := (prv _ A ).

  Definition tprv `{falsity_flag} `{peirce} (T : form Prop) phi :=
     A, ( psi, A T ) A .

End ND_def.

Arguments ExI {_} {_} {_} {_} {A} t {}.

Arguments prv {_ _ _ _} _ _.
Notation "A ⊢ phi" := (prv A ) (at level 55).
Notation "A ⊢C phi" := (@prv _ _ _ class A ) (at level 55).
Notation "A ⊢I phi" := (@prv _ _ _ intu A ) (at level 55).
Notation "A ⊢M phi" := (@prv _ _ falsity_off intu A ) (at level 55).
Notation "T ⊢T phi" := (tprv T ) (at level 55).
Notation "T ⊢TI phi" := (@tprv _ _ _ intu T ) (at level 55).
Notation "T ⊢TC phi" := (@tprv _ _ _ class T ) (at level 55).