Re: unison vectors (meta discussion)

Hi Gene,

(response to posts on Tuning list about defining
unison vectors).

Of course one would need to tread more carefully
if one wanted to look at a lattice maybe in the
context of the BP scale and treat the 3/1
as the underlying equivalence, and 2/1
and 5/1 as the lattice vectors.

In that context it might help to clarify
things to refer to it as a pitch class
lattice. But then again, I think
it might be clearer to say
just that elements a 3/1 apart
are treated as the "same" element
in the lattice.

After all mathematicians speak like
that too. They know about the notion
of an equivalence class, but they
fall into natural language too so long
as they know that what they say is
understood.

Actually a lot of even mathematical
work involves some hand waving saying
for instance (if the mathematician
stops to be more rigorous in his
presentation)

"This could all be written out
using well formed formulae in
first order predicate calculus
because of ..." - but only logicians
ever formulate proofs in that
form and proofs like that are
exceedingly long and cumbersome
so even logicians leave out steps
and do some hand-waving.

No-one else even attempts
to present a logically
complete proof with all the
details exactly spelt out
like that. Nearly all
proofs in Maths have a high
element of intuitive understanding
required to follow the details
of the proof - and then
the idea is that in principle
it could all be written out
rigorously since we understand
and can see why it is true and
know that true deductions can
be written out rigorously
like that - that our basic
concepts we use have been formulated
in such a way that they could be
writen out - that is all the
average mathematician needs
or cares to know about the
true underlying foundations of his subject.
and rightly so.

I'm not even sure myself if the
completely written out detailed
proof is the truer or better one.
really. It came last historically
and for centuries mathematicians
got on perfectly well without
a complete analysis of the logical
foundations of the concepts they
used.

Robert

--- In metatuning@yahoogroups.com, "Robert Walker" <robertwalker@n...>
wrote:

> No-one else even attempts
> to present a logically
> complete proof with all the
> details exactly spelt out
> like that.

The automatic theorem provers do; the Robbins conjecture was proven by
machine and the proof invovled the construction and verification of a
formal proof.

> I'm not even sure myself if the
> completely written out detailed
> proof is the truer or better one.

There's something to be said for the notion that a proof framed in
such a way that it can be machine verified is a plus. It will take a
while to do that to Bourbaki, I suppose.

Hi Gene,

> > No-one else even attempts
> > to present a logically
> > complete proof with all the
> > details exactly spelt out
> > like that.

> The automatic theorem provers do; the Robbins conjecture was proven by
> machine and the proof invovled the construction and verification of a
> formal proof.

Yes true, if it can be machine verified then it has a formal proof
- even if the verification doesn't actually expand it completely
into a formal proof, it verifies that a formal proof exists
which is as good as actually constructing one.

> There's something to be said for the notion that a proof framed in
> such a way that it can be machine verified is a plus. It will take a
> while to do that to Bourbaki, I suppose.

Yes surely.

I was just thinking about a good example of omitted axioms
and remembered the ones left out of Euclid. Do you remember
those?

For instance the one that if a line intersects one of
the sides of a triangle then he assumes that it must
interesect one of the other sides, somewhere in book 1.
It can't be derived from his other
axioms though it is intuitively obvious that
if a line enters a triangle then it has to leave
it through one of its sides. No-one noticed the
omission until Hilbert's work on an axiom
system for geometry in 1899.

Presumably you could make a consistent "geometry"
in which that doesn't get assumed - I wonder
what it wuold be like - assume there exists
a line that enters a triangle and never leaves
it... Sort of a singularity in euclidean
geometry. You could almost imagine an axiom
like that being used in string theory
or some such exotic geometry.

Robert

--- In metatuning@yahoogroups.com, "Robert Walker" <robertwalker@n...>
wrote:

> I was just thinking about a good example of omitted axioms
> and remembered the ones left out of Euclid. Do you remember
> those?

I'd heard about that somewhere and as a result in my high school
geometry class I gave the teacher hell at the beginning trying to make
him prove everything from the axioms. This amused the other kids in
the class, since it slowed things way down, but then he banned such
digressions and I gave up and sat around reading a calculus book in
class to keep from getting bored.

> Presumably you could make a consistent "geometry"
> in which that doesn't get assumed - I wonder
> what it wuold be like - assume there exists
> a line that enters a triangle and never leaves
> it... Sort of a singularity in euclidean
> geometry. You could almost imagine an axiom
> like that being used in string theory
> or some such exotic geometry.

It would be interesting to find Hilbert's axioms and take a look at
what models you could get by leaving some of them out. Sounds like a
great thesis topic; you could get someone to graduate with a PhD and a
thesis on elementary synthetic geometry.