Weir's Theory, the mathematical background

Logicians use theories in two ways: they reason about them and they reason within them. When you reason about a theory, you want the theory to be as simple as possible. When you reason within a theory, you want as many bells and whistles as possible.

There is a standard method for having your cake and eating it too: You keep the official theory simple, and introduce the bells and whistles, not as a part of the theory, but as metalinguistic abbreviations for things in the theory.

Example: A typical formalized logic includes only one quantifier, say, %$\exists$%. We then say, at some point, we will write %$\forall$% as an abbreviation for %$\lnot\exists\lnot$%. Thus, our theory still has only one quantifier, but we have the notational convenience of having two.

Weir can't use the standard trick: to show that his theory is coherent, he introduces it in a familiar background theory. However, in that background theory, his theory doesn't work as he wishes: he has an object that is supposed to be the domain of absolutely everything, but, in the background theory, the objects that are "in" that domain form a set, and so there are objects not in it. His solution is to throw away the ladder: after showing the theory coherent in a familiar background theory, he discards that background, and shows how to develop the theory with itself as a background theory. In that development, there is nothing to block his domain of absolutely everything from including absolutely everything. That means that he is developing his theory with a goal of working in it, and so he needs the bells and whistles to actually be in the theory, not just abbreviations expressed in a familiar background theory he wishes to discard. Russell, Hilbert, and others in the early 20th Century developed logical theories as foundations in which they hoped to do mathematics. They therefore formalized the bells and whistles in the theory. Today, no one bothers, and so Weir uses techniques that are unfamiliar.

When can you introduce a name for an object? When you know what the object is, that is, when you have a characterization of the object that shows that there is exactly one such object (that is, that there is at least one such object (existence) and that there is at most one such object (uniqueness)).

Fix a set, call it %$S$%. Every formula %$\phi (x)$% in one free variable defines a unique subset of %$S$%, that we usually, in the metalanguage, call %$\{x\in S:\phi (x)\}$%. In the object language, we just observe that it is easy to prove that there is a unique set %$a$% such that %$\forall y (y\in a\leftrightarrow y\in x\land\phi (y))$%. We don't "officially" give it a name. The proof I just waved at orally is a justification for introducing, for each %$\phi (x)$% the following notation for a function into the language of set theory: %$\{x\in s:\phi (x)\}$%. We then can prove the following facts.

For any %$s$%, for any %$y$%, if %$y\in \{x\in s:\phi (x)\}$%, then %$y\in s$% and %$\phi (y)$%. There is also a converse rule. Using those rules, one can prove that, for any %$s$%, %$\{x\in s:\phi (x)\}$% exists, is unique, and is (for %$S$%) the %$a$% introduced above. What I have done here is different from the procedure I indicated above: instead of introducing %$\{x\in s:\phi (x)\}$% axiomatically as an abbreviation, I found some "rules of inference" that are equivalent to such an introduction. I can them use them instead and introduce %$\{x\in s:\phi (x)\}$% "axiomatically."

We can do the same thing again to introduce "new" properties of objects: associate an object (call it a "property") with every formula with one free variable. Make up a new relation, %$\varepsilon$% that holds between an object and a property if and only if the object has the property. Use a different style of brackets for properties: %$[x\in s:\phi (x)]$%, and introduce the "same" axioms, with curly brackets replaced by square ones and membership signs replaced by "falling under" signs. This is not eliminable by definition. Ordinarily, we would explicate such objects away.

The properties will be different from sets in an important way: any collection is a set, but only collections definable by a formula have been introduced as properties. We have therefore, at least left the possibility open that there are fewer properties than sets.

What I've done above is not exactly what Weir does, since Weir wants "absolutely everything." He introduces properties, not of subcollections of a set, but of the whole domain. He therefore has, not %$[x\varepsilon s:\phi (x)]$% (which doesn't quite make sense), but %$[x:\phi (x)]$%.

We now have a property that can serve as a domain, namely, %$[x:x=x]$%. We also have a problem, namely the property, %$[x:\lnot x\varepsilon x]$%. Weir's system is inconsistent. What to do? He uses one version of Kripke's method of introducing a language that includes its own truth predicate.

In detail, he introduces a third "truth value," using strong Kleene (that is, for example the conjunction of anything false with anything is false, and so on for whatever is determined with some values absent), and closes using monotone induction: the bottom level is ordinary set theory (including set notation). At each subsequent level he adds property descriptors that only use %$\phi$%s from previous levels. At each level, he adds the property axioms and makes everything true that is true on every possible extension of what came earlier. The result is that %$[x:\lnot x\varepsilon x]$% poses no problem, since %$[x:\lnot x\varepsilon x]\varepsilon [x:\lnot x\varepsilon x]$% never gets a truth value.

Weird Philosophy

Weir doesn't like traditional absolutist views because they fail to produce a domain of everything, as claimed: they require hierarchies of domains of what are not counted as things, and that seems, to Weir, to be cheating.

