[FOM] 294: Concept Calculus 3

[Harvey Friedman]

We first correct some typos in #289,
http://www.cs.nyu.edu/pipermail/fom/2006-June/010627.html

I wrote:

"For FFF(6), the lower bounds are much sharper. Any proof that FFF(5) exists
in ATR must use at least A(10) symbols, where A is a common presentation of
the unary form of the Ackermann function. FFF(5) is greater than all least
witnesses of Sigma01 sentences provably true in ATR using at most A(10)
symbols."

This should be 

For FFF(6), the lower bounds are much sharper. Any proof that FFF(6) exists
in ATR must use at least A(10) symbols, where A is a common presentation of
the unary form of the Ackermann function. FFF(6) is greater than all least
witnesses of Sigma01 sentences provably true in ATR using at most A(10)
symbols. 

The last paragraph about FFF(5) does not need to be changed.

#####################################

We continue from Concept Calculus 2, June 20, 2006,
http://www.cs.nyu.edu/pipermail/fom/2006-June/010622.html.

CONCEPT CALCULUS
by
Harvey M. Friedman
June 25, 2006

Introduction.
1. Varying Quantity, Common Scale.
2. Varying Quantity, Common Scale, Transitions.
3. Varying Quantity - SIMPLIFIED.
4. Two Varying Quantities, Three Separate Scales.
5. Binary Relation, Single Scale.
6. Binary Relation, Two Separate Scales.
7. Multiple Agents, Two States.
8. Varying Bit.
9. Persistently Varying Bit.
10. Naive Time. 
11. Epochs Replacing Transitions.
12. Mereological Development.

Concept Calculus 1 http://www.cs.nyu.edu/pipermail/fom/2006-June/010616.html
has sections 1,2. Concept Calculus 2
http://www.cs.nyu.edu/pipermail/fom/2006-June/010622.html has sections 3-7.
We begin with section 8.

NOTE: It appears that we have understated the logical strength of our
strongest theories, that use Strong Transition Accumulation. We will report
on this as soon as we have some definitive information.

8. VARYING BIT.

In this section, we work with a bit varying over time. This is much more
elemental than any context considered in sections 1-7.

In order to get logical strength out of this very elemental situation, we
need to use forward translations of time. This is most conveniently
introduced through an addition function.

Forward time translation is based on the idea that for any times a,b, time
going forward from a looks the same as time going forward from b.

Conceptually, a+b from the point of view of a looking forward, corresponds
exactly to b from the point of view of -infinity looking forward. I.e., the
"amount of time from a to a+b is measured by b".

We also say that a+b is the result of translating a by b. Let A be a set of
points. The translation of A by b is the set of all a+b such that a lies in
A.

We work in the usual predicate calculus with equality with the binary
relation symbol <, the unary predicates T,P, and the binary operation +.

Here, as before, T(t) means that "t is a transition".

P corresponds to the varying bit. P(t) means "the varying bit at time t is
1".  

We can give several informal interpretations of this setup.

a. A light is flashing on and off, forever. P(t) means that the light is on
at time t. 

b. An agent is active or inactive, at any given time. P(t) means that the
agent is active at time t.

c. Instead of a time scale, we think of a physical ray, or one dimensional
space with a direction. There are pointmasses at some positions. P(t) means
that there is a pointmass at position t. Or P(t) means that the mass density
at time t is 1; otherwise 0.

All three of these interpretations suggest some natural and fundamental
restrictions on behavior, that are not considered in this section. There are
considered in section 9 and later.

LINEARITY. < is a linear ordering.

TRANSITIONS. Every time is earlier than some transition.

BOUNDED TIME TRANSLATION. For every given range of times before a given time
b, there exists a translation time c such that a time before b lies in the
range of times if and only if the bit at time b+c is 1.

BOUNDED TIME TRANSLATION. (therexists c)(forall t < b)(phi iff P(t+c)),
where phi is a formula of L(<,T,P,+) in which c is not free.

The idea of Bounded Time Translation is our usual one: that the behavior of
P over bounded intervals is arbitrary, up to translation. As mentioned
above, various reasonable objections can be made to this idea in the full
generality used here, some of which are met in the next section on Flashing
Lights. 

