Epistemic Utility Theory 2013, University of Bristol

Summer school: August 14-16, 2013

Conference: August 17-18, 2013

Speakers: Jim Joyce, Rachael Briggs, Kenny Easwaran, Jennifer Carr, Branden Fitelson, Katie Steele, Jason Konek, Ben Levinstein, Richard Pettigrew.

Graduate papers: Dmitri Gallow (Michigan) and Jeremy Lent (Michigan)

For details, please https://sites.google.com/site/bristolsummerschool/

## Tuesday, 30 July 2013

## Monday, 29 July 2013

### What Did the Philosophers Ever Do For Us?

About a year ago, I gave a list of achievements of analytic metaphysics.

A couple of friends said to me, "Look - that's not metaphysics! It's mathematics!". Ok. Fair enough - but then you can't have it both ways. Here we go with a list of the parts of modern

To be a bit more serious, maybe we should think of these as all

I neglected to mention The Romans.

A couple of friends said to me, "Look - that's not metaphysics! It's mathematics!". Ok. Fair enough - but then you can't have it both ways. Here we go with a list of the parts of modern

*mathematics*invented by*philosophers*, in the period roughly 1879-1922:1. The theory of(Admittedly, mostly logic and foundations, and mainly Frege and Russell. There's overlap, of course, with Dedekind, Cantor, Peano, Zermelo; and somewhat later, Hilbert, von Neumann and so on. I have also ignored the Poles. Not on purpose. Mainly because I know much less about Lesniewski's work.)relations.

2. The theory ofquantification.

3. The analysis of what avariableis.

4.Truth tables/compositionality.

5. The formulation offormationandinference rules.

6. The recognition of the intimate relation of $A$ and "$A$ is true".

7.Higher-order logic.

8. The theory oftypes.

9. The theory ofidentity.

10. The concept of anabstraction principle.

11. The definition ofcardinality.

12. The definition ofancestral(transitive closure).

13. The derivation of Peano's axioms from an abstraction principle (Frege's Theorem)

14. The recognition of some need forlevels/types/orders.

15.Russell's paradox.

To be a bit more serious, maybe we should think of these as all

*simultaneously*parts of mathematics, philosophy and logic.I neglected to mention The Romans.

## Sunday, 28 July 2013

### Uniqueness in Structural Set Theories, II

In set theory, using a 1-sorted first-order language $L$ with $=$ and $\in$, one defines a set to be

It is a simple result that Extensionality implies that there is a

From Cantor on, the usual assumption is that the

But in Structural Set Theories, like $\mathsf{ETCS}$ and $\mathsf{SEAR}$, one cannot prove uniqueness of mathematical objects, and, in particular, the uniqueness of the empty set. Instead, an empty set is defined as an

So---at least as I now understand it---in category theory, one can't prove, for objects $X,Y$ in a category $\mathcal{C}$, a uniqueness claim:

*empty*just if it has no elements. That is,$\mathsf{Empty}(x)$ for $\forall y(y \notin x)$The axiom $\mathsf{Ext}$ of

*Extensionality*states that sets with the same elements are*identical*:$\forall x \forall y(\forall z(z \in x \leftrightarrow z \in y) \to x = y)$(This axiom can be modified to allow urelemente/atoms, by restricting the quantifiers $\forall x, \forall y$, to classes/sets.)

It is a simple result that Extensionality implies that there is a

*unique*empty set:$\mathsf{Ext} \vdash \forall x \forall y((\mathsf{Empty}(x) \wedge \mathsf{Empty}(y)) \to x = y)$For assume $\mathsf{Ext}$ and let $\mathsf{Empty}(x)$ and $\mathsf{Empty}(y)$. Given any $z$, we have $z \notin x$ and $z \notin y$. So, $z \in x \leftrightarrow z \in y$. So, by $\mathsf{Ext}$, $x = y$.

From Cantor on, the usual assumption is that the

*concept*of set is inseparable from Extensionality.But in Structural Set Theories, like $\mathsf{ETCS}$ and $\mathsf{SEAR}$, one cannot prove uniqueness of mathematical objects, and, in particular, the uniqueness of the empty set. Instead, an empty set is defined as an

*initial object in a certain category*. (Lawvere (1964) gave the first categorical characterization of the set-theoretic universe.) And while one can prove that initial objects are (uniquely) isomorphic, one cannot prove that initial objects are*identical:*one cannot*express*that they are identical.So---at least as I now understand it---in category theory, one can't prove, for objects $X,Y$ in a category $\mathcal{C}$, a uniqueness claim:

$(\mathsf{Initial}_{\mathcal{C}}(X) \wedge \mathsf{Initial}_{\mathcal{C}}(Y)) \to X = Y$And this is merely because one can't

*express*identity of objects:$X = Y$.

