(* 
  Autor(s):
    Andrej Dudenhefner (1) 
  Affiliation(s):
    (1) Saarland University, Saarbrücken, Germany
*)

(* 
  Problem(s):
    Provability in Hilbert-style calculi (HSC_PRV)
    Recognizing axiomatizations of Hilbert-style calculi (HSC_AX)

  HSC_PRV:
    Fix a list s₁,...,sₙ of formulae.
    Given a formula s, is s₁,...,sₙ ⊢ s derivable?

  HSC_AX:
    Given a list s₁,...,sₙ of formulae such that 
    a → b → a ⊢ sᵢ is derivable for i = 1...n,
    is s₁,...,sₙ ⊢ a → b → a derivable?

  References:
    1 Grigoriy V. Bokov: Undecidable problems for propositional calculi with implication. 
      Logic Journal of the IGPL, 24(5):792–806, 2016. doi:10.1093/jigpal/jzw013
    2 Andrej Dudenhefner, Jakob Rehof: Lower End of the Linial-Post Spectrum. 
      TYPES 2017: 2:1-2:15. doi: 10.4230/LIPIcs.TYPES.2017.2
*)

Require Import List.
Import ListNotations.

(* propositional formulae s, t ::= a | s → t *)
Inductive formula : Set :=
  | var : nat -> formula
  | arr : formula -> formula -> formula.

(* substitute ζ t replaces each variable n in t by ζ n *)
Fixpoint substitute (ζ: nat -> formula) (t: formula) : formula :=
  match t with
  | var n => ζ n
  | arr s t => arr (substitute ζ s) (substitute ζ t)
  end.

(* Hilbert-style calculus *)
Inductive hsc (Gamma: list formula) : formula -> Prop :=
  | hsc_var : forall (ζ: nat -> formula) (t: formula), In t Gamma -> hsc Gamma (substitute ζ t)
  | hsc_arr : forall (s t : formula), hsc Gamma (arr s t) -> hsc Gamma s -> hsc Gamma t.

(* is the formula s derivable from the fixed list of formulae Gamma? *)
Definition HSC_PRV (Gamma: list formula) (s: formula) := hsc Gamma s.

(* the formula a → b → a *)
Definition a_b_a : formula := arr (var 0) (arr (var 1) (var 0)).

(* list of formulae derivable from a → b → a *)
Definition HSC_AX_PROBLEM := { Gamma: list formula | forall s, In s Gamma -> hsc [a_b_a] s}.

(* is the formula a → b → a derivable? *)
Definition HSC_AX (l: HSC_AX_PROBLEM) := hsc (proj1_sig l) a_b_a.