Harvey Friedman has done some nice work on leveraging his theory of explicit definitions for set theory (cf. The Logical Strength of Mathematical Statements I, 1976) to give a language for doing mathamtics in a way that can be easily translated into proofs over ZFC.
Charles Stewart
- 2.3k
- 19
- 27