[Agda] Fwd: Can intuitionistic type theory express derivations of physical equations more strictly?

[Hidekazu IWAKI]

Sorry. I didn't send the reply to the mailing list.
---------- Forwarded message ----------
From: Hidekazu IWAKI <i.hidekazu at gmail.com>
Date: 2017-09-29 23:49 GMT+09:00
Subject: Re: [Agda] Can intuitionistic type theory express derivations
of physical equations more strictly?
To: Mario Castelán Castro <marioxcc.MT at yandex.com>


2017-09-29 1:38 GMT+09:00 Mario Castelán Castro <marioxcc.MT at yandex.com>:
> On 28/09/17 07:38, Hidekazu IWAKI wrote:
>> I'd like to describe a physical system with the intuitionistic type
>> theory(not computer simulation).  I wonder if it is possible to convince
>> readers that all famous physical equations have evenly a strict derivation.
>> So I want to confirm it with the type theory.
>>
>> In order to refer, I'm looking about such a system, a plot or a
>> interpretation of value with type in physics. Does anyone know such a
>> information?
>
> Hello.
>
> First, I must note that my knowledge of constructive type theory is near
> null. I am subscribed to this mailing list because I am interested in
> learning Agda and its underlying logic but so far I have not allocated
> the required time.
>

Thank you for your honesty! I also don't have enough knowledge about
the type theory. I cannot yet understand Martin-Löf's papers enough.
If anything, I prefer to Göran Sundholm's philosophical papers at this
time. So, since asking makes me think more about some topics of it, I
did to understand more better. To tell the truth, I have little
knowledge of Agda. Of course, I have programmed in Haskell years ago.

> What specific famous physical equations do you have in mind?
>
I understand, as you said, that to specify worrying factors makes this
question more concrete; however, I have no equation proposed and don't
want to be misunderstood.

> I have been thinking about formalizing (in HOL4) a derivation of the
> Lorentz transform from invariance or symmetry axioms, something like the
> textbook derivation (in special relativity) of the Lorentz transform
> based on the invariance of the speed of light and isotropy of space.
> Having done this, the natural continuation is to follow with the laws of
> relativistic mechanics and eventually electromagnetics. Unfortunately, I
> need more background in analysis before undertaking the part about
> electromagnetics.
>
Sorry. I do not know HOL4 and not realize what the point is. But as
far as I can tell you that each theory has a different origin. So
there is not a natural continuation, probably. Einstein developed the
eventually electromagnetics in implicit and mechanics of
electron(1907); however so-called "relativistic
mechanics"(non-Newtonian mechanics) was developed by Gilbert Newton
Lewis and his coworker Richard Chess Tolman. Although Lewis and
Tolman's mechanics rested on Einstein's 1907 paper, Lewis constructed
it based on another principle at the beginning, so there are some
conceptual mismatch between Einsterin's theory and their
mechanics.(e.g. "rest mass". Because Lewis believe the absolute space
existence at the beginning.)

=== References ===
Gilbert N. Lewis "A revision of the Fundamental Laws of Matter and Energy"
https://en.wikisource.org/wiki/A_revision_of_the_Fundamental_Laws_of_Matter_and_Energy

Gilbert N. Lewis and Richard C. Tolman "The Principle of Relativity,
and Non-Newtonian Mechanics"
https://www.jstor.org/stable/pdf/20022495.pdf?refreqid=excelsior:03dbb0a71b64f57611cdac1adaf32035
=======
> (Side note: Poincaré and Lorentz formulated special relativity; Einstein
> just took what these men had already discovered, added his own
> metaphysical interpretation and published it as if it was his sole work;
> in other words, plagiarism combined with philosophical bullshit)
>
You have a sure eye. I think that it is very important to distinguish
what Einstein was doing or not doing in order to understand the 20th
physics.

Sincerely,
IWAKI

> --
> Do not eat animals; respect them as you respect people.
> https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>