Formal Objectivism!

from http://www.andrej.com/objectivism/

(1) |- man(x) <==> animal(x) & rational(x) [definition]
(2) |- man(y) [hypothesis]
(3) |- y = y [by Axiom of Identity]
(4) |- rational(y) [by (1) and (2)]
(5) |- knows(y, y=y) [by (3) and (4)]
(6) |- rational(y) & value(y, v) ==> v [Rational Value Theorem]
(7) |- egoist(x) <==> value(x, x = x) [definition of egoism]
(8) |- not(egoist(y)) ==> not(value(y, y = y)) [from (7) instantiating x = y]
(9) |- not(egoist(y)) ==> value(y, not(y = y)) [by not-propagation]
(10)|- not(egoist(y)) ==> not(y = y) [by (9) and (6)]
(11)|- not(egoist(y)) ==> false [by (10) and (3)]
(12)|- egoist(y) [by (11) ad absurdum]
(13)|- man(y) ==> egoist(y) [by (2) and (12) by ==> introduction]

The author happens to be a logician with a "good" constructivist philosophy, and (evidently) a good sense of humour.

a framework for doing formal science

So, in my goal of formal theories (since I'm still brainstorming), I'm throwing together a bunch of ideas uncritically:

Here, the goal is a framework for doing formal science.

Why
* I used to study physics. I liked it a lot. I quit physics because it was often not clear what they meant: from classical to quantum mechanics, things were never very clear. One-on-one help sessions were resource-wasteful and often didn't help, due to differences in style (I have quite an extreme, inflexible, logical learning style). I even became skeptical that they understood their stuff. Frustrated, I decided to become a mathematician.

* Among mathematicians, after getting good at proofs, I was became confused and bored, because their proofs were vague, repetitive and full of mental busy work, and what we were trying to do in each bit wasn't clear, so I decided to become a logician.

(By the way, textbooks were never much better: however well things are organized, they are a far cry from what I would consider optimal. And it's not necessarily because of the static medium.)

* Even with logicians, I was disappointed because they don't treat the meta-language with the same rigor as the object language. They are basically ordinary mathematicians who study logic. The next obvious step would be to become a proof theorist.

But now I'm conscious of the problem, and I don't want to take it any further: the problem is writing down everyday arguments in an unambiguous and organizable manner. Formal theories are what I want. And interacting with these formal theories / interactively constructing proof objects seems like TheRightThing. Proof Assistants in Mathematics

Other advantages:
* Formal proofs can be written in standard "idioms" (I don't mean just questions of normalization, but also layout), and be thus, easier to read once learned. The present chaotic mix of styles is certainly far from optimal.
* Not only can you have proof assistants, but also proof visualization tools, making arguments even easier to understand.

However, someone beat me to writing the first science book with a formal language (van Benthem-Jutting had translated an analysis book into AUTOMATH, but that was math). Here is a quote, stating their philosophy:

Sussman - Structure and Interpretation of Classical Mechanics (Ch.2)

Classical mechanics is deceptively simple. It is surprisingly easy to get the right answer with fallacious reasoning or without real understanding. Traditional mathematical notation contributes to this problem. Symbols have ambiguous meanings that depend on context, and often even change within a given context.1

For example, a fundamental result of mechanics is the Lagrange equations. In traditional notation the Lagrange equations are written


The Lagrangian L must be interpreted as a function of the position and velocity components qi and i, so that the partial derivatives make sense, but then in order for the time derivative d/dt to make sense solution paths must have been inserted into the partial derivatives of the Lagrangian to make functions of time. The traditional use of ambiguous notation is convenient in simple situations, but in more complicated situations it can be a serious handicap to clear reasoning. In order that the reasoning be clear and unambiguous, we have adopted a more precise mathematical notation. Our notation is functional and follows that of modern mathematical presentations.2 An introduction to our functional notation is in an appendix.

I am extremely frustrated by having to prove things theorem where things are not explicitly quantified, or quantified with ambiguous words like "any" (depending on the context). Most experts don't bother to make things explicit because they assume it's understood.


---
Related Notes:

Things I've constantly have to remind students / myself. Finding your way when you are lost:
* What are you trying to do?
* Do you understand what everything means?
* Abstract away from the math: focus on the big picture, the concepts. Once you have the concepts, it's easier to fill in the computations/calculations later.
* Whenever I learn new theory (e.g. category theory), I want a formal axiomatic system for working with it. If this is not specified, an informal "proof method" will do, otherwise it's not clear at all what level of explanation is being asked for in the proof. Why do I seem to be alone with these concerns?

scam of the day

Pay to take surveys at http://www.wcsurveys.com

I wonder what exactly they do (or don't do) after they charge the credit cards. I imagine they just give you a useless set of pointers as VERY IMPORTANT INFORMATION, kinda like MLM.