Definability of + in SOL
rzach opened this issue · 0 comments
rzach commented
In second-order-arithmetic/metatheory/second-order-arithmetic.tex, the proof of sol-pa-definable appears to be incomplete: the statement claims that + and × are definable in PA²† as well, but only ≤ is proven.
Carry out the proof for + and leave only × as an exercise.
(Reported by @ionathanch in #230 (comment) )