[FOM] Arithmetic-free theory of formal systems?
vester at jaist.ac.jp
Tue May 18 03:35:03 EDT 2004
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.
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).
More information about the FOM