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
(*>*)