He doesn't like traditional relativist views because he takes them to either be incoherent or to be expressively inadequate.

He does make the interesting remark that the standoff is a kind of Kantian antinomy. That means, at least, that no rational considerations can settle the standoff on one side or the other. We can't hope to find find any considerations along the lines considered that count on either side of the standoff.

I'm inclined to agree. I therefore think we need to turn to considerations other than those connected with the paradoxes if we are to make any progress. Weir draws a different conclusion: the dichotomy results from a common assumption that we can't have it all. The usual way to deal with antinomies is to dissolve them by identifying and rejecting the common assumptions of the two sides that lead to a standoff. Weir therefore tries to show that we can have everything, that is (342), a language L with a well-defined semantics (in particular for quantification) such that consequence, satisfaction, truth, for L are all definable in L, there is a proof system for L that can be proved sound in L, there is a recursive semantics for L expressible in L, there is an object in the domain of L that is the domain of absolutely everything, and we have reasons to think the whole package is reasonable (consistent) that are at least as good as the one we have for the more familiar systems that are widely accepted (that is, set theory, and Tarskian set-theoretic semantics).

In thinking that a theory with such characteristics would eliminate the debate, Weir presumes that the only substantial issues are,

1. Expressive adequacy
2. Semantic adequacy
3. Proof-theoretic tractability: we have a soundness proof

He doesn't take having a complete proof system to be a desideratum. We don't have one, for example, for second-order logic. Having one is certainly nice for some purposes, but no one had one or at least thought that they had one even in cases like that for millenia. It is not, he says, a requirement on a metaphysically and semantically coherent theory.

It is perfectly true that the paradoxes are generally take to block having a language that can provide its own semantics both because of the liar and Russell's and related paradoxes. Relativists often take that to be a critical deficiency of absolutist systems, but it is not where most relativists we have discussed begin. They begin with the "obvious" assumptions required to obtain Russell's paradox and take them to be true. That is, they are, at least implicitly, requiring that any adequate theory must obey some versions of the following principles:

• Every domain is an object, a "collection"
• The objects in any collection that have a definite property themselves form a collection
• The property that a definite collection has in virtue of being a "member" of a definite collection is a definite property

So, let's look at how Weir's theory does. He has a bewildering variety of collection-type roles within his theory. In fact, it is rather odd to see how bewildering it is, given that he has only finitely many and most of the other theories have either infinitely or indefinitely many (Fine, modal).

One type he has is ordinary sets on a single domain. He also has second-order quantification over his domain. I'll call the extensions of the one-place second-order variables classes.

The class of self-identical things would serve as the domain Weir wants if only it were an object. It, and all of the classes we need to do semantics, is characterizable as the extension of a formula with one free variable.

We can, Weir's view nearly goes, therefore take the formulas in one free variable to be the objects we need. That is, of course, obviously false: the formula 'x=x' is just a string of three symbols, not a domain at all. However, the string of symbols '[x:x=x]' looks a lot better. If we can give that string the semantics of a denoting term, then, what it denotes presumably will be what we're looking for.

That is done in two stages: first, a set-theoretic semantics to show that what is being done is coherent, then, since on the set-theoretic semantics the domain is a set, hence not absolutely everything, we show how to give the semantics of the theory within the theory itself.

Since we want a theory not of things like '[x:x=x],' but of their denotations, we give the kinds of things such symbols denote a name, "properties," and we seek to identify them among the domain that is to serve as absolutely everything that we already have. They shouldn't be sets: their internal structure as sets won't reflect their nature as "properties." We therefore take them to be urelements. There will be a predicate that picks out the properties. So, what properties will properties have?

There is a new relation %$\varepsilon$% "falling under" that every object may or may not bear to every "property."

There are some basic properties. I don't think he ever gives any examples, so here are a couple: There is the "property" urelement (distinct from the predicate U (is an urelement). The characteristic property of urelement is %\[\forall x(x\varepsilon \text{urelement}\leftrightarrow Ux)\]% There is the property (set) membership. Its characteristic property is %\[\forall xy(\langle x,y\rangle \varepsilon \text{membership}\leftrightarrow x\in y)\]%

He gives the semantics of properties in the "obvious" way. That seems to specify the semantics of %$[x:\phi ]$%. We also get from that two principles that will be his proof-theoretic rules: From %$a\varepsilon [x:\phi ]$%, infer %$\phi a$%. From %$\phi a$%, infer %$a\varepsilon [x:\phi ]$%. I was at first misled into thinking that the reason he gives rules instead of the corresponding biconditional was just that he wanted a natural deduction system. In fact, however, the biconditionals are not true in his system.

Everything looks hunky dory, but we've just axiomatized "na\"{\i}ve "property" theory." The paradoxes all appear. He therefore only assumes the semantics just given for %$\phi$%s that do not include %$\varepsilon$% and closes in the Kripkean manner we discussed last class.

-- ShaughanLavine - 24 Mar 2009