[FOM] Arithmetic-free theory of formal systems?

[Rene Vestergaard]

In response to Timothy Chow's question and the various answers to it, in 
particular the one by John McCarthy, allow me to point to my thesis "The 
Primitive Proof Theory of the lambda-Calculus". In it, I develop a 
substantial part of lambda-calculus theory using only the proof 
principles John McCarthy referred to. In other words, all proofs are 
conducted over the lambda-calculus presented as first-order abstract 
syntax while using only structural or rule induction and while relying 
on structural-recursive definitions for all arguments to do with 
totality, computability, and functionality. Substantial parts of the 
work has been formally verified in the Isabelle/HOL theorem prover in 
conjunction with James Brotherston.

The results that most directly address Timothy Chow's questions are 
Prop. 1.28 (and the preceding lemmas), which shows that Curry-style 
substitution is a total, computable function and, presumably, Section 
3.3, which shows that alpha-equivalence is decidable.

Sincerely,
Rene Vestergaard

Details at: http://www.jaist.ac.jp/~vester/, 
http://www.jaist.ac.jp/~vester/Writings/thesis.pdf (please note that the 
proof of Lemma 7.22 contains an error, as it stands).