TRANSITION SIMILARITY. Any true statement involving x,y and a transition z >
x,y, remains true if z is replaced by any transition w > z. Here we use
L(<,P,+) to present the statement.

TAIL TRANSITION SIMILARITY. Any true statement involving x,y remains true if
we hypothetically restrict the transitions to those that are <= max(x,y)
together with those that are >= any given transition > x. Here we use
L(<,T,P,+) to present the true statement.

TRANSITION ACCUMULATION. There is a point which is the limit of earlier
transitions.

STRONG TRANSITION ACCUMULATION. There is a transition which is the limit of
earlier transitions.

Note that these axioms correspond exactly to those given in section 3 (and,
basically, to other sections), except that we have incorporated addition in
Bounded Time Translation (instead of the previous Arbitrary Bounded Ranges).

Note also that we do not need any fact whatsoever about addition, except
that embodied in Bounded Time Translation.

THEOREM 8.1. Linearity + Transitions + Bounded Time Translation + Transition
Similarity interprets ZFC + "there exists a subtle cardinal" and is
interpretable in ZFC + "there exists an almost ineffable cardinal". This is
provable in EFA. 

THEOREM 8.2. Linearity + Transitions + Bounded Time Translation + Tail
Transition Similarity interprets ZFC + "for all x containedin omega, x#
exists" and is interpretable in ZFC + "there exists a measurable cardinal".
This is provable in EFA.

THEOREM 8.3. Linearity + Transitions + Bounded Time Translation + Tail
Transition Similarity + Transition Accumulation interprets ZFC + "there
exists a measurable cardinal kappa with kappa many measurable cardinals
below kappa" and is interpretable in ZFC + "there exists a measurable
cardinal kappa with normal measure 1 measurable cardinals below kappa". This
is provable in EFA.

THEOREM 8.4. Linearity + Transitions + Bounded Time Translation + Tail
Transition Similarity + Strong Transition Accumulation interprets ZFC +
"there exists a measurable cardinal kappa with normal measure 1 measurable
cardinals below kappa (order >= 2)" and is interpretable in ZFC + "there
exists a measurable cardinal kappa of order >= 3". This is provable in EFA.

NOTE: With regard to Theorem 8.4, see the NOTE at the beginning of this
posting.

We would like to know that these theories are compatible with substantial
principles concerning time and addition. This turns out to be the case, as
we see in the next two sections.

9. PERSISTENTLY VARYING BIT.

In this section, we weaken Bounded Time Translation considerably to meet
objections concerning what is viewed as 'unrealistic' bit variation.

The idea is to reflect the view that a varying bit must be persistent - or
alternatively, that one is only interested in persistently varying bits.

Specifically, the value of the bit at any time persists up to some later
time. 

We say that a range of times is persistent if and only if for any time t
there exists t1 > t such that i) if t lies in the range of times then every
time in the interval [t,t1) lies in the range of times; if t does not lie in
the range of times then no time in the interval [t,t1) ies in the range of
times. 

Formally, let t1 not appear in phi. The formula "phi is persistent on the
variable t" is 

(forall t)(therexists t1 > t)(for all t2)(t <= t2 < t1 implies (phi iff
phi[t/t2])).  

PERSISTENT TIME TRANSLATION. For any time b and persistent range of times,
there exists a translation time c such that any time before b lies in the
range of times if and only if the bit at time b+c is 1.

PERSISTENT TIME TRANSLATION. (phi is persistent on the variable t) implies,
(therexists c)(forall t < b)(phi iff P(t+c)), where phi is a formula of
L(<,T,P,+) in which c,t1 do not appear.

The idea can be given in two closely related alternative forms:

a. Any possible behavior of a varying bit over a bounded time interval will
occur + the behavior of a varying bit must be persistent.
b. Any possible behavior of a persistently varying bit over a bounded time
interval will occur.

We cannot carry out the development in section 8 with this fundamentally
weakened Time Translation axiom scheme. However, we can carry it out if we
add 

ADDITION. y < z implies x+y < x+z.

ORDER COMPLETENESS. Every nonempty range of times with an upper bound has a
least upper bound. Here we use L(<,T,P,+) to present the nonempty range of
times. 

