[FOM] methodological thesis

[Mitch Harris]

On Wed, Apr 30, 2008 at 1:23 AM, Rupert McCallum
<rupertmccallum at yahoo.com> wrote:
>  --- Harvey Friedman <friedman at math.ohio-state.edu> wrote:
>
>  > I would like to discuss a methodological issue related to philosophy.
>  >
>  > THESIS. Suppose that a philosophical paper P, in any part of
>  > philosophy, consisting of informal prose, without new formalisms or
>  > new theorems or new formal conjectures, represents intellectual
>  > progress. Then there exists a paper Q with the following properties.
>  > 1. Q focuses on associated new formal definitions, new formalisms,
>  > new
>  > formal conjectures, and new theorems.
>  > 2. Q has a relatively small amount of informal prose.
>  > 3. Q can be written using the current level of practice in formal
>  > methods and foundational thinking.
>  > 4. P is fully subsumed by Q.
>  >
>  > The challenge to me would be to subsume the proposed P paper into the
>  > subsuming Q paper.
>
>  You say "any part of philosophy", so that gets me thinking about
>  examples in normative ethics.
...
> But doing a subsuming Q paper; well, I'd be interested in what that would look like.

An example: Spinoza's Ontology, by Jan Hladik

  http://lat.inf.tu-dresden.de/research/papers/2004/Hladik-WSPI-04.pdf

Abstract. We examine the possibility of applying knowledge represen-
tation and automated reasoning in the context of philosophical ontology.
For this purpose, we use the axioms and propositions in the first book
of Spinoza's Ethics as knowledge base and a tableau-based satisfiability
tester as reasoner. We are able to reconstruct most of Spinoza's system
with formal logic, but this requires additional axioms which are assumed
implicitly by Spinoza. This study illustrates how tools developed in com-
puter science can be of practical use for philosophy.

-- 
Mitch Harris