Clock Math

Imagine a clock with only 5 numbers on the face: 1,2,3,4,5.

Win the dial moves from the number 1 position on the face of the clock to the number 2 position on the face of the clock, we represent this movement as: 1 + 1 = 2.

Win the dial goes from position 2 to position 3, we represent this as:

2 + 1 = 3.

Win the dial goes from position 3 to position 4, we rite: 3 + 1 = 4.

Win the dial goes from position 4 to position 5, we rite: 4 + 1 = 5.

Win the dial goes from position 5 back to position 1, we represent this as: 5 + 1 = 1.

So here we list our clock dial movement facts:

1 + 1 = 2.

2 + 1 = 3.

3 + 1 = 4.

4 + 1 = 5.

5 + 1 = 1.

In order to not confuse these “clock numbers” with the natural numbers, we will represent these numbers by prefixing them with a backslash.

So we rerite our clock dial movement facts this way:

\1 + \1 = \2.

\2 + \1 = \3.

\3 + \1 = \4.

\4 + \1 = \5.

\5 + \1 = \1.

In the discussion that follows, I will rite the predicates '∈' and 'is a member of' by the word 'in'.

Now suppose a set C contains only these “clock numbers”. Then the following facts are also true:

\1 in C.

\2 in C.

\3 in C.

\4 in C.

\5 in C.

(x in C => (x = \1 or x = \2 or x = \3 or x = \4 or x = \5))(x)

Add to these facts one more fact:

((x in C & y in C) => x + y = y + x)(y,x) This is the commutative rule.

We will call these facts the axioms of our clock system.

With these axioms, we can derive many therems by using the rules of natural deduction plus the substitucion rule of equality. [V]

The substitucion rule is: For all F, Z, X, Y: If F is a property and Z is a set and X is a member of Z and Y is a member of Z and X = Y and X has the property F, then Y also has the property F.

Another way to rite this rule is:

(F es property & z es set & x in z & y in z & x = y & F(x) => F(y))(F,z,y,x)

If we play around with this system, we will start to see certin patterns. One of these patterns is that win we start our dial at any number on the clock face and we move the dial 5 units forward, the dial always arrives back to the number that we started from. [i] Let us try to prove that this pattern is a result of the axioms of this system. In other words, we want to show: (x in C => x + \5 = x)(x). [ii]

To proceed, our first step is to hypothesize a set that contains only these “clock numbers”. We also hypothesize the dial movement facts for these numbers that are listed above, and the commutative rule for these numbers. We rite this hypothesis:

0H: C es set & (\1 in C) & (\2 in C) & (\3 in C) & (\4 in C) & (\5 in C) & (x in C => (x = \1 or x = \2 or x = \3 or x = \4 or x = \5))(x) & (\1 + \1 = \2) & (\2 + \1 = \3) & (\3 + \1 = \4) & (\4 + \1 = \5) & (\5 + \1 = \1) & ((x in C & y in C) => x + y = y + x)(y,x)	hypothe-sis introduc-tion i.e. hypth
(* Now that we have ritten our initial hypothesis, we proceed to derive further therems and ultimately the conclusion we are seeking for. *)
(* We now list each proposition of the hypothesis thru conjunction elimination. *)
C es set	conjunction elimination i.e. cnj out
(\1 in C) & (\2 in C) & (\3 in C) & (\4 in C) & (\5 in C)	cnj out
(\1 in C)	cnj out
\1 in C	() out
(\2 in C) & (\3 in C) & (\4 in C) & (\5 in C)	cnj out
(\2 in C)	cnj out
\2 in C	() out
(\3 in C) & (\4 in C) & (\5 in C)	cnj out
(\3 in C)	cnj out
\3 in C	() out
(\4 in C) & (\5 in C)	cnj out
(\4 in C)	cnj out
\4 in C	() out
(\5 in C)	cnj out
\5 in C	() out
(x in C => (x = \1 or x = \2 or x = \3 or x = \4 or x = \5))(x) & (\1 + \1 = \2) & (\2 + \1 = \3) & (\3 + \1 = \4) & (\4 + \1 = \5) & (\5 + \1 = \1) & ((x in C & y in C) => x + y = y + x)(y,x)	cnj out
(x in C => (x = \1 or x = \2 or x = \3 or x = \4 or x = \5))(x)	cnj out
(\1 + \1 = \2) & (\2 + \1 = \3) & (\3 + \1 = \4) & (\4 + \1 = \5) & (\5 + \1 = \1) & ((x in C & y in C) => x + y = y + x)(y,x)	cnj out
(\1 + \1 = \2) & (\2 + \1 = \3) & (\3 + \1 = \4) & (\4 + \1 = \5) & (\5 + \1 = \1)	cnj out
((x in C & y in C) => x + y = y + x)(y,x)	cnj out
(\5 + \1 = \1)	cnj out
\5 + \1 = \1	() out
(\1 + \1 = \2) & (\2 + \1 = \3) & (\3 + \1 = \4) & (\4 + \1 = \5)	cnj out
(\4 + \1 = \5)	cnj out
\4 + \1 = \5	() out
(\1 + \1 = \2) & (\2 + \1 = \3) & (\3 + \1 = \4)	cnj out
(\3 + \1 = \4)	cnj out
\3 + \1 = \4	() out
(\1 + \1 = \2) & (\2 + \1 = \3)	cnj out
(\2 + \1 = \3)	cnj out
\2 + \1 = \3	() out
(\1 + \1 = \2)	cnj out
\1 + \1 = \2	() out
(* We now derive sum therems by the commutative rule. *)
((x in C & y in C) => x + y = y + x)(y,x)	repeat i.e. rp
((\2 in C & y in C) => \2 + y = y + \2)(y)	specification i.e. spc
((\2 in C & \1 in C) => \2 + \1 = \1 + \2)	spc
\2 in C & \1 in C	conjunction introduction i.e. cnj
\2 + \1 = \1 + \2	modus ponens i.e. mp
((x in C & y in C) => x + y = y + x)(y,x)	rp
((\3 in C & y in C) => \3 + y = y + \3)(y)	spc
((\3 in C & \1 in C) => \3 + \1 = \1 + \3)	spc
\3 in C & \1 in C	cnj
\3 + \1 = \1 + \3	mp
((x in C & y in C) => x + y = y + x)(y,x)	rp
((\4 in C & y in C) => \4 + y = y + \4)(y)	rp
((\4 in C & \1 in C) => \4 + \1 = \1 + \4)	rp
\4 in C & \1 in C	cnj
\4 + \1 = \1 + \4	mp
((x in C & y in C) => x + y = y + x)(y,x)	rp
((\5 in C & y in C) => \5 + y = y + \5)(y)	spc
((\5 in C & \1 in C) => \5 + \1 = \1 + \5)	spc
\5 in C & \1 in C	cnj
\5 + \1 = \1 + \5	mp
((x in C & y in C) => x + y = y + x)(y,x)	rp
((\5 in C & y in C) => \5 + y = y + \5)(y)	spc
((\5 in C & \2 in C) => \5 + \2 = \2 + \5)	spc
\5 in C & \2 in C	cnj
\5 + \2 = \2 + \5	mp
((x in C & y in C) => x + y = y + x)(y,x)	rp
((\5 in C & y in C) => \5 + y = y + \5)(y)	spc
((\5 in C & \3 in C) => \5 + \3 = \3 + \5)	spc
\5 in C & \3 in C	cnj
\5 + \3 = \3 + \5	mp
((x in C & y in C) => x + y = y + x)(y,x)	rp
((\5 in C & y in C) => \5 + y = y + \5)(y)	spc
((\5 in C & \4 in C) => \5 + \4 = \4 + \5)	spc
\5 in C & \4 in C	cnj
\5 + \4 = \4 + \5	mp
((x in C & y in C) => x + y = y + x)(y,x)	rp
((\5 in C & y in C) => \5 + y = y + \5)(y)	spc
((\5 in C & \5 in C) => \5 + \5 = \5 + \5)	spc
\5 in C & \5 in C	cnj
\5 + \5 = \5 + \5	mp
(* We now derive some addition therems by substitution *)
\5 + \1 = \1 + \5	rp
\5 + \1 = \1	rp
\1 + \5 = \1	substitution i.e. sbst
\5 + \2 = \2 + \5	rp
\1 + \1 = \2	rp
\5 + \2 = (\1 + \1) + \5	sbst
\5 + \2 = \1 + \1 + \5	() out
\5 + \1 = \1 + \5	rp
\5 + \2 = \1 + (\5 + \1)	sbst
\5 + \2 = \1 + \5 + \1	() out
\5 + \1 = \1	rp
\5 + \2 = \1 + (\1)	sbst
\5 + \2 = \1 + \1	() out
\1 + \1 = \2	rp
\5 + \2 = (\2)	sbst
\5 + \2 = \2	() out
\5 + \2 = \2 + \5	rp
\2 + \5 = \2	sbst
\5 + \3 = \3 + \5	rp
\2 + \1 = \3	rp
\5 + \3 = (\2 + \1) + \5	sbst
\5 + \3 = \2 + \1 + \5	() out
\5 + \1 = \1 + \5	rp
\5 + \3 = \2 + (\5 + \1)	sbst
\5 + \1 = \1	rp
\5 + \3 = \2 + (\1)	sbst
\5 + \3 = \2 + \1	() out
\2 + \1 = \3	rp
\5 + \3 = \3	sbst
\5 + \3 = \3 + \5	rp
\3 + \5 = \3	sbst
\5 + \4 = \4 + \5	rp
\3 + \1 = \4	rp
\5 + \4 = (\3 + \1) + \5	sbst
\5 + \4 = \3 + \1 + \5	()
\5 + \1 = \1 + \5	rp
\5 + \4 = \3 + (\5 + \1)	sbst
\5 + \1 = \1	rp
\5 + \4 = \3 + (\1)	sbst
\5 + \4 = \3 + \1	() out
\3 + \1 = \4	rp
\5 + \4 = \4	sbst
\5 + \4 = \4 + \5	rp
\4 + \5 = \4	sbst
\5 + \5 = \5 + \5	rp
\4 + \1 = \5	rp
\5 + \5 = \5 + (\4 + \1)	sbst
\4 + \1 = \1 + \4	rp
\5 + \5 = \5 + (\1 + \4)	sbst
\5 + \5 = \5 + \1 + \4	() out
\5 + \1 = \1	rp
\5 + \5 = (\1) + \4	sbst
\5 + \5 = \1 + \4	() out
\4 + \1 = \1 + \4	rp
\5 + \5 = \4 + \1	sbst
\4 + \1 = \5	rp
\5 + \5 = \5	sbst