THEOREM 9.1. Linearity + Addition + Order Completeness + Transitions +
Persistent Time Translation + Transition Similarity interprets ZFC + "there
exists a subtle cardinal" and is interpretable in ZFC + "there exists an
almost ineffable cardinal". This is provable in EFA.

THEOREM 9.2. Linearity + Addition + Order Completeness + Transitions +
Persistent Time Translation + Tail Transition Similarity interprets ZFC +
"for all x containedin omega, x# exists" and is interpretable in ZFC +
"there exists a measurable cardinal". This is provable in EFA.

THEOREM 9.3. Linearity + Addition + Order Completeness + Transitions +
Persistent Time Translation + Tail Transition Similarity + Transition
Accumulation interprets ZFC + "there exists a measurable cardinal kappa with
kappa many measurable cardinals below kappa" and is interpretable in ZFC +
"there exists a measurable cardinal kappa with normal measure 1 measurable
cardinals below kappa". This is provable in EFA.

THEOREM 9.4. Linearity + Addition + Order Completeness + Transitions +
Persistent Time Translation + Tail Transition Similarity + Strong Transition
Accumulation interprets ZFC + "there exists a measurable cardinal kappa with
normal measure 1 measurable cardinals below kappa (order >= 2)" and is
interpretable in ZFC + "there exists a measurable cardinal kappa of order >=
3". This is provable in EFA.

NOTE: With regard to Theorem 8.4, see the NOTE at the beginning of this
posting.

10. NAIVE TIME.

In sections 8 and 9, we use an addition function. In section 9, we used some
properties of <,+. These properties are fragments of a natural theory of
Naive Time, which is of interest in its own right.

In sections 8,9, we can add Naive Time to all of the theories considered,
and obtain the same results.

Naive Time uses <,+ (with identity). When we apply it, we will generally
have a larger language, and possibly sorts in addition to the time scale
sort.

NAIVE LINEARITY. < is a linear ordering with left endpoint and no right
endpoint.

NAIVE COMPLETENESS. Every range of times with an upper bound has a least
upper bound. Here we use L(<,+), or the underlying language of the theory
being axiomatized, to present the nonempty range of times.

NAIVE ADDITION. For every x, the function x+y of y is strictly increasing
from all points onto the points >= x. We call this the translation function
at x. 0+x = x. x+(y+z) = (x+y)+z. Here 0 is the left endpoint.

This completes the presentation of the axioms of Naive Time.

Here are some consequences of Naive Time.

THEOREM 10.1. Every nonempty range of times has a greatest lower bound. Here
we use L(<,+) to present the nonempty range of times, or whatever the
underlying language of the theory being considered.

THEOREM 10.2. If x <= y then there is a unique z such that x+z = y.

THEOREM 10.3. 0+x = x+0 = x. y < z iff x+y < x+z. y = z iff x+y = x+z. For y
> 0, x+y is the least strict upper bound of the x+z, z < y. x <= y implies
x+z <= y+z. 

Naive Time splits into two branches.

DISCRETENESS. There is an immediate successor of the left endpoint.

DENSITY. There is no immediate successor of the left endpoint.

THEOREM 10.4. Naive Time + Discreteness proves every point has an immediate
successor. Every nonempty range of values has a least element. Here we use
L(<,+), or the underlying language of the theory being axiomatized, to
present the nonempty range of times.

THEOREM 10.5. Naive Time + Density proves that between any two points there
is a third.

Everywhere through sections 1-9, we can add Naive Time + Discreteness to the
various axiom systems considered and obtain the same results. The same is
true of Naïve Time + Density.

11. EPOCHS REPLACING TRANSITIONS.

In all of the theories thus far, we have used a unary predicate P on the
time scale, where P(t) means "t is a transition". The idea is that
transition points mark out epochs.

We view this as a small step towards a fully mereological reworking of our
results. See Section 12 below.

However, we can take the view that changing epochs are not marked by single
points. Thus epochs are regions of time.

Under this approach, instead of the unary predicate T, we have a binary
relation E, where E(x,y) means that x,y are in the same epoch. Thus we have
the axiom

EPOCHS. E forms an equivalence relation, where every equivalence class under
E forms a bounded interval (however, the endpoints of these equivalence
classes may or may not exist).

Transition Similarity is replaced by

EPOCH SIMILARITY. Any true statement involving two given times and some
point from a later epoch, is also true about the two given times and some
point from any later epoch. Here we do not allow E to be used in the true
statement.

