[FOM] 207:On foundations of special relativistic kinematics 2

[Harvey Friedman]

Continuation from posting #206.

We now want to start crawling with some theoretical (as opposed to
observational) foundations of SRK (special relativistic kinematics).

Recall that I said there are probably hundreds of papers aiming to "derive
the Lorentz transformations", and so there is going to be at least a lot of
overlap with existing work.

But note just how closely related, in style, this treatment is with f.o.m.

MATHEMATICAL AXIOMATIZATION AND AUTONOMOUS AXIOMATIZATION.

I wish to draw a distinction between two kinds of first order
axiomatizations of a physical theory - or for that matter any theory with
nonmathematical components.

In *first order mathematical axiomatization*, all of mathematics is
completely taken for granted, requiring no axioms whatsoever, and all axioms
are in first order predicate calculus, generally with equality.

This is implemented as follows. A special sort is reserved for all
mathematical entities, and special constant, relation, and function symbols
are reserved for purely mathematical notions involving only mathematical
entities. Other sorts are reserved for physical entities. All axioms are in
an appropriate many sorted first order predicate calculus.

In the most obvious implementations, a single sort is reserved for sets, and
a single binary relation symbol epsilon is reserved for membership. The full
power of the usual set theoretic foundations of mathematics is assumed in
the background.

The so called "mathematical models" of the theory are to satisfy the first
order axioms in the usual sense in f.o.m. - but

*where the interpretation of the sort reserved for mathematical entities
must in fact be, exactly, the intended mathematical entities.*

Furthermore, the 

*purely mathematical, reserved, constant, relation, and function symbols
must have their intended interpretations.*

In practice, one does not need anything like the full mathematical universe,
or the full universe of sets, for the axiomatization of at least present day
physical science. Frequently one may wish to be explicit about just what
mathematics is involved. In this case, one typically sees one or more
reserved sorts, reserved for certain important kinds of mathematical
entities - together with the important associated mathematical relations and
operations. E.g., a sort reserved for real numbers, with the usual symbols
for the ordered field operations.

Because the so called mathematical models are required to be "correct" on
the mathematical part, validity is very badly behaved in general, even for
finitely axiomatized purely universal theories. In general, there cannot be
any reasonable complete set of axioms - obviously, even for the purely
mathematical part. 

However, this does not mean that there cannot be very informative and
striking logical properties of such first order systems, under this
"mathematically correct" semantics.

We see a clear opening here for striking logical behavior in specific cases,
but also, I believe, for some striking general theory.

In autonomous axiomatizations, no special logical status is given to purely
mathematical notions. Here we are talking about entirely first order
axiomatizations in many sorted predicate calculus, generally with equality,
with the ordinary notion of model. For emphasis, we will call these

autonomous models

as they do not take mathematics for granted.

In the case where the only relevant mathematics is (built explicitly out of)
the ordered field of real numbers, the obvious move is to simply incorporate
one of the striking complete axiomatizations of it into the axiomatization
of the physical theory.

I defined T(max) in my posting #205, First Order Extremal Clauses 1/18/04
2:25PM, for use in the formulation of autonomous axiomatizations.

In the case of mathematical axiomatizations, we can often get away without
T(max), but rather the extremal clause

*there is no proper extension of this system, preserving the mathematical
sort.*

This will be used in the first axiomatization (mathematical axiomatization)
of special relativistic kinematics, in the next posting.

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

I use http://www.mathpreprints.com/math/Preprint/show/ for manuscripts with
proofs. Type Harvey Friedman in the window.
This is the 207th 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-149 can be found at
http://www.cs.nyu.edu/pipermail/fom/2003-May/006563.html  in the FOM
archives, 5/8/03 8:46AM. Previous ones counting from #150 are:

150:Finite obstruction/statistics  8:55AM  6/1/02
151:Finite forms by bounding  4:35AM  6/5/02
152:sin  10:35PM  6/8/02
153:Large cardinals as general algebra  1:21PM  6/17/02
154:Orderings on theories  5:28AM  6/25/02
155:A way out  8/13/02  6:56PM
156:Societies  8/13/02  6:56PM
157:Finite Societies  8/13/02  6:56PM
158:Sentential Reflection  3/31/03  12:17AM
159.Elemental Sentential Reflection  3/31/03  12:17AM
160.Similar Subclasses  3/31/03  12:17AM
161:Restrictions and Extensions  3/31/03  12:18AM
162:Two Quantifier Blocks  3/31/03  12:28PM
163:Ouch!  4/20/03  3:08AM
164:Foundations with (almost) no axioms, 4/22/0  5:31PM
165:Incompleteness Reformulated  4/29/03  1:42PM
166:Clean Godel Incompleteness  5/6/03  11:06AM
167:Incompleteness Reformulated/More  5/6/03  11:57AM
168:Incompleteness Reformulated/Again 5/8/03  12:30PM
169:New PA Independence  5:11PM  8:35PM
170:New Borel Independence  5/18/03  11:53PM
171:Coordinate Free Borel Statements  5/22/03  2:27PM
172:Ordered Fields/Countable DST/PD/Large Cardinals  5/34/03  1:55AM
173:Borel/DST/PD  5/25/03  2:11AM
174:Directly Honest Second Incompleteness  6/3/03  1:39PM
175:Maximal Principle/Hilbert's Program  6/8/03  11:59PM
176:Count Arithmetic  6/10/03  8:54AM
177:Strict Reverse Mathematics 1  6/10/03  8:27PM
178:Diophantine Shift Sequences  6/14/03  6:34PM
179:Polynomial Shift Sequences/Correction  6/15/03  2:24PM
180:Provable Functions of PA  6/16/03  12:42AM
181:Strict Reverse Mathematics 2:06/19/03  2:06AM
182:Ideas in Proof Checking 1  6/21/03 10:50PM
183:Ideas in Proof Checking 2  6/22/03  5:48PM
184:Ideas in Proof Checking 3  6/23/03  5:58PM
185:Ideas in Proof Checking 4  6/25/03  3:25AM
186:Grand Unification 1  7/2/03  10:39AM
187:Grand Unification 2 - saving human lives 7/2/03 10:39AM
188:Applications of Hilbert's 10-th 7/6/03  4:43AM
189:Some Model theoretic Pi-0-1 statements  9/25/03  11:04AM
190:Diagrammatic BRT 10/6/03  8:36PM
191:Boolean Roots 10/7/03  11:03 AM
192:Order Invariant Statement 10/27/03 10:05AM
193:Piecewise Linear Statement  11/2/03  4:42PM
194:PL Statement/clarification  11/2/03  8:10PM
195:The axiom of choice  11/3/03  1:11PM
196:Quantifier complexity in set theory  11/6/03  3:18AM
197:PL and primes 11/12/03  7:46AM
198:Strong Thematic Propositions 12/18/03 10:54AM
199:Radical Polynomial Behavior Theorems
200:Advances in Sentential Reflection 12/22/03 11:17PM
201:Algebraic Treatment of First Order Notions 1/11/04 11:26PM
202:Proof(?) of Church's Thesis 1/12/04 2:41PM
203:Proof(?) of Church's Thesis - Restatement 1/13/04 12:23AM
204:Finite Extrapolation 1/18/04 8:18AM
205:First Order Extremal Clauses 1/18/04 2:25PM
206:On foundations of special relativistic kinematics 1 1/21/04 5:50PM