Formal Models of Aspects of Wittgenstein's Tractatus
Overview
A Formal model of semantics similar to aspects of the Tractatus.
A form is modelled as a constructor.
Introduction
Purposes

The main purposes are:

First
to show that some aspects of Wittgenstein's Tractatus can be illuminated by formalisation.
Second
to make a connect between the X-Logic modelling, which is an engineering design activity, and analytic philsophy.
Scope
This model is drawn from a very tiny part of the Tractatus, and the parts on which it is based will be mentioned in the discussion. It is safe to assume that I don't understand most of the rest of the Tractatus, and so its entirely possible that what the rest says is sufficient for those in the know to invalidate this interpretation. So far as I have read the comments of others on what the Tractatus does, the part which is here modelled appears to receive very little attention, and in particular the closeness of the relationship between the Tractatus and the (now) accepted semantics of first order logic is not something I have seen mentioned elsewhere.
Vocabulary
world (1.2)
= set of facts (no things). These appear to be atomic facts since they are asserted to be logically independent (1.21)
state-of-affairs (2.01)
= combination of objects(=things). These are, in a sense, possible facts.
object (2.01)
constituents of states-of-affairs (not of the world)
picture (2.1)
a model of reality (of a state-of-affairs)
form
pictorial (2.15)
the possibility of a structure, what a picture has in common with reality
logical (2.18)
what any picture ("of whatever form") has in common with reality
proposition (3.1)
a picture of reality
thought (3.)
part of a picture of the world, a proposition with sense
language (4.001)
the totality of propositions
The Theory tract
We here introduce the new theory in the context of galactic set theory (though it could have been done in less exotic environs).
xl-sml
open_theory "gst";
set_pc "gst";
force_new_theory "tract";
force_new_pc "tract";

Form
A form is modelled as a constructor.
Forms
We model forms as constructors which take indexed set collections and make some construction from them. To give an excess of abstract generality to the kind of construction which can be made, the codomain of a constructor is the Galactic set theory over the kind of objects in the collection. We require these forms to lose no information. The following predicate sums up these ideas about the modelling of forms:
xl-holconst
is_form: (('i 'a) 'a GS) BOOL
is_form = OneOne
It is intended that forms will always be polymorphic in the type of objects involved, I have no way of saying this formally. This permits exactly the same form to be used in constructing a proposition and a state-of-affairs. In the first case the form is applied to some indexed collection of names and in the second a collection of objects, these two collections having the same type of indexes.

up quick index © RBJ

$Id: tractatus.xml,v 1.1.1.1 2000/12/04 17:24:29 rbjones Exp $