(* -------------------start of inner hypothesis units-------------------- *)
1H: \6 in C	hypth
(x in C => (x = \1 or x = \2 or x = \3 or x = \4 or x = \5))(x)	rp
(\6 in C => (\6 = \1 or \6 = \2 or \6 = \3 or \6 = \4 or \6 = \5))	spc
\6 in C	rp
(\6 = \1 or \6 = \2 or \6 = \3 or \6 = \4 or \6 = \5)	mp
\6 = \1 or \6 = \2 or \6 = \3 or \6 = \4 or \6 = \5	() out
2H: \6 = \1	hypth
\1 + \5 = \1	rp
\6 + \5 = \1	sbst
\6 + \5 = \6	sbst
-2H: \6 = \1 => \6 + \5 = \6	conditional proof or conditional introduction i.e. cp
\6 = \1 or \6 = \2 or \6 = \3 or \6 = \4 or \6 = \5	rp
\6 + \5 = \6 or \6 = \2 or \6 = \3 or \6 = \4 or \6 = \5	constructive dilemma
2H: \6 = \2	hypth
\2 + \5 = \2	rp
\6 + \5 = \2	sbst
\6 + \5 = \6	sbst
-2H: \6 = \2 => \6 + \5 = \6	cp
\6 + \5 = \6 or \6 = \2 or \6 = \3 or \6 = \4 or \6 = \5	rp
\6 + \5 = \6 or \6 + \5 = \6 or \6 = \3 or \6 = \4 or \6 = \5	constructive dilemma
\6 + \5 = \6 or \6 = \3 or \6 = \4 or \6 = \5	((p or p) <=> p)
2H: \6 = \3	hypth
\3 + \5 = \3	rp
\6 + \5 = \3	sbst
\6 + \5 = \6	sbst
-2H: \6 = \3 => \6 + \5 = \6	cp
\6 + \5 = \6 or \6 = \3 or \6 = \4 or \6 = \5	rp
\6 + \5 = \6 or \6 + \5 = \6 or \6 = \4 or \6 = \5	constructive dilemma
\6 + \5 = \6 or \6 = \4 or \6 = \5	((p or p) <=> p)
2H: \6 = \4	hypth
\4 + \5 = \4	rp
\6 + \5 = \4	sbst
\6 + \5 = \6	sbst
-2H: \6 = \4 => \6 + \5 = \6	cp
\6 + \5 = \6 or \6 = \4 or \6 = \5	rp
\6 + \5 = \6 or \6 + \5 = \6 or \6 = \5	constructive dilemma
\6 + \5 = \6 or \6 = \5	((p or p) <=> p)
2H: \6 = \5	hypth
\5 + \5 = \5	rp
\6 + \5 = \5	sbst
\6 + \5 = \6	sbst
-2H: \6 = \5 => \6 + \5 = \6	cp
\6 + \5 = \6 or \6 = \5	rp
\6 + \5 = \6 or \6 + \5 = \6	constructive dilemma
\6 + \5 = \6	((p or p) <=> p)
-1H: \6 in C => \6 + \5 = \6	cp
(x in C => x + \5 = x)(x)	generalization ie. genrl
(* --------this is the desired conclusion-------------------*)
(* Now that we have derived the desired conclusion, we derive the general conclusion that if we have the clock system that we initially hypothesized, then the conclusion follows that win we start our dial at any number on the clock face and we move the dial 5 units forward, the dial always arrives back to the number that we started from. *)
-0H: (C es set & (\1 in C) & (\2 in C) & (\3 in C) & (\4 in C) & (\5 in C) & (x in C => (x = \1 or x = \2 or x = \3 or x = \4 or x = \5))(x) & (\1 + \1 = \2) & (\2 + \1 = \3) & (\3 + \1 = \4) & (\4 + \1 = \5) & (\5 + \1 = \1) & ((x in C & y in C) => x + y = y + x)(y,x) ) => (x in C => x + \5 = x)(x)	cp
(* we now complete the generalization of the remaining variables *)

