Tuesday, 30 July 2013

Formal epistemology summer school / conference in Bristol

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/

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 mathematics invented by philosophers, in the period roughly 1879-1922:
1. The theory of relations.
2. The theory of quantification.
3. The analysis of what a variable is.
4. Truth tables/compositionality.
5. The formulation of formation and inference rules.
6. The recognition of the intimate relation of $A$ and "$A$ is true".
7. Higher-order logic.
8. The theory of types.
9. The theory of identity.
10. The concept of an abstraction principle.
11. The definition of cardinality.
12. The definition of ancestral (transitive closure).
13. The derivation of Peano's axioms from an abstraction principle (Frege's Theorem)
14. The recognition of some need for levels/types/orders.
15. Russell's paradox.
(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.)

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 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:
"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: the Univalence 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.
(Hat-tip: Richard Zach!)

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 an informal argument whose purpose is to convince those who endeavor to follow it that a certain mathematical statement is true (and, ideally, to explain why it 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}$ ("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$"
$X \in Y$ for "$X$ is an element of $Y$"
$\mathsf{Class}(X)$ for "$X$ is a class"
We introduce explicit definitions:
$\mathsf{Memb}(X)$ is short for $\exists Y(X \in Y)$.
$\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)$.
In quantifiers, it's convenient to use somewhat type-theoretic looking abbreviations:
$X : \mathsf{Class}$ for $\mathsf{Class}(X)$.
$X : \mathsf{Memb}$ for $\mathsf{Memb}(X)$.
$X : \mathsf{Atom}$ for $\mathsf{Atom}(X)$.
For quantification over 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:
Axioms 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).$
These are impredicative class comprehension (restricted to 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 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 categorical formulations of set theory. These are sometimes also called "structural set theories". There are a number of these now, including:
Historically, Lawvere's $\mathsf{ETCS}$ appeared first, in
Lawvere, 1964: "An elementary theory of the category of sets", Proceedings of the National Academy of Sciences of the USA 52, 1506-1511.
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.,
ETCS at nLab.
Structural set theory at nLab.
SEAR at nLab.
Two summaries of the philosophical outlook are given in recentish blogposts:
Tom Leinster, "Rethinking Set Theory", n-Category Cafe (Dec 18, 2012; article here)
Mike Shulman, "From Set Theory to Type Theory", n-Category Cafe (Jan 7, 2013)
Both have very stimulating comments! Mike Shulman emphasizes the following difference:
... 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 not given to you as an element of $X$, then it isn’t an element of $X$, and no 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.
It 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 consider
  • 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.). 
Still, let's put that worry aside.

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}$
$v^{el}_i : v^{set}_j$
$v^{rel}_i : v^{set}_j \looparrowright v^{set}_k$
Nothing else is a term. (These are "type-declarations". Note that variables are not counted as terms.)

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:
$x = y$
$\varphi = \psi$
These are all the atomic formulas.

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,
set variables do not appear in any atomic formulas.
Rather, set variables appear only in complex 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.
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.
Nothing else 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$
$\phi \leftrightarrow \theta$ is short for $(\phi \to \theta) \wedge (\theta \to \phi)$
So, for example, we have:
$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)
$(\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)$
The second axiom, Axiom 1 (Relational comprehension) is an 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 an empty set.

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 a tabulating set
$C: \mathsf{Set}$
and projection functions
$p : C \looparrowright A$,
$q : C \looparrowright A$
such that
$(\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 :
$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: applicability. So, here is a revised list:
(Austerity) $F$ is conceptually austere.
(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.
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 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$.
The class of molecules in a sample of gas or fluid. 
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$.

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:
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), is a set. Furthermore, extensionally inequivalent representations exist. E.g., there are two distinct sets $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 are arbitrary choices. It doesn't in fact ever matter which "choice" we make, unless we ask a dumb question. 
(There is a technical reason for it not ever mattering: these reductions can be formulated as 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:
Extend set theory with abstraction principles for sui generis mathematical objects.
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.

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$.
(N-Abs) $|X| = |Y| \leftrightarrow X \sim Y$.
(E-Abs) $Equiv_{\phi} \to ([x]_{\phi} = [y]_{\phi} \leftrightarrow \phi(x,y))$.
where $\phi = \phi(x,y)$ is a formula with two free variables, and $Equiv_{\phi}$ says that $\phi$ expresses an equivalence relation.

  • (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).
Define $\mathsf{SGM}$ (for "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 a conservative extension of $\mathsf{MKA}$.
For 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.

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:
All sui generis abstracta are atoms.
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 the 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.


First, my favourite - the FBI's file on Carnap!
FBI Records (Rudolph Carnap)
Rudolph Carnap: Books 
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", Handbook of the History of Logic.)
In the occasional book,
Philosophy for Linguists: An Introduction 
Mindful Universe: Quantum Mechanics and the Participating Observer
In 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 Empiricist
Some blogs:
A Profile of Rudolph Carnap (3quarksdaily)
On Rudolph Carnap's The Logical Structure of the World (Partially Examined Life)
Online excerpts (this is very good, btw: Carnap on observables and Ramsey sentences):
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 "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, Introduction to Mathematical Logic, Chapter 4, "Axiomatic Set Theory".
except that (Impredicative) Class Comprehension is assumed as an 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$"
$X \in Y$ for "$X$ is an element of $Y$"
$Cl(X)$ for "$X$ is a class"
We introduce explicit definitions:
$Memb(X)$ is short for $\exists Y(X \in Y)$.
$Atom(X)$ is short for $\neg Cl(X) \wedge Memb(X)$.
Axioms 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).$
These are 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\}$
$\mathcal{A} \models \mathsf{ASC}$
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.
(Pair) If $x,y$ are members, then $\{x,y\}$ is a set.
And one can then continue to add one's favourite set existence axioms.

Sunday, 14 July 2013

Theorem 1

In the previous century, I wrote a paper
Ketland 1999: "Deflationism and Tarski's Paradise" (Mind). 
The main point of this paper was to argue that 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) in
Leitgeb 2007: "What Theories of Truth Should be Like (but Cannot be)" (Phil Compass: available here). 
These two conditions are incompatible, in some scenarios, because of Gödel's incompleteness theorems: hence, deflationary 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" (J. Phil, 1998),
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,
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 published
Halbach 1999, "Disquotationalism and Infinite Conjunctions" (Mind),
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 paper 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):
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 any distinct sentences $\phi, \theta$ in $L$,
$T \vdash\ulcorner \phi \urcorner \neq \ulcorner \theta \urcorner$.
Let $\Psi$ be a finite set 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$.
Proof: Let the assumptions be as stated, and let $\Psi = \{\psi_1, \dots, \psi_n\}$ be given. Define the following $L$-formula:
$\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)$
$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) \vdash
(\ulcorner \psi_i \urcorner = \ulcorner \psi_i \urcorner \wedge \psi_i)$
and so,
$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)$ 
$T \vdash \mathsf{True}^{\circ}(\ulcorner \psi_i \urcorner) \leftrightarrow \psi_i$ 

Here then is one modification of "Theorem 1" which is ok:
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 any distinct sentences $\phi, \theta$ in $L$,
$T \vdash \ulcorner \phi \urcorner \neq \ulcorner \theta \urcorner$.
Then $T \cup \Delta_{TB}$ conservatively extends $T$ (for $L$-sentences).
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$.

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$
$\mathsf{True}(\ulcorner \psi_n \urcorner) \leftrightarrow \psi_n$
(I.e., these are T-sentences occurring in the proof $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
$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.