FOM: the necessary truth of "7+5=12"

[Neil Tennant]

Vaughan Pratt thinks it is not necessarily true that 7 + 5 = 12.  This
note will show what problems he then has to face.

Abbreviations:

Zero(F) =df ~ExFx
One(F) =df Ex(Fx & (y)(Fy -> y=x))
Two(F) =df ExEy(Fx&Fy&(w)(Fw->(w=xvw=y)))
:
etc.

The generic representative from this list is of the form "There are
exactly n Fs".  Note that these are all sentences of first-order logic
with identity, but without any explicit notation for numbers.

F|G =df ~Ex(Fx&Gx) 	("Nothing is both F and G")
#F =df #xFx		("the number of Fs")
5 =df sssss0
7 =df sssssss0
12 =df ssssssssssss0
n* =df the numeral in (0,s) notation  for the natural number n
Seven(F) =df There are exactly seven Fs
Five(G) =df There are exactly five Gs
Twelve(FvG) =df There are exactly twelve (F or G)s

We offer the following inference rule as defining the operation + in
general:

[Defn.+]	F|G  |-  #(FvG) = #F + #G

This says that the number of things in the union of two disjoint
collections is the SUM of the numbers of things within each
collection.

We have the following schema governing numerosity and number:

[Schema N]	There are exactly n Fs -||- #xFx = n*

Consider now the following proof:

1.	Seven(F)	Assumption				 {1}
2.	Five(G)		Assumption				 {2}
3.	F|G		Assumption				 {3}
4.	Twelve(FvG)	By first-order logic from 1,2,3  	 {1,2,3}
5.	#(FvG) = 12	By Schema N from 4		 	 {1,2,3}
6.	#(FvG) = #F+#G	By Defn. +  from 3	 		 {3}
7.	#F+#G = 12	By substitutivity of identicals from 5,6 {1,2,3}
8.	#F = 7		By Schema N from 1			 {1}
9.	#G = 5		By Schema N from 2			 {2}
10.	7 + 5 = 12	By substitutivity of identicals (x2) from 7,8,9 {1,2,3}


To show that the conclusion "7 + 5 = 12" is NECESSARILY true, it
suffices to exhibit particular predicates F, G for which 1, 2 and 3
are necessarily true.  It is left as an exercise to the reader to
verify this for the following choices for F and G:

Fx : x=0 v x=s0 v x=ss0 v x=sss0 v x=ssss0 v x=sssss0 v x=ssssss0

Gx : x=sssssss0 v x=ssssssss0 v x=sssssssss0 v x=ssssssssss0 v x=sssssssssss0

To prove Seven(F), Five(G) and F|G one simply needs to be able to
refute any identity statement involving distinct numerals. That is a
simple matter of the logic of numbers, requiring only the (logical
derivability of) the usual first and second Peano-Dedekind axioms for
successor:

	(x)~0=sx
	(x)(y)(sx=sy -> x=y)

Now let us return to Vaughan Pratt's claim that it is not necessarily
true that 7 + 5 = 12.  He will have to tell us which step in our proof
of its necessity is at fault.

The only materials used in that proof are: (intuionistic relevant)
first-order logic; (the left-to-right direction of) Schema N; the
definition of +; the two Peano-Dedekind axioms for successor (the ones
that say that 0 is initial and that there is no backward branching
with successor).

Vaughan, which of these do you think might fail to be necessary?

If you find fault with any part of intuitionistic relevant logic then
you will be refusing to accept inferences that are directly expressive
of the meanings of the logical operators.  If you refuse to accept the
left-to-right direction of Schema N, then you are refusing to
participate in natural number discourse altogether, or at least
refusing to acknowledge that the natural numbers can be used to count
finite collections. If you refuse to accept the operational definition
of +, then you are so changing the meaning of that arithmetical sign
that your claim is devoid of any interest.  If you refuse to accept
the two Peano-Dedekind axioms indicated, then you are so changing the
meanings of the arithematical signs 0 and s that your claim is once
again devoid of any interest.

So which is it to be?

Neil Tennant