Formal Objectivism!

[gusl]

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.

Comments

[jcreed.livejournal.com]

Yes, Andrej Bauer's a really cool guy. He TAed one of the category theory courses I took a few years ago when he was still here at CMU.

[gustavolacerda.livejournal.com]

Hey, btw, I have a friend here who's probably going to CMU to do a PhD in ML or Comp. Linguistics. I think he would like to ask you a few questions.

Re:

[jcreed.livejournal.com]

sure, have him email me at my lj username dot andrew dot cmu dot edu.

Re:

[rdore.livejournal.com]

i believe that first dot is more than like an at

Re:

[dr4b]

Hee. I drove Andrej Bauer's car once. Of course, he had sold it to Kevin Watkins by then.