((S es set & (\1 in S) & (\2 in S) & (\3 in S) & (\4 in S) & (\5 in S) & (x in S => (x = \1 or x = \2 or x = \3 or x = \4 or x = \5))(x) & (\1 + \1 = \2) & (\2 + \1 = \3) & (\3 + \1 = \4) & (\4 + \1 = \5) & (\5 + \1 = \1) & ((x in S & y in S) => x + y = y + x)(y,x) ) => (x in S => x + \5 = x)(x))(S)	genrl
((S es set & (\1 in S) & (\2 in S) & (\3 in S) & (\4 in S) & (\50 in S) & (x in S => (x = \1 or x = \2 or x = \3 or x = \4 or x = \50))(x) & (\1 + \1 = \2) & (\2 + \1 = \3) & (\3 + \1 = \4) & (\4 + \1 = \50) & (\50 + \1 = \1) & ((x in S & y in S) => x + y = y + x)(y,x) ) => (x in S => x + \50 = x)(x))(S, \50)	genrl

((S es set & (\1 in S) & (\2 in S) & (\3 in S) & (\40 in S) & (\50 in S) & (x in S => (x = \1 or x = \2 or x = \3 or x = \40 or x = \50))(x) & (\1 + \1 = \2) & (\2 + \1 = \3) & (\3 + \1 = \40) & (\40 + \1 = \50) & (\50 + \1 = \1) & ((x in S & y in S) => x + y = y + x)(y,x) ) => (x in S => x + \50 = x)(x))(S, \50, \40)	genrl
((S es set & (\1 in S) & (\2 in S) & (\30 in S) & (\40 in S) & (\50 in S) & (x in S => (x = \1 or x = \2 or x = \30 or x = \40 or x = \50))(x) & (\1 + \1 = \2) & (\2 + \1 = \30) & (\30 + \1 = \40) & (\40 + \1 = \50) & (\50 + \1 = \1) & ((x in S & y in S) => x + y = y + x)(y,x) ) => (x in S => x + \50 = x)(x))(S, \50, \40, \30)	genrl

((S es set & (\1 in S) & (\20 in S) & (\30 in S) & (\40 in S) & (\50 in S) & (x in S => (x = \1 or x = \20 or x = \30 or x = \40 or x = \50))(x) & (\1 + \1 = \20) & (\20 + \1 = \30) & (\30 + \1 = \40) & (\40 + \1 = \50) & (\50 + \1 = \1) & ((x in S & y in S) => x + y = y + x)(y,x) ) => (x in S => x + \50 = x)(x))(S, \50, \40, \30, \20)	genrl
((S es set & (\10 in S) & (\20 in S) & (\30 in S) & (\40 in S) & (\50 in S) & (x in S => (x = \10 or x = \20 or x = \30 or x = \40 or x = \50))(x) & (\10 + \10 = \20) & (\20 + \10 = \30) & (\30 + \10 = \40) & (\40 + \10 = \50) & (\50 + \10 = \10) & ((x in S & y in S) => x + y = y + x)(y,x) ) => (x in S => x + \50 = x)(x))(S, \50, \40, \30, \20, \10)	genrl

Notes:

i: Note the clock number \5 is similar to the real number 5, but does have some differences. For one thing, \5 is like the additive identity element.

ii: In a universally quantified formula, I rite the list of quantified variables that appear in the formula at the end of the formula, rather then at the beginning. This is simply my custom. Also, since I take universal quantification as the default form of quantification, over existential quantification, I ofen omit the explicit symbol for the universal quantifier.

So insted of riting '(∀x)(x in R => x + 1 in R)',

I usually rite: (x in R => x + 1 in R)(x).

V: The rules of natural deduction include modus ponens, conjunction introduction, conjunction elimination, conditional proof, disjunction introduction, disjunction elimination, generalization, specification, etc. and the therems of propositional calculus, such as ((P or P) <=> P).