Tail Transition Similarity is replaced by

TAIL EPOCH SIMILARITY. Any true statement involving two given times remains
true if we hypothetically remove those times that lie in some bounded
interval of epochs after the two given times. Here we allow E to be used in
the true statement.

Transition Accumulation is replaced by

EPOCH ACCUMULATION. There is an epoch which is a limit of earlier epochs.

The results conform to the following analogies.

Transitions: Epochs.
Transition Similarity: Epoch Similarity.
Tail Transition Similarity: Tail Epoch Similarity.
Strong Transition Accumulation: Epoch Accumulation.

Transition Accumulation does not have an obvious analog in the epoch
formulation.

NOTE: With regard to Theorem 8.4, see the NOTE at the beginning of this
posting.

12. MERELOGICAL DEVELOPMENT.

To be continued.

**********************************

I use http://www.math.ohio-state.edu/%7Efriedman/ for downloadable
manuscripts. This is the 295th in a series of self contained numbered
postings to FOM covering a wide range of topics in f.o.m. The list of
previous numbered postings #1-249 can be found at
http://www.cs.nyu.edu/pipermail/fom/2005-June/008999.html in the FOM
archives, 6/15/05, 9:18PM. NOTE: The title of #269 has been corrected from
the original.

250. Extreme Cardinals/Pi01  7/31/05  8:34PM
251. Embedding Axioms  8/1/05  10:40AM
252. Pi01 Revisited  10/25/05  10:35PM
253. Pi01 Progress  10/26/05  6:32AM
254. Pi01 Progress/more  11/10/05  4:37AM
255. Controlling Pi01  11/12  5:10PM
256. NAME:finite inclusion theory  11/21/05  2:34AM
257. FIT/more  11/22/05  5:34AM
258. Pi01/Simplification/Restatement  11/27/05  2:12AM
259. Pi01 pointer  11/30/05  10:36AM
260. Pi01/simplification  12/3/05  3:11PM
261. Pi01/nicer  12/5/05  2:26AM
262. Correction/Restatement  12/9/05  10:13AM
263. Pi01/digraphs 1  1/13/06  1:11AM
264. Pi01/digraphs 2  1/27/06  11:34AM
265. Pi01/digraphs 2/more  1/28/06  2:46PM
266. Pi01/digraphs/unifying 2/4/06  5:27AM
267. Pi01/digraphs/progress  2/8/06  2:44AM
268. Finite to Infinite 1  2/22/06  9:01AM
269. Pi01,Pi00/digraphs  2/25/06  3:09AM
270. Finite to Infinite/Restatement  2/25/06  8:25PM
271. Clarification of Smith Article  3/22/06  5:58PM
272. Sigma01/optimal  3/24/06  1:45PM
273: Sigma01/optimal/size  3/28/06  12:57PM
274: Subcubic Graph Numbers  4/1/06  11:23AM
275: Kruskal Theorem/Impredicativity  4/2/06  12:16PM
276: Higman/Kruskal/impredicativity  4/4/06  6:31AM
277: Strict Predicativity  4/5/06  1:58PM
278: Ultra/Strict/Predicativity/Higman  4/8/06  1:33AM
279: Subcubic graph numbers/restated  4/8/06  3:14AN
280: Generating large caridnals/self embedding axioms  5/2/06  4:55AM
281: Linear Self Embedding Axioms  5/5/06  2:32AM
282: Adventures in Pi01 Independence  5/7/06
283: A theory of indiscernibles  5/7/06  6:42PM
284: Godel's Second  5/9/06  10:02AM
285: Godel's Second/more  5/10/06  5:55PM
286: Godel's Second/still more  5/11/06  2:05PM
287: More Pi01 adventures  5/18/06  9:19AM
288: Discrete ordered rings and large cardinals  6/1/06  11:28AM
289: Integer Thresholds in FFF  6/6/06  10:23PM
290: Independently Free Minds/Collectively Random Agents  6/12/06  11:01AM
291: Independently Free Minds/Collectively Random Agents (more)  6/13/06
5:01PM 
292: Concept Calculus 1  6/17/06  5:26PM
293: Concept Calculus 2  6/20/06  6:27PM

Harvey Friedman