From Undecidability Require Import Shared.ListAutomation.
From Undecidability.Synthetic Require Import Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts.
Import ListAutomationNotations.
From FOL Require Import FragmentSyntax Theories.

Local Unset Implicit Arguments.
Section Gentzen.

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

  Inductive sprv : forall (b : falsity_flag), list form -> option form -> form -> Prop :=
  | Contr {b} A phi psi : sprv b A (Some phi) psi -> phi el A -> sprv b A None psi
  | IR {b} A phi psi : sprv b (phi :: A) None psi -> sprv b A None (phi → psi)
  | AllR {b} A phi : sprv b (map (subst_form ↑) A) None phi -> sprv b A None (∀ phi)
  | Absurd A phi : sprv falsity_on A None ⊥ -> sprv falsity_on A None phi
  | Ax {b} A phi : sprv b A (Some phi) phi
  | IL {b} A phi psi xi : sprv b A None phi -> sprv b A (Some psi) xi -> sprv b A (Some (phi → psi)) xi
  | AllL {b} A phi t psi : sprv b A (Some (phi[t..])) psi -> sprv b A (Some (∀ phi)) psi.

  Notation "A '⊢S' phi" := (sprv _ A None phi) (at level 30).
  Notation "A ';;' phi '⊢s' psi" := (sprv _ A (Some phi) psi) (at level 70).
  Arguments sprv {_} _ _ _.

  Definition stprv {b : falsity_flag} (T : theory) (phi : form) : Prop :=
    exists A, A ⊏ T /\ sprv A None phi.
End Gentzen.

#[global]
Hint Constructors sprv : core.

Notation "A '⊢S' phi" := (sprv _ A None phi) (at level 30).
Notation "A ';;' phi '⊢s' psi" := (sprv _ A (Some phi) psi) (at level 70).
Notation "A '⊢SE' phi" := (sprv falsity_on A None phi) (at level 30).
Notation "A ';;' phi '⊢sE' psi" := (sprv falsity_on A (Some phi) psi) (at level 70). Arguments sprv {_} {_} {_} _ _ _.
Notation "T '⊩SE' phi" := (@stprv _ _ falsity_on T phi) (at level 30).