Theory Abstract_Jeroslow_Encoding

chapter ‹Jeroslow's Variant of G\"odel's Second Incompleteness Theorem›

(*<*)
theory Abstract_Jeroslow_Encoding imports
"Syntax_Independent_Logic.Deduction"
begin
(*>*)

section ‹Encodings and Derivability›

text ‹Here we formalize some of the assumptions of Jeroslow's theorem:
encoding, term-encoding and the First Derivability Condition.›


subsection ‹Encoding of formulas›

locale Encode =
Syntax_with_Numerals
  var trm fmla Var FvarsT substT Fvars subst
  num
for
var :: "'var set" and trm :: "'trm set" and fmla :: "'fmla set"
and Var FvarsT substT Fvars subst
and num
+
fixes
(*************************************)
(* Numeric formulas are assumed to be encoded as numerals: *)
enc :: "'fmla  'trm" ("_")
assumes
enc[simp,intro!]: " φ. φ  fmla  enc φ  num"
begin

end ― ‹context @{locale Encode}


subsection ‹Encoding of computable functions›

text ‹Jeroslow assumes the encodability of an abstract (unspecified) class of
computable functions and the assumption that a particular function, @{term "sub φ"} for each formula
@{term φ}, is in this collection. This is used to prove a different flavor of the diagonalization
lemma (Jeroslow 1973). It turns out that only an encoding of unary computable functions
is needed, so we only assume that.›

locale Encode_UComput =
Encode
  var trm fmla Var FvarsT substT Fvars subst
  num
  enc
for
var :: "'var set" and trm :: "'trm set" and fmla :: "'fmla set"
and Var FvarsT substT Fvars subst
and num
and enc ("_")
+
― ‹Abstract (unspeficied) notion of unary "computable" function
between numerals, which are encoded as numerals. They
contain a special substitution-like function @{term "sub φ"} for each formula @{term "φ"}.›
fixes ucfunc :: "('trm  'trm) set"
  and encF :: "('trm  'trm)  'trm"
  and sub :: "'fmla  'trm  'trm"
assumes
― ‹NB: Due to the limitations of the type system, we define @{term "ufunc"} as a set of functions
between terms, but we only care about their actions on numerals ...
so we assume they send numerals to numerals:›
ucfunc[simp,intro!]: " f n. f  ucfunc  n  num  f n  num"
and
encF[simp,intro!]: " f. f  ucfunc  encF f  num"
and
sub[simp]: "φ. φ  fmla  sub φ  ucfunc"
and
― ‹The function @{term "sub φ"} takes any encoding of a function @{term "f"} and returns the encoding of
the formula obtained by substituting for @{term "xx"} the value of @{term "f"} applied to its own encoding:›
sub_enc:
" φ f. φ  fmla  Fvars φ = {xx}  f  ucfunc 
    sub φ (encF f) = enc (inst φ (f (encF f)))"


subsection ‹Term-encoding of computable functons›

text ‹For handling the notion of term-representation (which we introduce later),
we assume we are given a set @{term "Ops"} of term operators and their encodings as numerals.
We additionally assume that the term operators behave well w.r.t. free variables and
substitution.›

locale TermEncode =
Syntax_with_Numerals
  var trm fmla Var FvarsT substT Fvars subst
  num
for
var :: "'var set" and trm :: "'trm set" and fmla :: "'fmla set"
and Var FvarsT substT Fvars subst
and num
+
fixes
Ops ::  "('trm  'trm) set"
and
enc :: "('trm  'trm)  'trm" ("_")
assumes
Ops[simp,intro!]: "f t. f  Ops  t  trm  f t  trm"
and
enc[simp,intro!]: " f. f  Ops  enc f  num"
and
Ops_FvarsT[simp]: " f t. f  Ops  t  trm  FvarsT (f t) = FvarsT t"
and
Ops_substT[simp]: " f t. f  Ops  t  trm  t1  trm  x  var 
  substT (f t) t1 x = f (substT t t1 x)"
begin

end ― ‹context @{locale TermEncode}


subsection ‹The first Hilbert-Bernays-Löb derivability condition›

locale HBL1 =
Encode
  var trm fmla Var FvarsT substT Fvars subst
  num
  enc
+
Deduct
  var trm fmla Var FvarsT substT Fvars subst
  num
  eql cnj imp all exi
  prv
for
var :: "'var set" and trm :: "'trm set" and fmla :: "'fmla set"
and Var FvarsT substT Fvars subst
and num
and eql cnj imp all exi
and prv bprv
and enc ("_")
+
fixes P :: 'fmla
assumes
P[intro!,simp]: "P  fmla"
and
Fvars_P[simp]: "Fvars P = {xx}"
and
HBL1: "φ. φ  fmla  Fvars φ = {}  prv φ  prv (subst P φ xx)"
begin

text ‹Predicate version of the provability formula›
definition PP where "PP  λt. subst P t xx"

lemma PP[simp]: "t. t  trm  PP t  fmla"
  unfolding PP_def by auto

lemma Fvars_PP[simp]: "t. t  trm  Fvars (PP t) = FvarsT t"
  unfolding PP_def by auto

lemma [simp]:
"n  num  subst (PP (Var yy)) n yy = PP n"
"n  num  subst (PP (Var xx)) n xx = PP n"
  unfolding PP_def by auto

lemma HBL1_PP:
"φ  fmla  Fvars φ = {}  prv φ  prv (PP φ)"
  using HBL1 unfolding PP_def by auto

end ― ‹context @{locale HBL1}

(*<*)
end
(*>*)