A proof of nominalism: an exercise in successful reduction in logic

Let us assume also that f does not appear nested in (1). That means that it occurs in F only in contexts like A(f(x)) or f(x) = a. Hence (1) is of the form

Now (1) is easily seen to be equivalent with the following formula

This equivalence can be shown to hold as follows: The Skolem function translation into second-order form is

This elimination is obviously repeatable so as to be extendable to any number of initial universal quantifiers in the prenex form of F and to any number of initial existential quantifiers (f₁)(f₂), … instead of the single one (f).

If there is nesting of the functions f₁, f₂,… in F, it can be eliminated by introducing new functions f_i and new universal quantifiers (x_i). For instance, if in F there occurs a term f_i(f₂(x)), we can add a new initial existential quantifier (g) and add after the prenex of F the conjunct
(4) (z)(u)((g(z) = u)  (w)(w=f₂(u) & z=f₁(w))
This procedure can be generalized. We can in fact easily replace predicate variables in the initial formula by variables for their characteristic functions. This extends the procedure so as to eliminate any formula-initial second-order existential quantifier albeit at the cost of introducing independence indicators (slashes). Moreover, this elimination can be applied to any unnegated existential quantifier in context, not just initial ones.

As to universal second-order quantifiers and negated second-order existential quantifiers, it suffices to point out that a universal second-order quantifier (f) prefixing a subformula (f)F[f] can be replaced by (f) F(f). We can now eliminate (f) from the subformula (f)F[f] in the way just indicated. The result does not contain second-order quantifiers (if we apply the reduction from inside out) but does normally contain contradictory negations . It is therefore a FEIF logic (sub) formula.

When these eliminations are carried out step by step in a given second-order formula, moving from inside out, all the second-order quantifiers are ultimately eliminated. The procedure does introduce independence indicators and contradictory negations, which is to say that the result is a FEIF formula, but does not introduce any second-order quantifiers. This accomplishes the reduction of the entire traditional second-order logic to the first-order level. The reduct sentence is a first-order sentence: all its quantifiers range over first-order entities. However, it does contain contradictory negations also within the scope of quantifiers. The additional power of second-order logic is therefore due, not to its being second-order, but to its unlimited use of contradictory negation. This means essentially unlimited use of tertium non datur. In a sense, this vindicates Brouwer’s idea that the excessive power of classical mathematics stems from the use of the principle of excluded middle.

The same reduction can apparently be used to translate logic of the order n+1 to the order n and hence ultimately to the first-order level. This possibility will not be discussed here, however.

Thus for instance a (sub) formula of the form

(6) (x)(y)(z)F[x,y,z]

will be replaced in our reduction by a formula of the form

(7) (f₁)(f₂)(g)F(f₁,g(f₁),f₂(f₁,g(f₁))]

(In this case the function f₁ is reduced to a constant.)

By repeated applications of this procedure, moving from outside in, we can formulate a second-order truth condition for each FEIF sentence. In the reduct, all contradictory negations  occur in the negation prenexes of atomic formulas. Hence by the earlier reduction it is equivalent to a FEIF sentence. The functions g₁, g₂, …, f₁,f₂,… deputize quantifiers in F. These quantifiers in turn codify moves made by players in the game G(F) connected with F. Hence, only variables occurring in the arguments of these functions can only be variables bound to other quantifiers in F.

In other words, by translating this second-order formula back to FEIF first-order logic we obtain for suitable FEIF languages a truth condition expressible in the same language.

Putting all this together, we can prove strictly the possibility of nominalism in the foundations of mathematics. This result is not only of philosophical interest. It has major implications for the foundations of mathematics in general and even for mathematics itself. First-order axiomatic set theory becomes redundant and so does in principle higher-order logic, except perhaps as a convenient shorthand. Our working logic will look more like general topology than conventional first-order logic. I will leave the rest of the resulting revolution to my audience to carry out.

References

Ebbinghaus, Heinz-Dieter, 2007, Ernst Zermelo, Berlin, Springer.

Henkin, Leon, 1949, “The completeness of the first-order fractional calculus”, Journal of Symbolic Logic vol. 14, pp. 159-166.

Hilbert, David, 1996 (original 1918), “Axiomatic thinking”, in: William B. Ewald (ed), From Kant to Hilbert, vol. 2, Oxford, Clarendon Press, pp. 1105-1115.

Hilbert, David, 1998 (original 1922), “The new grounding of mathematics, First report” in: William B. Ewald (ed), From Kant to Hilbert, vol. 2, Oxford, Clarendon Press, pp. 1115-1134.

Hilbert, David, and Paul Bernays, 1939, Grundlagen der Mathematik, vol. 2, Berlin, Springer.

Hintikka, Jaakko, 1955, “Notes on quantification theory”, Societas Scientiarum Fennicae, Commentationes Physican Mathematicae vol. 17, no. 2

Hintikka, Jaakko, 1996, The Principles of Mathematics Revisited, Cambridge, Cambridge University Press.

Hintikka, Jaakko, 2004(a), “What is the true algebra of logic?” in : Vincent Hendricks

et al. (eds), First-order Logic Revisited, Berlin, Logos Verlag, pp. 117-128.

Hintikka, Jaakko, 2004(b), “Independence friendly logic and axiomatic set theory”, Annals of Pure and Applied Logic, vol. 126, pp. 313-333.

Hintikka, Jaakko, 2006, “Truth, negation and other basic notions of logic” in: J.van

Benthem et al. (eds), The Age of Alternative Logics, Berlin, Springer,

pp. 195-219.

Hintikka, Jaakko, forthcoming, “Reforming logic (and set theory).

Hintikka, Jaakko and Jack Kulas, 1983, The Game of Language (Synthese Language Library vol. 22), D. Reidel, Dordrecht.

Hintikka, Jaakko, and Gabriel Sandu, 1999, “Tarski’s guilty secret: compositionality”, in Jan Wolenski and Ecklhart Köhler (eds.), Alfred Tarski and the Vienna Circle, Kluwer Academic, Dordrecht, pp. 217-230.

Jónsson, Bjarni, and Alfred Tarski, 1951, “Boolean algebras and operators I”, American Journal of Mathematics, vol. 73, pp.891-939.

Jónsson, Bjarni, and Alfred Tarski, 1952 , “Boolean algebras and operators II”, American Journal of Mathematics, vol. 74, pp.127-162.

Väänänen, Jouko, 2001, “Second-order logic and the foundations of mathematics”,

Zermelo, Ernst, 1908(a), “Neuer Beuer’s für die Möglichkeit einer Wohlordnung”, Mathematische Annalen vol. 65, pp. 107-128.