more FormalBlog

Mathematicians informally talk about formal structures. The object of their reasoning is formal, but their method is not.

Logicians (except those "logicians" who are only interested in applications, like myself) are mathematicians whose formal structures are logics and models. Like mathematicians, their method is informal.

---

Me and Henrik just did some "conceptual analysis" for Philosophy of Mathematics, and proved that "realism-in-truth-value leads to a normative philosophy of mathematics". (i.e. m |= forall phi (phi \/ ~phi) => exists F_mu (Normative (F_mu) /\ m |= F_mu) )

To help you read it:

x |= y means "x believes y"

m : Mathematician
F_mu : Philosophy of Mathematics (sorry, no dependent types yet)
Normative : Philosophy -> t (predicate over philosophies)

Also, we used:

Definition: A philosophy F is normative iff it contains at least one non-empirical statement.
Axiom: all universal statements about infinite sets are non-empirical.

I just wish we had a hypertext authoring tool to connect formal and informal, as described here.

My dynamic approach advocates:
* mixing formal and informal (i.e. not-yet-formal) terms
* allowing for revision of one's ontology... a modular design helps here!
* definitions can come later, as the proof demands them.

I love doing this: I am in love with modeling reasoning processes. Can anyone think of a good name for this gradual formalization approach? "Conceptual analysis"? "Rational analysis"?