*So*... as far as I understand the conceptual ideology/assumptions of Category Theory (which I'm not so sure I do understand),*there simply is no identity predicate for mathematical objects*. It was quite surprising to me when I realised this might be so.## Saturday, 27 July 2013

### "Structuralism, Invariance and Univalence" (Steve Awodey)

A link to a new paper by Steve Awodey (CMU and MCMP) on structuralism and univalence:

"(Hat-tip: Richard Zach!)Structuralism, Invariance and Univalence"

Recent advances in foundations of mathematics have led to some developments that are significant for the philosophy of mathematics, particularly structuralism. Specifically, the discovery of an interpretation of Martin-Löf’s constructive type theory into abstract homotopy theory suggests a new approach to the foundations of mathematics, with both intrinsic geometric content and a computational implementation. Leading homotopy theorist Vladimir Voevodsky has proposed an ambitious new program of foundations on this basis, including a new axiom with both geometric and logical significance: theUnivalence Axiom. It captures the familiar aspect of informal mathematical practice according to which one can identify isomorphic objects. While it is incompatible with conventional foundations, it is a powerful addition to the framework of homotopical type theory.

### Re-proving theorems, and the trouble with incorrect proofs of true statements

(Cross-posted at NewAPPS)

**“That's the problem with false proofs of true theorems: it's not easy to produce a counterexample.”**
This is a comment by Jeffrey Shallit in a post on a
purported proof of Fermat’s Last Theorem. (Incidentally, the author of the
purported proof comments here at M-Phi occasionally.) In all its apparent
simplicity, this remark raises a number of interesting philosophical questions. (Being the pedantic philosopher that I am, I'll change a bit the terminology and use the phrase 'incorrect proof' instead of 'false proof', which I take to be a category mistake.)

First of all, the remark refers to a pervasive but prima
facie slightly puzzling feature of mathematical practice: mathematicians often formulate
alternative proofs of theorems that have already been proved. This may appear
somewhat surprising on the assumption that mathematicians are (solely) in the
business of establishing (mathematical) truths; now, if a given truth, a
theorem, has already been established, what is the point of going down the same
road again? (Or more precisely, going to the same place by taking a different
road.) This of course shows that the assumption in question is false:
mathematicians are not only interested in

*theorems*, in fact they are mostly interested in*proofs*. (This is one of the points of Rav’s thought-provoking paper ‘Why do we prove theorems?’)
There are several reasons why mathematicians look for
new proofs of previously established theorems, and John Dawson Jr.’s excellent ‘Why do mathematicians re-prove theorems?’ discusses a number of these reasons. The
original proof may be seen as too convoluted or not sufficient explanatory –
ideally, a proof shows not only

*that*P is the case, but also*why*P is the case (more on this below). Alternatively, the proof may rely on notions and concepts alien to the formulation and understanding of the theorem itself, giving rise to concerns of purity. Indeed, recall that Colin McLarty motivates his search for a new proof of Fermat’s Last Theorem in these terms: “Fermat’s Last Theorem is just about numbers, so it seems like we ought to be able to prove it by just talking about numbers”. This is not the case of the currently available proof by Wiles, which relies on much heavier machinery.
From the point of view of the dialogical conception of
proofs that I’ve been developing, as involving a proponent who wants to establish the conclusion and an opponent who seeks to block the derivation of the conclusion (see here and here), an important reason to re-prove theorems would be
related to the

*persuasive**function*of proofs. Dawson does mention persuasion in his paper, but he does not adopt an explicit dialogical, multi-agent perspective:[W]e shall take a proof to be aninformalargument whose purpose is to convince those who endeavor to follow it that a certain mathematical statement is true (and, ideally, to explainwhyit is true). (p. 270)

(In my opinion, this is a fabulous definition of mathematical proofs, except for the fact that it is not explicitly multi-agent.) That is, a given proof, while correct, may still fail to be sufficiently convincing
in this sense. I am here reminded of Smale’s original proof of the possibility
of eversion of the sphere, which however did not exhibit the process through
which the eversion would take place. It was only when Morin built clay models
of the stages of the process that it became clear not only

*that*a sphere can be eversed, but also*how*it can be eversed. (In mathematics,*whys*often become*hows*, i.e. how to construct a given entity, how to realize a given process etc.) In fact, it is now known that there are different ways of eversing the sphere.
Still within the dialogical framework, another reason to
formulate alternative proofs of theorems are the different commitments and
tastes of various audiences. A mathematical proof is a

*discourse*, and even though there is an absolute sense in which a proof is or is not correct, different proofs will be more or less persuasive to different audiences. For example, this observation would explain the search for constructive as well as classical proofs of the same theorems, thus catering for different groups of potential addressees. More generally, different preferences in argumentative styles (not only in theoretical commitments as the ones separating classical and constructivist mathematicians) may also create the space for several proofs of the same theorems.
And here is a final, less ‘noble’ reason for re-proving
previously established theorems: such proofs are harder to refute. The mathematician’s preferred approach to refuting a proof is to provide a counterexample, i.e. a situation or construction
where the premises hold but the conclusion (the theorem) does not. Now, if
providing such a counterexample were the only move available to opponent to block the
inference of the conclusion by proponent (a thought that I confess to have
entertained for a while), then every proof of a true theorem would be a valid
proof, no matter how absurd and defective (such as the one motivating
Shallit’s comment above).

This is exactly why a proof cannot be a one-step
argument going directly from premises to conclusion (which is, in effect, a
necessarily truth-preserving move in the case of true theorems): a proof spells
out the intermediate steps, which must be individually perspicuous and
explanatory – and yes, also necessarily truth-preserving. So incorrect proofs
of true theorems require the additional work of delving into the details of the
proof in its different steps in order to reveal where the mistake(s) lie(s) –
more work, and often tedious work.

Nobody said it was easy being a mathematical opponent.

## Monday, 22 July 2013

### Slight Reformulation of ASC

This is a slightly different formulation of the theory of classes and atoms, $\mathsf{ASC}$ ("

The official language $L$ of $\mathsf{ASC}$ is a 1-sorted first-order language, with variables

As mentioned before, this "second-order" theory $\mathsf{ASC}$ of classes is very weak. It has 1-element models. More generally, the models are related to power-set Boolean algebras, analogous to how models for $\mathsf{MK}$ can be understood as $\mathcal{P}(V_{\alpha})$, with $\alpha$ inaccessible.

*atoms, sets and classes*") that I rather like, because of its generality (it permits urelemente/atoms and has impredicative comprehension) and its minimal restrictions. It is closely related to $\mathsf{MKA}$, Morse-Kelley class theory with atoms.The official language $L$ of $\mathsf{ASC}$ is a 1-sorted first-order language, with variables

$X,Y, Z, X_1, X_2, \dots$and three primitive predicates:

$X = Y$ for "$X$ is identical to $Y$"We introduce explicit definitions:

$X \in Y$ for "$X$ is an element of $Y$"

$\mathsf{Class}(X)$ for "$X$ is a class"

$\mathsf{Memb}(X)$ is short for $\exists Y(X \in Y)$.In quantifiers, it's convenient to use somewhat type-theoretic looking abbreviations:

$\mathsf{Set}(X)$ is short for $\mathsf{Class}(X) \wedge \mathsf{Memb}(X)$.

$\mathsf{Atom}(X)$ is short for $\neg \mathsf{Class}(X) \wedge \mathsf{Memb}(X)$.

$X \equiv Y$ is short for $\forall Z(Z \in X \leftrightarrow Z \in Y)$.

$X : \mathsf{Class}$ for $\mathsf{Class}(X)$.For quantification over

$X : \mathsf{Memb}$ for $\mathsf{Memb}(X)$.

$X : \mathsf{Atom}$ for $\mathsf{Atom}(X)$.

*members*, one may introduce a new variable sort $x,y,z, \dots$ as follows:$\forall x \phi(x)$ is short for $(\forall X : \mathsf{Memb}) \phi(X))$Then the axioms look a bit prettier:

These are impredicative class comprehension (restricted toAxioms of$\mathsf{ASC}$:

(COMP) $\hspace{10mm}$ $(\exists X: \mathsf{Class})\forall y(y \in X \leftrightarrow \phi(y)).$

(EXT) $\hspace{13mm}$ $(\forall X : \mathsf{Class})(\forall Y : \mathsf{Class})

(X \equiv Y \to X = Y).$

(ATOM) $\hspace{10mm}$ $(\forall X: \mathsf{Atom})\forall Y(Y \notin X).$

*members*), extensionality (restricted to*classes*) and an axiom saying that atoms are empty. One may write down*any*formula $\phi(y)$ for comprehension (with $X$ not free of course!). Consistency of comprehension (COMP) is ensured because the inner quantification only goes over*members*.As mentioned before, this "second-order" theory $\mathsf{ASC}$ of classes is very weak. It has 1-element models. More generally, the models are related to power-set Boolean algebras, analogous to how models for $\mathsf{MK}$ can be understood as $\mathcal{P}(V_{\alpha})$, with $\alpha$ inaccessible.

## Sunday, 21 July 2013

### Abstract Structure and Types

If $G = (V,E)$ is a graph, with vertex set $V$ and edge relation $E$, the suggestion is that its

In particular, we obtain the

For a mathematical object $\mathcal{A}$ (such as a group, a field, a topological space, a manifold, etc., understood as a model), the diagram formula---or, more exactly, the propositional function $\hat{\Phi}_{\mathcal{A}}$ expressed by the diagram formula---encodes

Returning to the diagram formula, $\Phi_{G}(X_0, X_1)$, a special role is played by the variable $X_0$ which "picks out" the domain. Its role is more or less the same as that played by the variable $A$ in "type declarations" such as

*abstract structure*is the the*propositional function*expressed by its*diagram formula*$\Phi_G(X_0,X_1)$. For example, consider the two vertex directed graph:$G = (\{0,1\}, \{(0,1)\})$.Then, the abstract structure of $G$ is the propositional function $\hat{\Phi}_G$ expressed by the formula $\Phi_G(X_0,X_1)$:

$\exists v_0 \exists v_1 (X_0(v_0) \wedge X_0(v_1) \wedge \neg X_1(v_0,v_0) \wedge X_1(v_0,v_1)$ $ \wedge \neg X_1(v_1,v_0) \wedge \neg X_1(v_1,v_1) \wedge \forall z(X_0(z) \to (z = v_0 \vee z = v_1)))$The categoricity of the diagram formula $\Phi_{G}(X_0,X_1)$ ensures that it defines the isomorphism type of $G$. That is, for any graph $G^{\prime}$, we have:

$G^{\prime} \models \Phi_{G}(X_0,X_1)$ iff $G \cong G^{\prime}$.For example:

$G^{\prime} = (\{3,4\}, \{(3,4)\})$.This is isomorphic to $G$. That is,

$G \cong G^{\prime}$.So, $G^{\prime} \models \Phi_{G}(X_0,X_1)$.

In particular, we obtain the

*same*propositional function in both cases:$\hat{\Phi}_{G} = \hat{\Phi}_{G^{\prime}}$So, $G$ and $G^{\prime}$ have

*identical*abstract structure.For a mathematical object $\mathcal{A}$ (such as a group, a field, a topological space, a manifold, etc., understood as a model), the diagram formula---or, more exactly, the propositional function $\hat{\Phi}_{\mathcal{A}}$ expressed by the diagram formula---encodes

*all the structural information*concerning $\mathcal{A}$.Returning to the diagram formula, $\Phi_{G}(X_0, X_1)$, a special role is played by the variable $X_0$ which "picks out" the domain. Its role is more or less the same as that played by the variable $A$ in "type declarations" such as

$a : A$in structural set theory and type theories. We could rewrite the diagram formula more type-theoretically like this:

$(\exists v_0: X_0)(\exists v_1: X_0)(\forall z: X_0) (\neg X_1(v_0,v_0) \wedge X_1(v_0,v_1)$ $ \wedge \neg X_1(v_1,v_0) \wedge \neg X_1(v_1,v_1) \wedge (z = v_0 \vee z = v_1))$For this analysis, however, the type involved is always a type of

*set*: i.e., the carrier set of the mathematical model.## Saturday, 20 July 2013

### Uniqueness in Structural Set Theories

Over the last couple of years, I've occasionally tried to have a go at understanding certain

To some extent, the emergence of such "structural set theories" responds to the challenge, by some mathematicians who have expressed their preference for the ordinary (Cantorian) concept of a set as a "definite collection of things", to give a fully axiomatic presentation of structural set theory.

Here I try and focus on the theory $\mathsf{SEAR}$ ("sets, elements and relations") which I find a bit easier to understand, as the algebra only takes off slowly ... I only give the basic syntax (at least as I understand it: I may be reading it wrongly), and

What is interesting is the topic of

I take the alphabet $\Sigma$ of $L_{\mathsf{SEAR}}$ to be:

For each $i, j,k \in \omega$, the following expressions are terms:

For any element variables $x,y$, relation variables $\varphi, \psi$, the following are atomic formulas:

It is worth highlighting that equations with $=$ flanked by set variables, i.e., of the form

Then we define the formulas by the usual inductive clauses:

The first three axioms of $\mathsf{SEAR}$ are:

The third axiom, Axiom 2, asserts, in intuitive set-theoretic lingo, that given a relation

This theorem asserts the existence of

By Axiom 0, we have $A: \mathsf{Set}$ and $\exists x : A$ with $x = x$.

By Axiom 1, we may assert the existence and uniqueness of the relation

This proof establishes the existence and uniqueness of an empty relation

However, it does not establish the

I'm somewhat bothered by this. I could simply be misunderstanding something quite simple. But if not, then it seems that this kind of non-uniqueness would occur quite generally. The underlying reason for it, I think, is this. As I understand the syntax, it is stipulated from the outset that one cannot

What's unclear to me then, at bottom, is whether forbidding formulas of the form $A = B$ is

[UPDATE (21 July 2013): I have made a couple of notational revisions.]

*categorical formulations*of set theory. These are sometimes also called "structural set theories". There are a number of these now, including:- $\mathsf{ETCS}$: "elementary theory of the category of sets" (long version) (Lawvere 2005)
- $\mathsf{SEAR}$: "sets, elements and relations" (nLab)

Lawvere, 1964: "An elementary theory of the category of sets",A number of variants have since been given; and there are a number of very interesting recent formulations, given by category theorists Todd Trimble, Tom Leinster, Toby Bartels and Mike Shulman. These have been described at the category-theory wiki nLab: e.g.,Proceedings of the National Academy of Sciences of the USA52, 1506-1511.

ETCS at nLab.Two summaries of the philosophical outlook are given in recentish blogposts:

Structural set theory at nLab.

SEAR at nLab.

Tom Leinster, "Rethinking Set Theory", n-Category Cafe (Dec 18, 2012; article here)Both have very stimulating comments! Mike Shulman emphasizes the following difference:

Mike Shulman, "From Set Theory to Type Theory", n-Category Cafe (Jan 7, 2013)

... if $X$ is a structural-set, then there are some things which by their very nature are elements of $X$. (In $\mathsf{ETCS}$, those things are the functions with domain $1$ and codomain $X$.) If a thing is notIt seems to me, at first sight, that this will cause trouble with applied mathematics. For example, when we apply mathematics, in physics, chemistry, statistics and so on, one wants to considergiven to youas an element of $X$, then it isn’t an element of $X$, andno thing can be given to you as an element of more than one structural-set. The statement $A \in X$ is not something that you would ever think about proving about two pre-existing things $A$ and $X$, or assuming as a hypothesis except at the same time as you introduce $A$ as a new variable (as a way of saying “this is the sort of thing that $A$ is”). That is, to be maximally faithful to its usage in mathematics, $A \in X$ should not be considered as a proposition.

- classes of
*non-mathematical*things, - various
*quantity functions*(and indeed*physical fields*) from those things to various value ranges (e.g., $\mathbb{R}$ or some linear space, etc.).

To some extent, the emergence of such "structural set theories" responds to the challenge, by some mathematicians who have expressed their preference for the ordinary (Cantorian) concept of a set as a "definite collection of things", to give a fully axiomatic presentation of structural set theory.

Here I try and focus on the theory $\mathsf{SEAR}$ ("sets, elements and relations") which I find a bit easier to understand, as the algebra only takes off slowly ... I only give the basic syntax (at least as I understand it: I may be reading it wrongly), and

*three*of the axioms.What is interesting is the topic of

*uniqueness*.**1. Syntax of $L_{\mathsf{SEAR}}$**I take the alphabet $\Sigma$ of $L_{\mathsf{SEAR}}$ to be:

$\Sigma = \{\mathbf{Set}, =, :, \neg, \wedge, \vee, \bot, \exists, \forall , \looparrowright, (,) \} \cup \{v^{set}_i\}_{i \in \omega} \cup \{v^{rel}_i\}_{i \in \omega} \cup \{v^{el}_i\}_{i \in \omega}$Where it is implicitly assumed that all labelled syntactical thingies are

*distinct*. There are three things worth highlighting:(i) This language is 3-sorted (or there are 3 types, if you like). There are three disjoint sets (!!) $\{v^{set}_i\}$, $\{v^{rel}_i\}$, $\{v^{el}_i\}$ of variables, for "sets", "elements" and "relations". These will be relabelled, for ease of notation, in a moment.

(ii) There is a symbol, $:$, used for "type declaration". For example, given variables $x,A$, it gives a term $x : A$.

(iii) There is a symbol, $\looparrowright$, used for type declaration of relations: given $A,B, \varphi$, it gives a term $\varphi : A \looparrowright B$.

**Definition 1**(Terms of $L_{\mathsf{SEAR}}$)For each $i, j,k \in \omega$, the following expressions are terms:

$v^{set}_i : \mathsf{Set}$Nothing else is a term. (These are "type-declarations". Note that variables are not counted as terms.)

$v^{el}_i : v^{set}_j$

$v^{rel}_i : v^{set}_j \looparrowright v^{set}_k$

*Notation*: It is convenient to use the variables $x,y,z, \dots$ instead of $v^{el}_i$, in the obvious way. It is convenient to use the variables $A,B,C, \dots$ instead of $v^{set}_i$, in the obvious way. It is convenient to use the variables $\varphi, \psi, \dots$ instead of $v^{rel}_i$, in the obvious way.**Definition 2**(Atomic Formulas of $L_{\mathsf{SEAR}}$)For any element variables $x,y$, relation variables $\varphi, \psi$, the following are atomic formulas:

$\bot$These are all the atomic formulas.

$x = y$

$\varphi = \psi$

$\varphi(x,y)$

It is worth highlighting that equations with $=$ flanked by set variables, i.e., of the form

$A = B$,do

*not*count as atomic formulas. This is related to what is unclear about the uniqueness issue raised below. In fact, if I understand the syntax properly,Rather, set variables appear only in complexset variables do not appear in any atomic formulas.

*terms*: namely, either in the type-declaration$A : \mathsf{Set}$,or as domain and codomain within the type declaration

$\varphi : A \looparrowright B$of a relation.

**Definition 3**(Formulas of $L_{\mathsf{SEAR}}$)Then we define the formulas by the usual inductive clauses:

Each atomic formula is a formula.Nothing else is a formula.

If $\phi$ is a formula, then $\neg \phi$ is a formula.

If $\phi, \theta$ are formulas, then $\phi \vee \theta$ is a formula.

If $\phi, \theta$ are formulas, then $\phi \wedge \theta$ is a formula.

If $\phi$ is a formula and $t$ a term, then $(\forall t) \phi$ is a formula.

If $\phi$ is a formula and $t$ a term, then $(\exists t) \phi$ is a formula.

*Notation*: We don't fuss about brackets. We assume that the additional binary connectives $\to$ and $\leftrightarrow$ have been introduced by explicit definition in the usual way. That is:$\phi \to \theta$ is short for $\neg \phi \vee \theta$So, for example, we have:

$\phi \leftrightarrow \theta$ is short for $(\phi \to \theta) \wedge (\theta \to \phi)$

$A: \mathsf{Set}$ is a term.

$x : A$ is a term.

$\varphi: A \looparrowright B$ is a term.

$x = y$ is a formula.

$(\forall A : \mathsf{Set})(\exists \varphi: A \looparrowright A)(\forall x : A)(\forall y :A)(\varphi(x,y) \leftrightarrow x = y)$ is a formula.

**Definition 4**(*Function*) Suppose $\varphi : A \looparrowright B$ and, for all $x:A$, there is exactly one $y:B$ such that $\varphi(x,y)$. Then we say that $\varphi : A \looparrowright B$ is a function.*Notation*: It is convenient to introduce special variables, $p, q, \dots$ for functions. If$\varphi : A \looparrowright B$is a function, then we relabel as

$p : A \looparrowright B$instead, and the function notation

$p(x) = y$is short for $\varphi(x,y)$.

**2. Axioms of $\mathsf{SEAR}$**The first three axioms of $\mathsf{SEAR}$ are:

Axiom 0 (Non-Triviality).

$(\exists A: \mathsf{Set})(\exists x : A ) (x = x)$.

Axiom 1 (Relational Comprehension).

$(\forall A: \mathsf{Set})(\forall B: \mathsf{Set}) (\exists! \varphi : A \looparrowright B) (\forall x :A)(\forall y : B)(\varphi(x,y) \leftrightarrow P(x,y))$

Axiom 2 (Tabulations)The second axiom, Axiom 1 (Relational comprehension) is an

$(\forall A : \mathsf{Set})(\forall B: \mathsf{Set})(\forall \varphi : A \looparrowright B)(\exists C: \mathsf{Set})(\exists p : C \looparrowright A)(\exists q : C \looparrowright B)$

such that:

$(\forall x: A)(\forall y : B) (\varphi(x,y) \leftrightarrow (\exists r: C)(p(r) = x \wedge q(r) = y)$

$(\forall r:C)(\forall s:C) ((p(r) = p(s) \wedge q(r) = q(s)) \to r = s)$

*axiom scheme*. We may put for $P(x,y)$ any $L_{\mathsf{SEAR}}$-formula $\theta$ (so long as the relation variable $\varphi$ is not free in $\theta$).The third axiom, Axiom 2, asserts, in intuitive set-theoretic lingo, that given a relation

$R \subseteq A \times B$we have a

*set*$C : = \{(x,y) \in A \times B \mid Rxy\}$which is the set of "ordered pairs" in $R$. But the theory does not assume ordered pairs of elements as a primitive notion. So, to do this, Axiom 2 asserts the existence of a "tabulation"

$C, p, q$(of the appropriate types) where the functions $p : C \to A$ and $q : C \to B$ project, for any pair $(x,y) \in C$, the first and second components of the pair.

**3. Existence of Empty Set**

**Theorem 1**. $\mathsf{SEAR} \vdash (\exists C:\mathsf{Set})(\forall y:C)(y \neq y)$This theorem asserts the existence of

*empty set.*__an__**Proof**: Here is an informal proof based on the one at nLab (Theorem 1 too there).By Axiom 0, we have $A: \mathsf{Set}$ and $\exists x : A$ with $x = x$.

By Axiom 1, we may assert the existence and uniqueness of the relation

$\varphi : A \looparrowright A$such that

$\varphi(x,y) \leftrightarrow \bot$,for all $x, y : A$. Let us call this relation $\Phi$. So,

$(\forall x :A)(\forall y : A)(\Phi(x,y) \leftrightarrow \bot)$.By Axiom 2, we can assert the existence of

*tabulating set*__a__$C: \mathsf{Set}$and projection functions

$p : C \looparrowright A$,such that

$q : C \looparrowright A$

$(\forall x: A)(\forall y : A) (\Phi(x,y) \leftrightarrow (\exists r: C)(p(r) = x \wedge q(r) = y))$.And so, for all $x: A$, for all $y : A$,

$\bot \leftrightarrow (\exists r: C)(p(r) = x \wedge q(r) = y)$.Suppose, for a contradiction, we have $(\exists r: C)(r = r)$. So, let $p(r) = a$ and $q(r) = b$, with $a:A$ and $b:A$. Then

$(\exists r: C)(p(r) = a \wedge q(r) = b)$.And so, $\bot$. Therefore, $\neg (\exists r: C)(r = r)$. So, $C$ is empty. QED.

**4. Uniqueness**This proof establishes the existence and uniqueness of an empty relation

$\Phi : A \looparrowright A$.But note that this relation is sort of "attached" to $A$. It establishes the existence of

*an*empty set, namely $C : \mathsf{Set}$, which tabulates $\Phi$.However, it does not establish the

*uniqueness*of*the*empty set $\varnothing$.I'm somewhat bothered by this. I could simply be misunderstanding something quite simple. But if not, then it seems that this kind of non-uniqueness would occur quite generally. The underlying reason for it, I think, is this. As I understand the syntax, it is stipulated from the outset that one cannot

*express*"uniqueness" of a set $A$ satisfying some condition $P$ in this theory. To do this, we would need to write down:$P(A) \wedge P(B) \to A = B$But the required identity formula $A = B$, with set variables, is not syntactically allowed.

What's unclear to me then, at bottom, is whether forbidding formulas of the form $A = B$ is

*mandated*by the motivating philosophical/conceptual thought behind structural set theory, or whether it is largely a*matter of convenience*.[UPDATE (21 July 2013): I have made a couple of notational revisions.]

## Friday, 19 July 2013

### Average Height of a Beatle

Let :

Then define:

Let

$B := \{x \mid x$ is a Beatle $\}$and let:

$h_m(x) = r$stand for the quantity function which maps human beings to their heights in

*metres*.Then define:

$\overline{h}_B := \frac{1}{|B|} \sum_{x \in B} h_m(x)$This value is

*the average height of a Beatle*.Let

*C*be a class of human beings. Then:$\overline{h}_C := \frac{1}{|C|} \sum_{x \in C} h_m(x)$This value is

*the average height of an element of C*.### Applicability as an Adequacy Condition

This is a second post on the notion of a "foundation of mathematics". For example, Frege, Cantor, Russell and Zermelo gave foundations for parts of mathematics. I suggested five adequacy conditions for a claimed foundation $F$ for mathematics: (Austerity), (Non-Circularity), (Justification), (Interpretability Strength), (Structural Invariance).

That was a rough proposal. It occurs to me that I neglected an important condition:

In general, a theory of classes or sets is

That was a rough proposal. It occurs to me that I neglected an important condition:

*applicability*. So, here is a revised list:(Austerity) $F$ is conceptually austere.I've also reformulated the (Structural Invariance) condition. Beginning with $ZFC$, to discuss the natural numbers, one must definitionally extend in some way, defining "$x$ is a natural number". This can be done, but in many different ways, and the choice between these is

(Non-Circularity) $F$ is conceptually non-circular.

(Justification) $F$ has an intuitive epistemic justification.

(Applicability) $F$ should be applicable to non-mathematical subject matter.

(Interpretability Strength) $F$ has high interpretability strength.

(Structural Invariance) $F$ should not enforce arbitrary choices of reduction.

*arbitrary*. I believe that the*sui generis*approach sketched a while ago,*Sui Generis Mathematics*, provides the right way to resolve this problem.*Sui generis abstracta*(e.g., pairs, sequences, cardinals, equivalence types) are characterized by*abstraction principles*added to set theory as primitives.In general, a theory of classes or sets is

*applicable*because one can assert the existence of classes of*non-classes*(e.g., "set-theoretic atoms") and*non-mathematical entities*(e.g., spacetime points) using*comprehension*, as follows:$\exists X \forall x(x \in X \leftrightarrow \phi(x))$where $\phi(x)$ can be any predicate that applies to the non-classes, or to non-mathematical entities: e.g., lumps of material, regions of space, measuring rods, etc. So, one can talk about:

The class of spacetime points in the future light cone of some given event $e$.Without this, one cannot do physics. For example, one cannot do the kinetic theory of gases without assuming that one has a class $C$ of molecules in a certain spatial region $R$ (with volume $V$), with cardinality $N = |C|$, and some probability distribution of velocities over the molecules in $C$.

The class of molecules in a sample of gas or fluid.

## Wednesday, 17 July 2013

### New book series: PhD dissertations in logic

College Publications is now launching a new series
potentially of great interest to M-Phi’ers at large: Logic PhDs. The goal of
the series is to publish historically important doctoral theses as well as
remarkable recent ones, but for now the planned volumes are all historical
landmarks:

Christine Ladd-Franklin, 1882, The Johns Hopkins University

On the Algebra of Logic

PhD advisor: Charles Peirce

Volume prepared by Irving Anellis (Indiana University and
Peirce Edition Project, USA)

Haskell Curry, 1930, University of Göttingen

Grundlagen der kombinatorischen Logik (Foundations of
Combinatory logic)

PhD advisor: David Hilbert

Volume prepared by Jonathan Seldin (University of
Lethbridge, Canada)

Gerhard Gentzen, 1933, University of Göttingen

Untersuchungen über das logische Schließen (Researches on
Logical Deduction)

PhD advisor: Paul Bernays

Volume prepared by Jan von Plato (University of Helsinki,
Finland)

Saunders Mac Lane, 1934, University of Göttingen

Abgekürzte Beweise im Logikkalkul (Abbreviated Proofs in the
Logical Calculus)

PhD advisors: Hermann Weyl and Paul Bernays

Volume prepared by Peter Arndt (University of Regensburg,
Germany)

Jean Porte, 1965, University of Paris

Recherches sur la Théorie Générale des Systèmes Formels et
sur les Systèmes Connectifs

(Researches in the General Theory of Formal Systems and in
Connectives Systems)

PhD advisor: René de Possel

Volume prepared by Marcel Guillaume (University of
Clermont-Ferrand, France)

Hans Kamp, 1968, UCLA

Tense Logic and the Theory of Linear Order

PhD advisor: Richard Montague

Volume prepared by Alexander Rabinowitz, (Tel Aviv
University, Israel)

Krister Segerberg, 1971, Stanford University

An Essay in Classical Modal Logic

PhD advisor: Dana Scott

Volume prepared by Patrick Blackburn (University of
Roskilde, Denmark)

Jean-Yves Béziau, the series editor, informs me that volumes are already planned for the doctoral theses of Alfred
Tarski, Emil Post, Paul Bernays, John von Neumann, Jacques Herbrand, Kurt Gödel,
Stephen Kleene, Roland Fraïsse, Nuel Belnap, Jon Michael Dunn, Dov Gabbay,
Johan van Benthem.

This seems like a great
initiative, which will greatly facilitate the study of the history of logic.
Many important results were first proved in doctoral dissertations (Gentzen and
Gödel spring to mind, but there are many others), so it makes good sense to
make these texts more readily available (those not originally in English will be translated). Moreover, each volume will contain an
extensive presentation of the author and his/her work and the historical
context, as well as further developments inspired by the work in question. (And last but not least, College Publications is a non-profit publisher with the mission of publishing high-quality books at reasonable prices, including those in this series.)

The series is open to
further suggestions, so if readers have ideas of other doctoral dissertation
meriting to be included, please speak up in comments. (I am very glad to see Ladd-Franklin's dissertation as one of the volumes in preparation, but it would be great if the series could publish many more female authors as well.)

## Monday, 15 July 2013

### SGM: Sui Generis Mathematics

The Cantorian transfinite cumulative hierarchy $V$ of pure wellfounded sets has an amazing property:

One might object:

A much more serious objection (based on Benacerraf's famous 1965 article "What Numbers Could Not Be"):

These "arbitrary choices" are, I believe, rather like

How might one give a theory of these objects which did

I think the answer is this:

For the

Intuitively:

In more detail, $\mathsf{SGM}$ implies the existence of

Every mathematical object that anyone has ever thought of can be "represented/modelled" in $V$.That is: pairs, relations, functions, tuples, sequences, ordinals, cardinals, $\mathbb{N}$, $\mathbb{Z}$, $\mathbb{Q}$, $\mathbb{R}$, $\mathbb{C}$, infinitesimals, etc., S_n, graphs, groups, vector spaces, topological spaces, manifolds, fibre bundles, etc., etc., can all be represented in $V$. In fact, most of them live happily inside the rank $V_{\omega + n}$, with $n$ around $3$.

One might object:

Ah, but what about proper classes?Well, ok, these are structures that are just as large as $V$ itself.

A much more serious objection (based on Benacerraf's famous 1965 article "What Numbers Could Not Be"):

"Represented" yes, but that doesn't mean that, e.g., the real number $\pi$, or the group SU(3),(There is a technical reason for it not ever mattering: these reductions can be formulated asisa set. Furthermore,extensionally inequivalentrepresentations exist. E.g., there are twodistinctsets $X$ and $Y$ both of which can represent/model the natural numbers. And this phenomenon of non-uniqueness is pervasive. In a sense, there are lots and lots arearbitrary choices. It doesn't in fact ever matter which "choice" we make, unless we ask a dumb question.

*definitional extensions*of $ZFC$ and definitional extensions are conservative.)These "arbitrary choices" are, I believe, rather like

*gauge choices*. We can choose some set $X$ to represent $\mathbb{N}$, or $\mathbb{R}$, etc., and in many inequivalent ways. But perhaps we would like to have natural numbers and real numbers living in the mathematical universe quite*independently*of any reduction. They would be*sui generis*mathematical objects.*Sui generis*mathematical objects will always be representable in $V$. But they live*alongside*$V$, rather than*inside*$V$.How might one give a theory of these objects which did

*not*require some arbitrary choice for the reduction to sets? What would a "gauge-invariant" theory of*sui generis*mathematical objects---pairs, relations, functions, natural numbers, ordinals, etc.--- look like?I think the answer is this:

The kind of set/class theory one might start with is $\mathsf{ASC}$, "atoms, sets, and classes", as described in this M-Phi post, along with requisite set existence axioms. If one adds the usual set existence axioms, one gets a theory simlar to $\mathsf{MKA}$, Morse-Kelley set (class) theory with atoms.Extendset theory withabstraction principlesforsui generismathematical objects.

For the

*sui generis*entities, one can then consider quite a variety of abstraction principles for*sui generis*mathematical entities. Here are three:(T-Abs) $\sigma_n(x_1, \dots, x_n) = \sigma_n(y_1,\dots, y_n) \leftrightarrow x_1 = y_1 \& \dots \& x_n = y_n$.where $\phi = \phi(x,y)$ is a formula with two free variables, and $Equiv_{\phi}$ says that $\phi$ expresses an equivalence relation.

(N-Abs) $|X| = |Y| \leftrightarrow X \sim Y$.

(E-Abs) $Equiv_{\phi} \to ([x]_{\phi} = [y]_{\phi} \leftrightarrow \phi(x,y))$.

Intuitively:

- (T-Abs) is an abstraction principle yielding
*tuples*; - (N-Abs) is an abstraction principle yielding
*cardinal numbers*; - (E-Abs) is an abstraction principle yielding "
*equivalence types*" (e.g., isomorphism types).

*Sui Generis*Mathematics") to be the result of adding these abstraction principles to $\mathsf{MKA}$:$\mathsf{SGM} := \mathsf{MKA}$ + (T-Abs) + (N-Abs) + (E-Abs).Then I believe---but I'm also not entirely sure---that the following conjecture is correct:

$\mathsf{SGM}$ is aFor given a model for $\mathsf{MKA}$, then we can interpret each abstraction principle, in the fairly obvious way, to come out true. For the abstractions with tuples and equivalences, we know how to do this. For the abstraction given by (N-Abs), i.e., Hume's Principle, then the abstracta $|X|$ for set sized classes $X$ are interpreted as cardinals, in the usual way (i.e., initial ordinals). Any proper class sized $X$ has the same cardinality, $=|V|$: call this $\infty$. This can presumably be interpreted as some arbitrary object that is not an initial ordinal.conservative extensionof $\mathsf{MKA}$.

In more detail, $\mathsf{SGM}$ implies the existence of

*anti-zero*, $\infty$, i.e.,$\mathsf{SGM} \vdash \infty = |V|$Assuming there are atoms, then this unique very "large" entity could be interpreted as some atom. In fact, I am inclined to add as an axiom:

But this would then (in the intended model, as it were) force the collection $At$ of atoms to form a proper class sized collection. And theAll sui generis abstracta are atoms.

*cardinality*$|At|$ of the collection $At$ of atoms would be $\infty$, and also an element of the collection of atoms. I.e.,$\infty \in At$.But I think this is all ok.

### Rudolph

First, my favourite - the FBI's file on Carnap!

Er, in an essay on

FBI Records (Rudolph Carnap)Amazon?

Rudolph Carnap: BooksFacebook?

Rudolph Carnap(I know: that isn't Carnap.)

Er, in an essay on

*Carnap*and inductive logic (this one has*gotta*be a spellcheck typo ....)"Like his distinguished predecessors Bernoulli and Bayes, Rudolph Carnap continued to grapple with the elusive riddle of induction for the rest of his life." (in "Carnap and the Logic of Inductive Inference",In the occasional book,Handbook of the History of Logic.)

Philosophy for Linguists: An Introduction

Mindful Universe: Quantum Mechanics and the Participating ObserverIn an article,

".... but surely not in the case of Hilary Putnam or Rudolph Carnap" ("Modal Epistemology and the Rationalist Renaissance")In a 1978 book review in

*Mind*:Rudolph Carnap, Logical EmpiricistSome blogs:

A Profile of Rudolph Carnap (3quarksdaily)

On Rudolph Carnap'sOnline excerpts (this is very good, btw: Carnap on observables and Ramsey sentences):The Logical Structure of the World(Partially Examined Life)

Rudolph Carnap: Philosophical Foundations of Physics, Chapters 23-6

### ASC: Atoms, Sets and Classes.

The following "second-order" axiom system is one I've been thinking about for a couple of years. It is called $\mathsf{ASC}$, which stands for "

The formulation of $\mathsf{ASC}$ is modelled partly on Mendelson's formulation of $\mathsf{NBG}$ set theory in

To simplify notation, one may introduce a new variable sort $x,y,z, \dots$ as follows:

*atoms, sets and classes*". In a sense, it is the bottom level of Morse-Kelley class theory with atoms, $\mathsf{MKA}$. A set is defined to be a class which is a member of some class. Specific set existence axioms are then given in the usual second-order way.The formulation of $\mathsf{ASC}$ is modelled partly on Mendelson's formulation of $\mathsf{NBG}$ set theory in

Mendelson,except that (Impredicative) Class Comprehension is assumed as anIntroduction to Mathematical Logic, Chapter 4, "Axiomatic Set Theory".

*axiom*(scheme). The official language $L$ of $\mathsf{ASC}$ is a 1-sorted first-order language, with variables $X,Y, Z, X_1, X_2, \dots$ and three primitive predicates:$X = Y$ for "$X$ is identical to $Y$"We introduce explicit definitions:

$X \in Y$ for "$X$ is an element of $Y$"

$Cl(X)$ for "$X$ is a class"

$Memb(X)$ is short for $\exists Y(X \in Y)$.Then:

$Atom(X)$ is short for $\neg Cl(X) \wedge Memb(X)$.

These areAxioms of$\mathsf{ASC}$:

(COMP) $\exists X[Cl(X) \wedge \forall Y(Y \in X \leftrightarrow (Memb(Y) \wedge \phi(Y))].$

(EXT) $Cl(X) \wedge Cl(Y) \to (\forall Z(Z \in X \leftrightarrow Z \in Y) \to X = Y).$

(ATOM) $Atom(X) \to \forall Y(Y \notin X).$

*restricted*class comprehension, extensionality and an axiom saying that atoms are empty:To simplify notation, one may introduce a new variable sort $x,y,z, \dots$ as follows:

$\forall x \phi(x)$ is short for $\forall X(Memb(X) \to \phi(X))$So, that comprehension can be re-expressed in the more familiar "second-order" way:

(COMP) $\exists X(Cl(X) \wedge \forall y(y \in X \leftrightarrow \phi(y)))$.

Extensionality allows us to prove the uniqueness of any such class; and so we can form class abstracts:

$\{x \mid \phi(x)\}$

with the usual meaning (i.e., the class of all members $x$ such that $\phi(x)$), whose existence is guaranteed by (COMP).

This "second-order" theory $\mathsf{ASC}$ is very safe: it has 1-element models! For example, let the $L$-interpretation $\mathcal{A}$ be defined by:

$A = \{0\}$

$\in^{\mathcal{A}} = \varnothing$

$Cl^{\mathcal{A}} = \{0\}$

Then:

$\mathcal{A} \models \mathsf{ASC}$A

*set*is defined to be a*class*which is a*member*. That is,$Set(X)$ is short for $Cl(X) \wedge Memb(X)$The theory $\mathsf{ASC}$ proves the existence of the

*class*$\varnothing$, but does not prove that $\varnothing$ is a*set*. Similarly, given $X,Y$, $\mathsf{ASC}$ proves the existence of the*class*$\{X,Y\}$, but does not prove that $\{X,Y\}$ is a set. One can remedy this with specific set-existence existence axioms, such as:(Empty) $\varnothing$ is a set.And one can then continue to add one's favourite set existence axioms.

(Pair) If $x,y$ are members, then $\{x,y\}$ is a set.

## Sunday, 14 July 2013

### Theorem 1

In the previous century, I wrote a paper

Just before that, but unbeknownst to either of us, Stewart Shapiro published a paper,

Still, the wrong "theorem" itself comes from a theorem which is

I noticed the theorem was wrong, when the article appeared in January 1999. For in the same issue of

To give a corrected version, first here's a lemma---one that is useful in thinking about truth predicates (it shows that given a

Here then is one modification of "Theorem 1" which is ok:

So, suppose that

So suppose that the following are axioms of $\Delta_{TB}$ occurring in $P$

Next let $\Psi = \{\psi_1, \dots, \psi_n\}$. By the above Lemma, we may define $\mathsf{True}^{\circ}(x)$, and then we have, by the Lemma above, that

Next, given any $\theta_i$ in the proof $P$, we define $(\theta_i)^{\circ}$ to be the result of replacing each occurrence of a subformula $\mathsf{True}(t)$ in $\theta_i$ by $\mathsf{True}^{\circ}(t)$. We obtain the sequence:

Ketland 1999: "Deflationism and Tarski's Paradise" (The main point of this paper was to argue thatMind).

*deflationary*truth theories should (and indeed do, usually) satisfy a conservation condition, but*adequate*theories should satisfy a reflection condition. This reflection condition is Leitgeb's adequacy condition (b) inLeitgeb 2007: "What Theories of Truth Should be Like (but Cannot be)" (These two conditions arePhil Compass: available here).

*incompatible*, in some scenarios, because of Gödel's incompleteness theorems: hence, d*eflationary truth theories are inadequate*.Just before that, but unbeknownst to either of us, Stewart Shapiro published a paper,

Shapiro 1998, "Proof and Truth - Through Thick and Thin" (giving a similar argument against deflationism, based on conservation and reflection. And a few years before that (the similarities were unbeknownst to any of the three of us), Leon Horsten had given some similar arguments in a 1995 article,J. Phil, 1998),

Horsten 1995, "The Semantic Paradoxes, The Neutrality of Truth and the Neutrality of the Minimalist Theory of Truth".But in the 1999 paper, I'd given a "theorem", labelled "Theorem 1". This "theorem" is wrong. Somewhat fortunately, this theorem can be "fixed" by adding certain side conditions (see below). But, as stated, it's wrong. How I ended up with a wrong theorem is moderately interesting.

Still, the wrong "theorem" itself comes from a theorem which is

*not wrong*, which is what I'd started with (I vividly remember guessing it and working out the proof), and which is important in the sense that it's connected to the ensuing debate about the conservativeness/non-conservativeness of truth theories. That theorem is:$PA$ + the Tarski biconditionals for $L$-sentences is a conservative extension of $PA$.This can be established in a number of ways: e.g., model-theoretically and proof-theoretically. It's clear that the theorem should generalize, because very little of the apparatus of $PA$ is needed for this to hold. In fact, it is sufficient that the base theory $T$ prove the distinctness of distinct expressions. That is,

if $\epsilon_1 \neq \epsilon_2$, then $T \vdash \ulcorner \epsilon_1 \urcorner \neq \ulcorner \epsilon_2 \urcorner$.Unfortunately, I generalized too much! In my 1999 paper, I say that the set of Tarski-biconditionals

$\Delta_{TB} := \{\mathbf{True}(\ulcorner \phi \urcorner) \leftrightarrow \phi \mid \phi \in Sent(L)\}$conservatively extends

*any*theory $T$, and this isn't so. $T$ must satisfy certain conditions. And the proof I give, by model expansion, is somewhat muddled, as it assumes that one can extend the*domain*of the starting model $\mathcal{M}$ by adding infinitely many (codes of) sentences, and this is not correct.I noticed the theorem was wrong, when the article appeared in January 1999. For in the same issue of

*Mind*, Volker Halbach publishedHalbach 1999, "Disquotationalism and Infinite Conjunctions" (and reading his paper carefully made me notice that my result needed side conditions. Halbach's paper included reference to a wealth of other recent work on axiomatic truth theories of which I'd been completely unaware when I wrote my paper. (I knew only Tarski's original 1936 paperMind),

*Der Wahrheitsbegriff*and worked from there. I didn't know the subsequent work by, e.g., Wang, Mostowksi, Feferman, Friedman & Sheard, Cantini, Halbach*et al*.)To give a corrected version, first here's a lemma---one that is useful in thinking about truth predicates (it shows that given a

*finite*set of sentences, then defining truth for these is not difficult, given just a bit of syntax):Proof: Let the assumptions be as stated, and let $\Psi = \{\psi_1, \dots, \psi_n\}$ be given. Define the following $L$-formula:Lemma: Let $L$ be the usual language of arithmetic and let $L^+$ be the result of adding a new unary predicate symbol $\mathsf{True}$. Let $T$ in $L$ be a theory such that, for anydistinctsentences $\phi, \theta$ in $L$,

$T \vdash\ulcorner \phi \urcorner \neq \ulcorner \theta \urcorner$.Let $\Psi$ be afiniteset of $L$-sentences. Then there is an $L$-formula $\mathsf{True}^{\circ}(x)$ such that,

$T \vdash \mathsf{True}^{\circ}(\ulcorner \psi \urcorner) \leftrightarrow \psi$,for each $\psi \in \Psi$.

$\mathsf{True}^{\circ}(x) := \bigvee \{x = \ulcorner \psi \urcorner \wedge \psi \mid \psi \in \Psi\}$Let $\psi_i \in \Psi$ and consider $\mathsf{True}^{\circ}(\ulcorner \psi_i \urcorner)$. That is,

$(\ulcorner \psi_i \urcorner = \ulcorner \psi_1 \urcorner \wedge \psi_1) \vee \dots \vee (\ulcorner \psi_i \urcorner = \ulcorner \psi_n \urcorner \wedge \psi_n)$Note that, if $i \neq j$, then

$T \vdash \ulcorner \psi_i \urcorner \neq \ulcorner \psi_j \urcorner$So, if $i \neq j$,

$T \vdash \neg(\ulcorner \psi_i \urcorner = \ulcorner \psi_j \urcorner \wedge \psi_j)$So,

$T \vdash \bigwedge \{\neg(\ulcorner \psi_i \urcorner = \ulcorner \psi_j \urcorner \wedge \psi_j) \mid j \neq i\}$But, by the definition of $\mathsf{True}^{\circ}(\ulcorner \psi_i \urcorner)$, we have:

$T, \mathsf{True}^{\circ}(\ulcorner \psi_i \urcorner) \vdash (\ulcorner \psi_i \urcorner = \ulcorner \psi_1 \urcorner \wedge \psi_1) \vee \dots \vee (\ulcorner \psi_i \urcorner = \ulcorner \psi_n \urcorner \wedge \psi_n)$So, then

$T, \mathsf{True}^{\circ}(\ulcorner \psi_i \urcorner) \vdashand so,

(\ulcorner \psi_i \urcorner = \ulcorner \psi_i \urcorner \wedge \psi_i)$

$T, \mathsf{True}^{\circ}(\ulcorner \psi_i \urcorner) \vdash \psi_i$By similar reasoning,

$T, \psi_i \vdash \mathsf{True}^{\circ}(\ulcorner \psi_i \urcorner)$So,

$T \vdash \mathsf{True}^{\circ}(\ulcorner \psi_i \urcorner) \leftrightarrow \psi_i$QED.

Here then is one modification of "Theorem 1" which is ok:

Proof. We will suppose that $T \cup \Delta_{TB}$ proves some $L$-sentence $\phi$, and then "convert" the proof into a proof in $T$ of $\phi$.Theorem: Let $L$ be the usual language of arithmetic and let $L^+$ be the result of adding a new unary predicate symbol $\mathsf{True}$. Let $T$ in $L$ be a theory such that, for anydistinctsentences $\phi, \theta$ in $L$,

$T \vdash \ulcorner \phi \urcorner \neq \ulcorner \theta \urcorner$.Then $T \cup \Delta_{TB}$ conservatively extends $T$ (for $L$-sentences).

So, suppose that

$T \cup \Delta_{TB} \vdash \phi$,with $\phi \in Sent(L)$. Let

$P = (\theta_0, \dots, \theta_k)$be such a proof. If no axioms from $ \Delta_{TB}$ occur in $P$, then $P$ is a proof in $T$ of $\phi$ and we are done.

So suppose that the following are axioms of $\Delta_{TB}$ occurring in $P$

$\mathsf{True}(\ulcorner \psi_1 \urcorner) \leftrightarrow \psi_1$(I.e., these are T-sentences occurring in the proof $P$.)

$\dots$

$\mathsf{True}(\ulcorner \psi_n \urcorner) \leftrightarrow \psi_n$

Next let $\Psi = \{\psi_1, \dots, \psi_n\}$. By the above Lemma, we may define $\mathsf{True}^{\circ}(x)$, and then we have, by the Lemma above, that

$T \vdash \mathsf{True}^{\circ}(\ulcorner \psi_i \urcorner) \leftrightarrow \psi_i$for each $\psi_i \in \Psi$.

Next, given any $\theta_i$ in the proof $P$, we define $(\theta_i)^{\circ}$ to be the result of replacing each occurrence of a subformula $\mathsf{True}(t)$ in $\theta_i$ by $\mathsf{True}^{\circ}(t)$. We obtain the sequence:

$P^{\circ} = ((\theta_0)^{\circ}, \dots, (\theta_k)^{\circ})$Substitution preserves deducibility, and so this sequence is a

*proof**using the translations of*$T$-*sentences as axioms*. However, each $T$-sentence$\mathsf{True}(\ulcorner \psi_i \urcorner) \leftrightarrow \psi_i$occurring in the proof $P$ is translated to a

*theorem*of $T$, namely,$\mathsf{True}^{\circ}(\ulcorner \psi_i \urcorner) \leftrightarrow \psi_i$So, if we extend $P^{\circ}$ by inserting the missing subproofs (in $T$) of these theorems, we obtain then a new sequence $P^{\ast}$. This is then a proof of $\phi$ in $T$, as required. QED.

Subscribe to:
Posts (Atom)