Gustavo Lacerda

I am going to submit my thesis this wednesday afternoon. It will be finished tuesday evening.

Help me stay motivated: criticize! My latest version is very readable, but please criticize anything that is:
* unclear
* gramatically wrong, awkward, hard to read
* unflowy, ugly
* fallacious
* etc.

The topic, again, is about formalizing and automating (Kuhn and Kitcher's concept of) "normal science".

P.S. Those who contributed before or who are contributing now, please tell me what name I should use to acknowledge you. Internet handles are ok with me.

Many thanks.

((IMPLIES (UCM Body1 Pos2 Period1)
  (= (acc Body1) (/ (^ (vel Body1) 2) (distance (pos Body1) Pos2)))) (AXIOM)))

in other words "a = v^2 / r"

This result holds for bodies under uniform circular motion (UCM). Body1 refers to the body. Pos2 refers to the center of the circle traced by Body1 (pos is for "position").

There is an implicit universal quantifier over Body1, Body2, Period1. I wonder if I should make it explicit.
There is also an even more implicit universal quantifier over time, which I don't need to worry about much... until I deal with boundary conditions that quantify over a time domain that's not the universe (i.e. there are times when the equation doesn't hold).

My current system doesn't reason about predicates like UCM, as this would involve formalizing geometry, etc... which would be a thesis in itself. Such reasoning is left to the user: all the system does is keep track of the physical assumptions being made for each derivation (and make a conjunction of them). If those assumptions are contradictory, the user should know that there's no way to interpret the equation derived (or the set of situations where the equation holds is empty).

Given a boundary condition, like (UCM Moon (Pos Earth) Period1), I should be able to do a universal instantiation (UI):

((IMPLIES (UCM Moon (Pos Earth) (UCM-Period Moon Earth))
  (= (acc Moon) (/ (^ (vel Moon) 2) (distance (pos Moon) (pos Earth))))) (AXIOM)))

, where the variable (UCM-Period Moon Earth) is an unknown variable, a handy trick to avoid introducing an existential quantifier.

This is easy to do, by simple variable substitutions.

Combining this with the boundary condition above, (UCM Moon (Pos Earth) (UCM-Period Moon Earth)), we get, by modus ponens (MP):
(= (acc Moon) (/ (^ (vel Moon) 2) (distance (pos Moon) (pos Earth))))

My next and final step is to deal with inter-theoretical relations, reduction, etc. which could properly be called doing physics, unlike the above and the rest of my thesis, which is just symbol-crunching.

To begin doing physics, for example, we can start by noting that (UCM Moon (Pos Earth)) is not true. It's only true in this idealized model. Imagine that this error is only due to relativistic effects... So before we discover special relativity, we have to make do with an empirical model: a model that describes the phenomenon without linking to high-level laws. But can't we do better? Can't we link empirical models to high-level laws?

Yes, yes we can. And we can make these links by borrowing the explanatory power of our well-understood but ultimately incorrect model. Is the old model wrong? Yes! Is it obsolete? No.

Not only do we note that the old model's predictions hold in the limit case for low speeds, but even at high speeds, some relationships between the empirically-observed variables with remain the same as the relationships in the classical model.