Formal Results of Constructive Logicism
Neil W. Tennant · Oxford University Press eBooks · 2022
We prove in the metalanguage, by induction on natural numbers n, that derivations can be given in free Core Logic of all instances of Schema N (#xΦx = n ⊣⊢ ∇nxΦx). We also prove all of the Dedekind‒Peano postulates for successor arithmetic, including the Principle of Mathematical Induction. To this end one needs only the rules of free Core Logic itself, the rules for 0, s and # set out in Chapter 10, and certain logical rules about one-one mappings that are clearly stated. Among the lemmas proved along the way to the Dedekind‒Peano postulates is the result known as ‘Frege’s trick’: any natural number is the number of naturals preceding it. All derivations are given with complete formal rigor, but with additional commentary in ‘logician’s English’ to convey the gist of the formal work.