I am no longer a dogmatic formalization-ist

[gustavolacerda]

Last week, I had an excellent chat with Terry Stewart over AIM. We covered:
* cognitive modeling
* "neural compilers"
* philosophy of science (empirical vs theoretical models in physics and cogsci, unification/integration, predictions vs explanations, reduction). See his excellent paper here

Comments

Defending myself (slightly)

[anonymous]

This is the afore-mentioned Terry, attempting to defned himself a little bit.

To a certian degree, yes I do think that a lot of what is produced by universities doesn't count as a theory. However, that doesn't mean that I think those non-theory parts of research are useless. Instead, I'd say more that they are the necessary foundations on which a theory can be built.

But my main point is that, until you can specify a theory in such a way that it has non-ambiguous uses, then something is missing. This may be specifying it mathematically, or via logic, or via a computer program -- I don't care which (but as things get more complicated, I think computer programs are the way to go). Theories based on boxes and arrows, or verbal descriptions that don't define their underlying terms are useful in that they are intermediate stages, but I think the goal should be something more concrete. And once they are concrete, I think we get huge advantages (think of the change in physics once it was placed on a mathematical foundation).

Re: Defending myself (slightly)

[gustavolacerda]

hey, I was just going to email you about this. Hope you don't mind me blogging the conversation.

[rdore]

I like the idea of the following proof-checking game:
* Proposer needs to defend a theorem that he/she does or does not have a proof of.
* Skeptic tries to make Proposer contradict himself, or state a falsity.

Since formal proofs are typically too long (and unpleasant) to read in one go (see de Bruijn factor), this method only forces Proposer to formalize one branch of the proof tree. Since Skeptic can choose what branch this is, he should be convinced that Proposer really has a proof (even if it's not fully formalized).

What you're talking about sounds a lot like an interactive proof system, which is a well studied branch of complexity theory.