Skip to the Main Content

Note:These pages make extensive use of the latest XHTML and CSS Standards. They ought to look great in any standards-compliant modern browser. Unfortunately, they will probably look horrible in older browsers, like Netscape 4.x and IE 4.x. Moreover, many posts use MathML, which is, currently only supported in Mozilla. My best suggestion (and you will thank me when surfing an ever-increasing number of sites on the web which have been crafted to use the new standards) is to upgrade to the latest version of your browser. If that's not possible, consider moving to the Standards-compliant and open-source Mozilla browser.

February 26, 2020

Type Theory and Propositions

Posted by David Corfield

One of the things that philosophers will take a lot of getting used to, if HoTT is to be taken up as a new logic for philosophy, is the idea of propositions as a kind of types. We are very used to treating propositions with propositional logic, and then sets very differently, with first-order logic and some set axioms. This results in different issues arising for the latter, as when a philosopher worries about the ontological commitments of a simple piece of applied set theory or even applied arithmetic. It appears that speaking of two apples on my desk, I’m referring to some abstract entity 22. Then I’m to worry what kind of entity this number is, and how I can know about it. Applying logic by itself to the world is generally taken not to incur any such ontological debt.

Now, we are beginning to hear in analytic philosophy the idea that propositions are types, for instance, in the work of Hanks and Soames that propositions are types of predicative acts, as when we predicate wisdom of Socrates in ‘Socrates is wise’.

From the HoTT perspective, we will often have

x:AB(x):Prop, x: A \vdash B(x): Prop,

where from a:Aa: A we can then form B(a):PropB(a): Prop. And we can think of this type as predicating BB of aa. But propositions may arise by other routes, such as Id A(a,b)Id_A(a, b) for a set AA and two of its elements, e.g., is it the case that the tallest person in the room and the youngest person in the room coincide. Another form of proposition is generated as A\|A\| for a type AA. The latter is known as the bracket type where any elements of AA are identified. The proposition A\|A\| will be true when AA is inhabited. So if, say, AA is the type of occurrences of Kim drinking coffee yesterday, A\|A\| corresponds to the proposition whether Kim drank coffee yesterday.

Judging a proposition to be true is to judge the type to be inhabited. Propositions are just those kind of types which are subsingletons, or subterminal objects. Establishing that Kim drank coffee yesterday it doesn’t matter if you tell me about her morning espresso or her afternoon latte, they correspond to necessarily equal elements, |espresso||espresso| and |latte||latte|, in the mere proposition. We might be interested in the mere proposition rather than the set when all we care about is whether she drank any coffee that day (maybe it’s going to react with some medication) rather than a list of occurrences.

Taking propositions as subterminal objects makes sense of another conception of propositions that one encounters in the philosophical literature, namely, as the set of possible worlds (para. 6) in which they hold. This derives from a tradition which has looked to understand modal logic in terms of possible worlds. We can understand this viewpoint as concerning operations in a category varying over an object of worlds WW, what we call the slice category or over category. Then a subterminal object here corresponds to a monomorphism into WW, or in other words a subset of worlds for a set WW.

Something to be gained by HoTT is uniform type formation, so that, e.g., A×BA \times B is set product for sets and conjunction for propositions, while [A,B][A, B] is the set of functions B AB^A for sets and is implication, ABA \to B, for propositions. This explains all those analogies between logic and arithmetic, which otherwise seem to be mere coincidences, such as

  • (A&B)C(A \& B) \to C is True if and only if A(BC)A \to (B \to C) is True,

  • c (a×b)=(c b) a,c^{(a \times b)} = (c^b)^a,

These are each generated by a single adjunction.

[I’ll leave as an exercise how to understand c ib i= ic b ic^{\sum_i b_i} = \prod_i c^{b_i} and ( ib i) c= i(b i c)(\prod_i b_i)^c = \prod_i ({b_i}^c) as resulting from counting sets occurring in two adjunctions, and what the logical analogues amount to.]

But what about the philosophers’ disanalogy in ontological commitment between logic and arithmetic?

When we say of a proposition PP that it is true, we’re saying that the type PP is equivalent to the type 1\mathbf{1}. When we say ‘PP is false’, we’re saying that the type PP is equivalent to the type 0\mathbf{0}. 0\mathbf{0}, the empty type, is defined in HoTT inductively as the type with no constructors. The unit type, 1\mathbf{1}, is the type with a unique term, or the product type with no factors. We can also produce 1\mathbf{1} as [0,0][\mathbf{0}, \mathbf{0}], with its sole element, id 0id_{\mathbf{0}}. These are both propositions.

HoTT allows us to form the type of natural numbers inductively, and then also inductively Fin(n)Fin(n), a set with nn elements. Fin(0)Fin(0) is equivalent to 0\mathbf{0}, and Fin(1)Fin(1) is equivalent to 1\mathbf{1}. When we say there are two apples on the table, we are saying that there is an equivalence between the type of apples on the table and Fin(2)Fin(2).

We may take 1\mathbf{1} and Fin(2)Fin(2) to be part of the syntax, no more ontologically committing than is ×\times as product or conjunction. Or perhaps it might be argued that reference is being made to some ‘pure types’. Either way, there should be parity of treatment between applying logic and applying arithmetic/set theory if you adopt HoTT.

Posted at February 26, 2020 2:30 PM UTC

TrackBack URL for this Entry:   https://golem.ph.utexas.edu/cgi-bin/MT-3.0/dxy-tb.fcgi/3199

124 Comments & 0 Trackbacks

Re: Type Theory and Propositions

I am a little confused. Lets say I can form the type (apples on the table) : Type. Then to say that there are two apples on the table is to give a term

(there are two apples on the table) : ||(apples on the table) = Fin(2)||

It seems I have two types on hand – (apples on the table) and a type Fin(2) inductively defined to have exactly two instances – and I am relating these two types (via the relation of mere equivalence). How do I pass from this to any sort of ontological commitment. When is a type said to be a type of real existing entities, so that one may say that I am committing to the apples but not the abstract inductive type. Or am I to commit to both or neither?

I’m not sure what having an ontological commitment is supposed to mean: perhaps I have a model (reality) of reality and a fixed relationship between (apples on the table) and (reality) but not a fixed relationship between Fin(2) and (reality). I commit to those things that have a relationship with reality. But knowing that (there are two apples on the table) only merely gives me a relationship between Fin(2) and (reality), so I should only merely make such a commitment – in other words, I have made some commitment but not a particular commitment.

Posted by: David Jaz Myers on February 26, 2020 8:57 PM | Permalink | Reply to this

Re: Type Theory and Propositions

Thanks for the question. I should probably have given more of the philosophical context of this idea of ontological commitment. It’s not something that ever interested me in the past, but I raise it here since it shows up a clear difference in the attitude of analytic philosophers towards logic and mathematics.

The issue of ontological commitment drives a good part of analytic philosophy’s engagement with mathematics:

Quine (1976; 1980a; 1980b; 1981a; 1981c) and Putnam (1979a; 1979b) have argued that the indispensability of mathematics to empirical science gives us good reason to believe in the existence of mathematical entities. According to this line of argument, reference to (or quantification over) mathematical entities such as sets, numbers, functions and such is indispensable to our best scientific theories, and so we ought to be committed to the existence of these mathematical entities. To do otherwise is to be guilty of what Putnam has called “intellectual dishonesty” (SEP)

See how logic is used as a general tool to demonstrate one’s commitments, while the mathematical entities (numbers, sets) form the subject matter (what one is committed to).

One might accept the Quine-Putnam argument but still resist the conclusion by reformulating any expressions that mention mathematical entities to do without them. Hartry Field looks to do this is ‘Science without numbers’.

Field was very popular when I first started studying philosophy of mathematics, and I took this to be an indication of the degenerate nature of the discipline (hence the pointed title of my book – Towards a philosophy of real mathematics).

Now we find HoTT muddying the boundary between maths and logic, this might provide food for thought for the descendants of Putnam and Quine.

But there’s another line of thought that I think worth pursuing. The type formation - term introduction/elimination account of type theory has inspired the philosopher Robert Brandom to develop an ‘inferentialist’ account within general philosophy, where rather than seek the denotation of our terms, we look to understand the role they play in our inferences. With regard to logical connectives this goes right back to Wittgenstein: don’t look for the denotation of ‘and’, look instead at its grammatical role.

What I’m suggesting here is that one could make a case for all of the logic that is HoTT to be seen in a similar inferentialist light. In any case, HoTT should throw some cats among some pigeons.

Posted by: David Corfield on February 27, 2020 7:50 AM | Permalink | Reply to this

Re: Type Theory and Propositions

Field was very popular when I first started studying philosophy of mathematics, and I took this to be an indication of the degenerate nature of the discipline (hence the pointed title of my book – Towards a philosophy of real mathematics).

Interesting! When I encountered Field, I was very sympathetic to his project, because I had been trying to understand the theory of parametricity for System F.

Since parametricity lets you conjure the natural numbers out of pure second-order quantification and function types, I thought it ought to be possible to formulate a parametric dependent type theory validating an approach in the style of the ideas surrounding nominalism/fictionalism/logicism.

At the time I recall being very impressed by Thomas Fruchart and Giuseppe Longo’s Carnap’s Remarks on Impredicative Definitions and the Genericity Theorem. I’m slightly shocked at thinking about how long ago that was, though.

Posted by: Neel Krishnaswami on February 28, 2020 6:08 PM | Permalink | Reply to this

Re: Type Theory and Propositions

If I can ask a naive question, is this issue of “ontological committment” some kind of Platonist thing? It seems self-evident to me that mathematical objects exist as ideas — given the fact that we can think about them — and why would we need to commit ourselves to any other kind of existence?

Posted by: Mike Shulman on March 2, 2020 6:10 AM | Permalink | Reply to this

Re: Type Theory and Propositions

It’s not a Platonist thing. A better analogy is relative consistency – “the conceptual machinery required to believe X also lets you build Y, as well.”

Because philosophers tend to work with untyped first-order logic, the interpretation of all the quantifiers ranges over a common universe of discourse. So believing in one thing can mandate your belief in surprisingly many other things, as well, because everything the quantifiers range over has been cooked together in one big pot of soup.

Hence David’s remarks that the monopoly of FOL has misled philosophers about the philosophical conclusions they must draw; many apparent ontological commitments disappear if you are willing to make type distinctions in the syntax.

However, one thing that puzzles me is that even long before we reach dependent type theory, multi-sorted FOL could have had many of the same benefits, and I don’t know why philosophers have not used it for much? (Or maybe I just don’t know enough philosophy.)

Posted by: Neel Krishnaswami on March 2, 2020 12:34 PM | Permalink | Reply to this

Re: Type Theory and Propositions

I just don’t see how believing that “two” exists as an idea entails any sort of ontological committment beyond that required to have any sort of discussion at all, or how any machinery could mandate believing in sort of existence beyond that.

Posted by: Mike Shulman on March 2, 2020 3:13 PM | Permalink | Reply to this

Re: Type Theory and Propositions

There’s not exactly a general rule. For a general account see SEP.

But, if you buy into the Quine-Putnam argument, you’ll be committed to the existence of sets and numbers since they feature in our best science. Then it will be necessary for you to explain what kinds of entity you take these to be. An apparently reasonable option is to take them to be abstract entities. Then, so goes the thought, you owe us an explanation of how we can know things about abstract entities. If we take knowledge and reference to work according to some kind of casual relationship, you would have to explain how it is possible to enter into a causal relationship with an abstract entity.

It was this kind of consequence that led Field to want to rewrite statements of applied mathematics. He looks to do this for physics, but in the case of arithmetic this kind of rewriting might take us from ‘There are two apples on my desk’ to ‘There exists x, y, such that x and y are spacetime regions (in contact with my desk now), x and y are disjoint, x and y are apples, and other spacetime region of this kind which is an apple is either x or y’.

So ‘2’ disappears, and we don’t have to worry about commitment to it as an abstract entity.

Posted by: David Corfield on March 2, 2020 1:30 PM | Permalink | Reply to this

Re: Type Theory and Propositions

Is an “abstract entity” something in between a Platonic object and an idea? Why would one choose to take sets and numbers to be “abstract entities” rather than simply ideas?

Posted by: Mike Shulman on March 2, 2020 2:38 PM | Permalink | Reply to this

Re: Type Theory and Propositions

Cans of worms are opening up at every step, but this from Lowe would not be an atypical naming convention (SEP: object):

‘Thing’, in its most general sense, is interchangeable with ‘entity’ or ‘being’ and is applicable to any item whose existence is acknowledged by a system of ontology, whether that item be particular, universal, abstract, or concrete. In this sense, not only material bodies but also properties, relations, events, numbers, sets, and propositions are — if they are acknowledged as existing — to be accounted ‘things’.

From this standard view, seeing numbers as a kind of thing/entity (abstract ones) tallies with the way we appear to predicate and quantify so similarly:

  • This apple is green. There exists an apple that is green.
  • This proposition is true. There exists a proposition that is true.
  • Two is prime. There exists a number that is prime.
  • The set of natural numbers is of infinite cardinality. There exists a set of infinite cardinality.

Then one would have to say something about what makes for an entity to be abstract, how it can be concretely instantiated, and so on. If you’d like ‘ideas’ to play the role of abstract entities, you’ll have to do likewise.

If, on the other hand, you take ‘ideas’ to have a different meaning, you’ll have to tell us what this is. Are there non-mathematical ideas, perhaps one or some of: ‘justice’, ‘democracy’, ‘value’, ‘knowledge’, …?

You can perhaps see the advantage of the inferentialist looking to explain the meaning of terms by the roles they play in acceptable inference steps, rather than troubling about their reference.

Posted by: David Corfield on March 2, 2020 4:06 PM | Permalink | Reply to this

Re: Type Theory and Propositions

you owe us an explanation of how we can know things about abstract entities… you would have to explain how it is possible to enter into a causal relationship with an abstract entity… one would have to say something about what makes for an entity to be abstract… If you’d like ‘ideas’ to play the role of abstract entities, you’ll have to do likewise… [if] you take ‘ideas’ to have a different meaning, you’ll have to tell us what this is.

Perhaps, for some meaning of “one” and “you”. (-: Whoever it is that feels that this work needs to be done is welcome to do it. But even if one accepts that this work has to be done, I don’t see how it can cast any doubt on the ontological status of ideas or abstract entities, or suggest that anyone could avoid accepting their existence in the sense appropriate to them.

Posted by: Mike Shulman on March 4, 2020 11:27 PM | Permalink | Reply to this

Re: Type Theory and Propositions

Your description of Field’s approach is very interesting to me. It seems like he’s saying that he only wants to “cut eliminate” all uses of these abstract entities. While this seems utterly impractical for a working mathematician, the idea that ultimately all uses of abstract entities can be removed from an argument is somewhat sensible as long as the statements themselves don’t involve any abstract entities. It reminds me of the concept of a conservative extension of a logic: the extension adds some new constructs, but ultimately any proof in the larger logic can be “cut eliminated” into a (possibly much longer) proof in the smaller logic. Doesn’t sound much different from what I understand of Hilbert’s view of infinite sets.

Posted by: Max S. New on March 2, 2020 6:13 PM | Permalink | Reply to this

Re: Type Theory and Propositions

It seems like he’s saying that he only wants to “cut eliminate” all uses of these abstract entities. While this seems utterly impractical for a working mathematician, the idea that ultimately all uses of abstract entities can be removed from an argument is somewhat sensible as long as the statements themselves don’t involve any abstract entities.

Sounds like a good argument for becoming an ultrafinitist! :-P

Posted by: David Roberts on March 2, 2020 8:10 PM | Permalink | Reply to this

Re: Type Theory and Propositions

This is odd. We now have two people sympathetic to Field’s approach, including Neel back here.

How about redoing this rewriting in type theory? Say we have a type, AA, which is a set. Then the proposition ‘There are 2 AAs’ could be

x:A y:A(xy)× z:A((z=x)+(z=y)). \| \sum_{x:A} \sum_{y:A} (x \neq y) \times \prod_{z: A} ((z = x) + (z = y)) \|.

Is anything gained by that? With inductive types in the system is there any need for this?

Anyway, according to my line of thought, we’re already dealing with an abstraction when we say of a proposition that it’s true.

Posted by: David Corfield on March 3, 2020 8:39 AM | Permalink | Reply to this

Re: Type Theory and Propositions

The theorem (due to Field 1980) is this.

Let a signature σ\sigma be given, where we assume that all the predicates in σ\sigma apply to atoms (or urelements). Then take a standard system for mathematics with atoms, say ZFA σZFA_{\sigma}: this assumes a set of atoms; and it allows separation and replacement instances to contain formulas with all predicates for the combined, extended language (i.e., the extended language contains the predicates from σ\sigma, as well as a predicate At(x)At(x) and the predicate xyx \in y). Call the basic language L(σ)L(\sigma) and the extended language L(σ A,)L(\sigma_{A,\in}).

Field’s conservativeness theorem says that if you can prove an L(σ)L(\sigma) sentence ϕ\phi in applied set theory ZFA σZFA_{\sigma}, then it is logically true. So let ϕL(σ)\phi \in L(\sigma) and let ϕ A\phi^A be its relativization to “xx is an atom”. Then:

If ZFA σϕ AZFA_{\sigma} \vdash \phi^A then ϕ\vdash \phi.

A model-theoretic proof is this. Suppose ϕ\nvdash \phi. By the completeness theorem, there is a model N¬ϕN \models \neg \phi. One can define a transfinite sequence V α(N)V_{\alpha}(N) of models for the extended language, over NN (essentially the usual von Neumann universes, but built up from a base model NN containing urelements/atoms). Also, the “reduct” of these down to L(σ)L(\sigma), treating the extension of the predicate At(x)At(x) to be the domain is exactly the base model NN. This implies V α(N)ϕ AV_{\alpha}(N) \models \phi^A iff NϕN \models \phi. We can show V ω+ω(N)ZFA σV_{\omega + \omega}(N) \models ZFA_{\sigma}. Moreover, it follows from the previous sentence that V ω+ω(N)¬ϕ AV_{\omega + \omega}(N) \models \neg \phi^A. So, V ω+ω(N)V_{\omega + \omega}(N) is a model of ZFA σZFA_{\sigma}, but ϕ A\phi^A is false in V ω+ω(N)V_{\omega + \omega}(N). So, ZFA σϕ AZFA_{\sigma} \nvdash \phi^A. Contraposition gives the theorem.

Posted by: Jeffrey Ketland on March 3, 2020 4:23 PM | Permalink | Reply to this

Re: Type Theory and Propositions

V ω+ω(N)ZFA σV_{\omega + \omega}(N) \models ZFA_{\sigma}

Maybe this was supposed to be V ω+ω(N)ZA σV_{\omega + \omega}(N) \models ZA_{\sigma} or something? I was pretty sure replacement needs a lot more ranks than that.

Of course, this is tangential to the point about set theory being conservative for purely “logical” statements.

Posted by: Matt Oliveri on March 3, 2020 8:06 PM | Permalink | Reply to this

Re: Type Theory and Propositions

Oops - thanks, yes. Well spotted!

It should say V ω+ω(N)ZAV_{\omega+\omega}(N) \models ZA (and α\alpha inaccessible for ZFAZFA).

If we weaken applied set theory to remove axiom of infinity, then its V ω(N)V_{\omega}(N).

Posted by: Jeffrey Ketland on March 4, 2020 1:57 AM | Permalink | Reply to this

Re: Type Theory and Propositions

I think what often gets glossed over in philosophy are the differences between a proposition, its being true and a judgement that it is true, as pointed out by Per Martin-Löf in Truth of a Proposition, Evidence of a Judgment, Validity of a Proof.

We articulate a sentence and mean by it that the corresponding proposition is true, rather than doing so just to refer to the proposition as a type. This truth claim is to do just as much ‘work’ as to define a type in the world, such as apples now on my table, and judge it to be structurally equivalent to an abstract type, such as Fin(2)Fin(2).

Posted by: David Corfield on February 27, 2020 10:47 AM | Permalink | Reply to this

Re: Type Theory and Propositions

So, to the extent that we should care about “ontological commitments”, and that they are something evidently supposedly required in order to use set theory:

Most type constructors also come with ontological commitments–I would expect–simply because of metamathematical results relating various type systems to various corresponding theories based on predicate logic. For example, having a natural numbers type almost certainly makes the same commitments as some theory of arithmetic.

Posted by: Matt Oliveri on March 3, 2020 8:12 PM | Permalink | Reply to this

Re: Type Theory and Propositions

For the inferentialist, the classic case of finding out that a word is merely playing a role in inference rather than denoting anything is that of logical conjunction. ‘And’ means nothing more nor less that is given by its introduction/elimination/computation rules, etc.

Since conjunction is just binary product in the case of types that are propositions (though there’s a much more interesting story to tell about a ‘dependent and’, see Chap. 2), we should be able to extend the inferentialist picture here. But then is there something different about the type formation rule for product in the context of two specified types, and the type formation rule for the empty type in the empty context? Why should one rule be commitment-inducing and not the other?

And then what of forming the inductive type which is the natural numbers?

My ontological-commitment sensor isn’t very well-developed.

Posted by: David Corfield on March 4, 2020 7:54 AM | Permalink | Reply to this

Re: Type Theory and Propositions

But then is there something different about the type formation rule for product in the context of two specified types, and the type formation rule for the empty type in the empty context? Why should one rule be commitment-inducing and not the other?

Yes, I understood your point. The type constructors present in first-order logic do not seem to make additional commitments merely by considering them type constructors.

And then what of forming the inductive type which is the natural numbers?

My ontological-commitment sensor isn’t very well-developed.

My point was the concern that people who care a lot about ontological commitment may (quite possibly accurately) decide that the type theoretic perspective doesn’t shed much light on the issue.

Posted by: Matt Oliveri on March 4, 2020 9:53 AM | Permalink | Reply to this

Re: Type Theory and Propositions

Quine’s notion of “ontological commitment” for a theory TT amounts to: TT is ontologically committed to FFs iff TT implies “there exists an xx such that F(x)F(x)”.

See eg Alonzo Church 1958, “Ontological commitment”, Journal of Philosophy.

https://www.jstor.org/stable/2021909?seq=1

E.g., this is the kind of example Quine discusses:

(1) P(a)P(a) doesn’t imply Xhas(a,X)\exists X \ has(a, X).

For this, one needs a comprehension axiom of some kind.

But

(2) P(a)P(a) does (typically) imply xP(x)\exists x \ P(x).

The caveat is that this assumes that the constant aa denotes (which is presumed in first-order non-free logic). In some cases in natural language though, it doesn’t. E.g., “Pegasus doesn’t exist” doesn’t imply “There exists something that doesn’t exist”. Rather, “Pegasus” is a non-denoting name.

This is why Quine rejects the presumption that a predicate automatically denotes something and the presumption that a constant automatically denotes something. In “On what there is”, Quine makes the amusing suggestion of replacing names with predicates, like pegasize(x)pegasize(x). So “Pegasus doesn’t exist” gets formalized as: ¬xpegasize(x)\neg \exists x \ pegasize(x).

There are alternatives to Quine’s nominalism about fictional objects. For example, in one of the standard free logics (dual domain positive semantics), “Pegasus doesn’t exist” gets formalized (in the meta-theory) by saying “Pegasus is in the outer domain”.

Some more examples.

(3) “I did that for the sake of my friend Bob” does not imply “There is an xx such that xx is the sake of Bob” (at least, not obviously)

Quine says that the adverbial phrase “for the sake of X” is syncategorematic.

Geach and Kaplan gave this example (though Boolos prefers to use plural logic for this). Let the signature σ\sigma be {"critic","admires"}\{\text{"critic"}, \text{"admires"}\}, where “critic” is a unary predicate and “admires” is a binary predicate. Let L(σ)L(\sigma) be the first-order language over σ\sigma. Let L 2(σ)L_2(\sigma) be the second-order language over σ\sigma. Let L (σ)L_{\in}(\sigma) be the first-order language over σ{}\sigma \cup \{\in\}. Then

(4) “Some critics admire only each other” cannot be expressed in L(σ)L(\sigma).

But:

(5) “Some critics admire only each other” can be expressed in in L 2(σ)L_2(\sigma) and L (σ)L_{\in}(\sigma).

Boolos himself discusses examples like the following.

Let the signature σ\sigma be {"Napoleon","Donald","parent-of"}\{\text{"Napoleon"}, \text{"Donald"}, \text{"parent-of"}\}, where “Napoleon” and “Donald” are constants and “parent-of” is a binary predicate. Let L(σ)L(\sigma) be the first-order language over σ\sigma. Let L 2(σ)L_2(\sigma) be the second-order language over σ\sigma. Let L (σ)L_{\in}(\sigma) be the first-order language over σ{}\sigma \cup \{\in\}. Then

(6) “Napoleon is not an ancestor of Donald” cannot be expressed in L(σ)L(\sigma).

But

(7) “Napoleon is not an ancestor of Donald” can be expressed in L 2(σ)L_2(\sigma) and L (σ)L_{\in}(\sigma).

I.e., “There exists a relation RR which is the transitive closure of “parent-of” and (Napoleon, Donald) is not an element of RR”.

Boolos argues in his

“To Be is to be a Value of a Variable (or to be Some Values of Some Variables)” (1984, Journal of Philosophy)

that comprehension in L 2(σ)L_2(\sigma) is not committed to the existence of pluralities as objects; rather it is a primitive form of “plural quantification”. Personally, I don’t buy it. I agree with Quine that second-order logic is “set-theory in sheep’s clothing”.

As Harvey Friedman’s Reverse Mathematics Programme has shown, many well-known mathematical theorems can be shown to be equivalent (modulo RCA 0RCA_0) to certain set existence principles. For example, the Bolzano-Weierstrass Theorem is equivalent to ACA 0ACA_0: i.e., the set existence axiom:

(8) Xn(nXϕ(n))\exists X \forall n \ (n \in X \leftrightarrow \phi(n))

where ϕ(n)\phi(n) contains no set quantifiers.

This comprehension axiom asserts the existence of the set X={nϕ(n)}X = \{n \in \mathbb{N} \mid \phi(n)\}, defined by the arithmetic formula ϕ(n)\phi(n). So, the ontological commitments of The Bolzano-Weierstrass Theorem are (modulo RCA 0RCA_0) the arithmetically definable sets of numbers (with number and set parameters, to be exact).

Zermelo’s original set theory Z\mathsf{Z} implies the existence of the von Neumann ranks V αV_{\alpha} with α<ω+ω\alpha &lt; \omega + \omega. But it does not imply the existence of V ω+ωV_{\omega + \omega}. For that, one needs Replacement.

I guess one might also think these abstract looking set existence axioms must be irrelevant to mathematics down at the arithmetic or computational level. But in fact, stronger and stronger set existence axioms prove more and more new arithmetic (indeed Π 1\Pi_1) sentences and they speed up proofs of sentences already provable.

Posted by: Jeffrey Ketland on March 8, 2020 10:41 PM | Permalink | Reply to this

Re: Type Theory and Propositions

Perhaps another advantage of adopting dependent type theory then, since we won’t be able to write “there exists an xx such that F(x)F(x)”.

Posted by: David Corfield on March 9, 2020 5:49 PM | Permalink | Reply to this

Re: Type Theory and Propositions

What would replace A[Ax(xAx +A)]\exists A \ [\varnothing \in A \wedge \forall x (x \in A \to x^{+} \in A)], say? Or Xn(nXϕ(n))\exists X \forall n \ (n \in X \leftrightarrow \phi(n)), say? If it is equivalent, how is that proved and what is the point of making a fuss about equivalents? If not equivalent, what is the justification?

Posted by: Jeffrey Ketland on March 9, 2020 6:44 PM | Permalink | Reply to this

Re: Type Theory and Propositions

To answer such questions would require giving an account of how type theory goes about its business, what it does if it doesn’t operate via first-order logic + set axioms. The role of its ‘rule schemas’: dependent products, inductive types, and universes.

I don’t know what you know about type theory, so I’m not going to be able to do better here than refer you to some of Mike’s writings, in brief the post From Set Theory to Type Theory and the article written for philosophers, Homotopy type theory: the logic of space. Then, of course, there’s the HoTT book.

Posted by: David Corfield on March 10, 2020 8:47 AM | Permalink | Reply to this

Re: Type Theory and Propositions

Sure - type theory was invented by Russell (1903, 1908, 1912) and classic formulations given by Church, and then developed in countless various ways later, including what is now called higher-order logic. What Godel showed incomplete in 1931 was in fact type theory (Russell/Whitehead’s Principia). Lambda-abstraction (and higher-order logic) was invented by Frege, modified in certain ways by Russell, and then redeveloped by Church and others later. It’s implemented in modern programming languages. Combinators were invented by Schonfinkel and Curry. (A version became Quine’s predicate-functor logic.)

On your idea that existential quantifiers should be banned, I doubt that mathematicians will stop writing down ϵ\epsilon-δ\delta definitions and the like; or expressing that a function is surjective by saying “for any nn \in \mathbb{N}, there is some kk \in \mathbb{N} with n=f(k)n = f(k)”, etc.

Posted by: Jeffrey Ketland on March 10, 2020 9:19 PM | Permalink | Reply to this

Re: Type Theory and Propositions

Where did I say that existential quantifiers should be banned? I was simply pointing out that they won’t occur in the standard untyped way.

Of course, one will be able to express surjectivity of a function. Look at Definition 4.6.1 of the HoTT book. See how it’s done. The function, ff, is given to us with domain and codomain. The preimage of b:Bb:B is given as the type fib f(b)fib_f(b) (see Def 4.2.4 for how this is defined as a dependent sum). Then we’re looking to see that its propositional truncation, fib f(b)\|fib_f(b)\|, is inhabited for each bb.

The HoTT form of existential quantification is given by truncating (forming the bracket type of) a dependent sum (aka dependent pair).

So we have A:TypeA:Type and, given a:Aa:A, a proposition (i.e., a type with at most one element) B(a):PropB(a):Prop. Then the dependent sum is x:AB(x)\sum_{x:A}B(x), which collects pairs (a,p)(a, p) where a:Aa:A and pp is a warrant that BB holds of aa.

Then to express the proposition ‘There is an AA which is BB’, we truncate the dependent sum, x:AB(x)\| \sum_{x:A}B(x)\|. If I have a case of an AA which is BB, I can use this element to establish that ‘There is an AA which is BB’.

Posted by: David Corfield on March 11, 2020 9:27 AM | Permalink | Reply to this

Re: Type Theory and Propositions

I think Jeffrey was responding to your comment that

we won’t be able to write “there exists an xx such that F(x)F(x)”.

which sounds on a naive reading like it may be intending to ban existential quantifiers.

Posted by: Mike Shulman on March 11, 2020 5:27 PM | Permalink | Reply to this

Re: Type Theory and Propositions

There is an existential quantifier within type theory; it’s just that it’s constructed from the Σ\Sigma-type and propositional truncation rather than being a basic thing. I’m not sure quite what David meant, since he knows that, but maybe he was making the same point I was below that the notion of “ontological committment” needs to be modified for theories that aren’t built up from first-order logic.

Posted by: Mike Shulman on March 11, 2020 1:24 AM | Permalink | Reply to this

Re: Type Theory and Propositions

But it will then be a matter of translation. If someone says to me, “PAPA is really just about numbers”. I’d say, “Ok, but PAPA interprets finitary set theory ZF finZF^{fin} by translation; so PAPA can also be said to be about finite graphs, models, trees, etc.” No mathematician thinks a finite tree or a finite graph actually is a number (the number encoding it), etc. But these encodings reveal how strong various axioms/theorems are. So, probably with some careful choice of assumptions, there’ll be a version of the type theory you’re interested in which amounts to (i.e., is bi-interpretable with) ACA 0ACA_0 (which asserts the existence of arithmetically definable sets). The point about these latter systems is that their proof-theoretic strength has been very carefully calibrated over the last sixty years or so.

Incidentally, you might like to read together Quine’s 1948, Church’s 1958, Carnap’s 1950 and the Quine-Carnap debate. Also there’s a very nice new SEP entry written by Hannes Leitgeb and Andre Carus, “Rudolf Carnap” (esp. Sc 7).

Posted by: Jeffrey Ketland on March 11, 2020 5:54 AM | Permalink | Reply to this

Re: Type Theory and Propositions

I’m not sure quite what David meant…

Since David didn’t say that there wasn’t existential quantification, wonder no more.

I’ve just given above some account of what you say about propositional truncation of dependent sum types.

he was making the same point I was below that the notion of “ontological committment” needs to be modified for theories that aren’t built up from first-order logic.

I am making just that point, which is why we had better not give the impression that type theory is providing some minor variant on what much of analytic philosophy takes to be quantification.

The situation is much worse than you have back here:

Personally, I think this aspect of structural-set theory matches mathematical practice more closely. When I say “for all x,x 20x \in \mathbb{R}, x^2 \geq 0”, I regard it as a property of every real number that its square is nonnegative. I don’t regard it as a property of every thing in mathematics that if it happens to be a real number, then its square is nonnegative.

With their untyped quantifiers, there’s no reason to think quantifiers range only over somewhat delimited ranges, such as every mathematical object. When I say ‘All elephants are mammals’, the quantifier can range over absolutely everything - the cup of coffee on my desk, the Declaration of Independence, the number 3 and the planet Venus.

Small wonder quantifiers play such strange ontological roles in mainstream analytic philosophy.

Posted by: David Corfield on March 11, 2020 9:46 AM | Permalink | Reply to this

Re: Type Theory and Propositions

You say your quantifier “all” doesn’t range over the cup of coffee on my desk, the Declaration of Independence, the number 3 and the planet Venus; and then admit it does, since you refer to them!

Suppose we let X:={the cup of coffee on my desk,the Declaration of Independence,3,Venus}X: = \{\text{the cup of coffee on my desk}, \text{the Declaration of Independence}, 3, Venus\}.

I can then say, “The set of things David’s comment referred to is X. It has four elements”.

Is XX a type? What are its “introduction rules”? Normally, one would use some form of comprehension, amounting to:

Xw(wX((w=the cup)(w=the Declaration)(w=3)(w=Venus)))\exists X \forall w \ (w \in X \leftrightarrow ((w = \text{the cup}) \vee (w = \text{the Declaration}) \vee (w = 3) \vee (w = Venus))).

Is this forbidden?

Posted by: Jeffrey Ketland on March 11, 2020 1:52 PM | Permalink | Reply to this

Re: Type Theory and Propositions

In type theory, you can’t take elements that belong to distinct types and collect them into a new type. You can take a “subtype” of an existing type, i.e. you have separation, but not global comprehension (and not untyped union). If a:Aa:A and b:Bb:B the closest thing you can have to the set {a,b}\{a,b\} is something like a subset of the disjoint union A+BA+B consisting of inl(a)\inl(a) and inr(b)\inr(b).

Posted by: Mike Shulman on March 11, 2020 5:30 PM | Permalink | Reply to this

Re: Type Theory and Propositions

Yes, indeed. I know! The key here, as you say, is separation and union over types/classes/sets/what have you. I want to be able to assert that there are collections or sets of whatever variety I like. This can arise in applications, particularly semantic ones. Given a cup, a declaration, the number 3 and the planet Venus, there is a set X={the cup,the declaration,3,Venus}X = \{\text{the cup}, \text{the declaration}, 3, Venus\}; and it has four elements. But is this a type? I don’t mind saying each of the cup, the declaration, 3 and Venus are ur-elements (atoms). So, each lacks elements; and each is, from the point of view of the membership relation, a “structureless point”. Even so, if I assume the atoms form a set, Zw(wZatom(w))\exists Z \forall w \ (w \in Z \leftrightarrow \text{atom}(w)), along with the axioms that each of the above is an atom, then separation (along with a formula stating the disjunction of the four clauses) will give me XX and standard reasoning (assuming distinctness of the cup, the declaration, 3 and Venus) will give me |X|=4|X| = 4.

Actually, I don’t quite know how to show Venus3Venus \neq 3, even though it seems true. This is called “The Julius Caesar Problem” and was raised by Frege in 1884—about 80 years before Benacerraf famously raised the more general problem about sentences like “2={,{}}2 = \{\varnothing, \{\varnothing\}\}”, “2102 \in 10”, etc. Perhaps one should say, and it seems natural to say, they belong to “ontologically different categories”. But this goes far deeper into traditional ontology than mere questions about whether there are, say, infinite sets, etc.

Posted by: Jeffrey Ketland on March 11, 2020 6:18 PM | Permalink | Reply to this

Re: Type Theory and Propositions

Something relevant here is the object classifier, Type^Type\widehat Type \to Type. We can think of Type^\widehat Type as the type of pointed types (p. 143 of the HoTT book). An element of this type is a pair consisting of a type, AA, and an element a:Aa:A. We might call it the type of terms.

I will already have introduced the terms I mention as elements of already formed types: the cup: Cup, the declaration: Event, 3: Nat, Venus:Planet.

Then I can form the subtype of Type^\widehat Type that is ‘the terms I just mentioned’. This subtype is a set of cardinality 4.

Posted by: David Corfield on March 13, 2020 9:37 AM | Permalink | Reply to this

Re: Type Theory and Propositions

I will already have introduced the terms I mention as elements of already formed types: the cup: Cup, the declaration: Event, 3: Nat, Venus:Planet. Then I can form the subtype of Type^\hat{Type} that is ‘the terms I just mentioned’;. This subtype is a set of cardinality 4.

How do you know that there are such types as Cup, Event, \dots; and how do you know that there is a type of Terms-I-Just-Mentioned?

Is this not simply separation/comprehension? So, when you say, “we can form a type”, really this just means comprehension.

Posted by: Jeffrey Ketland on March 13, 2020 12:24 PM | Permalink | Reply to this

Re: Type Theory and Propositions

Yes, of course type theory has separation. It’s represented by a sigma-type: {x:AP(x)}= x:AP(x)\{ x:A \mid P(x) \} = \sum_{x:A} P(x), which makes sense since each proposition P(x)P(x) is itself a type. This is discussed in section 3.5 of the HoTT Book. Note that it truly is separation and not (unrestricted) comprehension: you can only collect together a “subtype” of things that already belong to the same type.

Of course ZFC also has only separation and not unrestricted comprehension; the difference is that ZFC has untagged unions. So once you have sets CupCup and EventEvent, ZFC will let you form CupEventCup\cup Event whose elements are all cups and also all events, and then apply separation to that. Whereas in type theory from two given types you can only form a disjoint union Cup+EventCup+Event, whose elements are “cups tagged with the fact that they are cups” and “events tagged with the fact that they are events”. David’s Type^\widehat{Type} is just the disjoint union of all types in the universe, tagged with the type that they belong to.

This solves the problem of whether Venus=3Venus=3 by declaring it a meaningless question: you can only compare two things for equality when they belong to the same type. After you put them into a disjoint union you can compare them, asking whether (say) inl(Venus)=inr(3)inl(Venus) = inr(3), but in that case the answer is always no because the union is disjoint: two things with different tags can never be equal.

The question of how you get a type like CupCup in the first place is not, I would say, really a mathematical or logical one. From the perspective of logic, we just assume given some mathematical objects that we may regard as representing real-world objects. (The mathematical objects discussed by mathematical theories like FOL and MLTT can’t, of course, literally be things like cups or planets.) If we are using FOL/ZFC, we start with one collection of urelements and then start grouping them into sets with the ZFC axioms, but if we are using dependent type theory it’s natural to instead start with multiple types of urelements.

Posted by: Mike Shulman on March 13, 2020 8:45 PM | Permalink | Reply to this

Re: Type Theory and Propositions

Declaring “Venus = 3” meaningless prevents us from concluding, e.g., that the set of things David mentioned in the conversation is {Venus,3}\{Venus, 3\}, and it has cardinality 2. To conclude this, we’d need the assumption that Venus3\Venus \neq 3. I agree that Venus and 3 are very different, perhaps living in “ontologically different categories”. But this surely tells me that Venus3\Venus \neq 3! I can see how you get around this with tagged types. But why not just have “Venus3Venus \neq 3” true to begin with?

Programming languages have the option of, e.g., using “==” which requires matching type, or using, e.g, “is” in Python and “identical(.,.)” in R, which permits distinct types and which test for exact equality. The philosopher’s identity predicate is always “identical”, and not the type-dependent “==”.

The mathematical objects discussed by mathematical theories like FOL and MLTT can’t, of course, literally be things like cups or planets.

That’s a very interesting comment, as I think my view would be the opposite (I’d guess all philosophers working in this area would say something similar). They’re cups, planets, etc.! After all, unless one has urelements, one doesn’t have applicable mathematics. (I come back to the second bit of the comment, on dependent types, at the bottom below.) Examples just using “set theory with urelements” would be things like

(1) The set of elephants is a subset of the set of mammals.

(2) The cardinal of the set of left-handed people is less than the cardinal of the set of right-handed people.

(3) There is no injective function from the set of people in this room to the set of handouts that I have printed.

(4) If the ordered pair (P,R)(P, R) of the set of spacetime points and their order relation satisfies conditions A 1,,A nA_1,\dots,A_n, then there is a isomorphism from (P,R)(P,R) to (,)(\mathbb{N},\leq).

(5) Napoleon is not an element of the set of all humans which contains Quine and is closed under the relation of being a parent-of.

(6) If LL is the set of land-areas in Konigsberg, BB the set of bridges there, and CC the connection relation (a function assigning to each bridge in BB a pair {x,y}\{x,y\} of land-areas from LL), then (L,B,C)(L,B,C) is a multigraph which has no Euler cycle.

A foundational account of mathematics must satisfy the condition that it shows how mathematics is applicable to non-mathematical subject matter. Frege stated a similar condition. Field’s approach does too (but by arguing it’s dispensable). Quine’s philosophy of mathematics is based on this. Putnam wrote an influential book on this. All of measurement theory is predicated on this.

This is partly why I’m interested in how comprehension (i.e., separation) operates here—to give various basic types, and derivative types obtained by products, etc. I’m also a bit curious about how HoTT (maybe with various modifications) would be “located” in the proof-theoretic interpretation hierarchy, from QQ at the bottom to ZFCZFC+large cardinals in the upper part.

Also, consider again Field’s conservativeness result I sketched above. We have a signature σ\sigma which does not contain \in or any mathematical vocabulary. The corresponding language is L(σ)L(\sigma). Call the extended language (obtained by adding “xyx \in y” and “At(x)At(x)”) L (σ)L_{\in}(\sigma). ZFA σZFA_{\sigma} is then set theory with atoms adapted to this signature. It has an axiom asserting there is a set of atoms (urelements), and has separation and replacement for any formula from L (σ)L_{\in}(\sigma). Then, for any ϕ\phi in the “non-mathematical” sublanguage L(σ)L(\sigma), we have:

(C) If ZFA σϕ AZFA_{\sigma} \vdash \phi^A then ϕ\vdash \phi

(ϕ A\phi^A is the relativization of ϕ\phi’s quantifiers to At(x)At(x))

I’m worried how one would express something corresponding to this on the HoTT approach.

(C) says that if ϕ A\phi^A is provable in ZFA σZFA_{\sigma}, then ϕ\phi is provable in plain logic alone. This shows one way that mathematics is eliminable in reasoning from an empirical assumption ϕ 1\phi_1 to an empirical conclusion ϕ 2\phi_2. Mathematics “speeds up” the reasoning, maybe by a huge amount; but even so, it’s eliminable. cf ACA 0ACA_0 is conservative over PAPA, but has non-elementary speed-up over PAPA.

If a foundational account is to generate interest, it must analyse applicability and show how it is possible. Perhaps it can show how mathematics can be eliminated when reasoning about points, regions, electrons, wavefunctions, Konigsberg bridges, etc.; or perhaps it can show how it is non-eliminable (Quine & Putnam’s view).

Back to the second part of Mike’s original comment:

If we are using FOL/ZFC, we start with one collection of urelements and then start grouping them into sets with the ZFC axioms, but if we are using dependent type theory it’s natural to instead start with multiple types of urelements.

Yes, but how do we decide which types exist? If I happen to have some basic (linguistic) predicates “xx is an aardvark”, “xx is a cup”, etc., can I simply promote each to a type—Aardvark, Cup, etc.? What do you say to an adamant nominalist who says, “Sets and types don’t exist. They’re abstract entities, and I reject the existence of abstract objects: all objects are concrete things in space and time. It’s no progress to replace sets by types. They’re just as bad as each other”?

Posted by: Jeffrey Ketland on March 13, 2020 11:26 PM | Permalink | Reply to this

Re: Type Theory and Propositions>

The philosopher’s identity predicate is always “identical”, and not the type-dependent “==”.

I very much hope you’re presenting this as an empirical observation and not some conceptual truth, an essential characteristic of what it is to be a philosopher.

I end chapter 2 of my book with a quotation from Brandom

…when we appreciate the modal commitments implicit in the use of all empirical descriptive vocabulary, we see that strongly cross-sortal identity claims-–those that link items falling under different sortal predicates with different criteria of identity and individuation–-are never true,

and add

With type theory as our means of expression, it’s not just that these claims are never true. Rather, such identity types are not well-formed, and as such are uninhabitable.

There are things to say with reference to Brandom’s ‘strongly’, but I’ll leave these to a future post on type dependency.

Posted by: David Corfield on March 14, 2020 9:15 AM | Permalink | Reply to this

Re: Type Theory and Propositions>

[quote from Brandom]

…when we appreciate the modal commitments implicit in the use of all empirical descriptive vocabulary, we see that strongly cross-sortal identity claims-–those that link items falling under different sortal predicates with different criteria of identity and individuation–-are never true,

Which is what I said! Philosophers working on this topic generally treat identity claims as determinately false when relating fundamental distinct domains. This simply confirms my point. The relevant notion (as Brandom makes clear) is the “is” of Python, or “identical” of R, and not the type-dependent “==”. Ask any normal speaker about the planet Venus and the number 3. Ask—are these the same thing? They’ll likely say, “No”—just as Brandom predicts.

There is a debate about “relative identity”, going back to Geach in the 60s. I do know all the arguments, and I’m not going to be convinced by repetition of the same old arguments, I’m afraid. I doubt most experts who are into this stuff will either.

Posted by: Jeffrey Ketland on March 14, 2020 1:54 PM | Permalink | Reply to this

Re: Type Theory and Propositions

We may well have reached the bedrock where our ‘spades turn’.

On the other thread I mentioned three consecutive Waynflete professors. To return to them here:

Collingwood would say something like: a proposition only makes sense in a series of questions and answers. The question ‘Are Venus and 3 the same?’ is not a question that can arise.

Ryle would no doubt say that to pose the question is to make a category mistake. A somewhat relevant quotation I have to hand is:

A man would be thought to be making a poor joke who said that three things are now rising, namely the tide, hopes and the average age of death. It would be just as good or bad a joke to say that there exist prime numbers and Wednesdays and public opinions and navies; or that there exist both minds and bodies.

I can’t see him look kindly on someone wondering about the identity of 3 and Venus.

Strawson: Given his (Collingwoodian) thought that questions about the present king of France do not arise, I would imagine (but am happy to be shown wrong) that he would also say of the question of the identity of Venus and 3 that it doesn’t arise, relevant presuppositions not being in place.

Interesting then to think about their attitudes towards formal logic. Collingwood had little regard for it. Ryle has much more to say about ‘informal logic’. Strawson wrote ‘An Introduction to Logical Theory’ in 1952, but was keen to point out its limitations.

I think it worth pursuing the idea that MLTT, although a formalism, addresses some of the worries of these thinkers. Ruling out an untagged proposition ‘Venus = 3’ is a start. Making good sense of ‘presuppositions’ is another.

Posted by: David Corfield on March 14, 2020 4:26 PM | Permalink | Reply to this

Re: Type Theory and Propositions

Since you raised the question, I asked my theorem prover:

axiomsc("all x -(planet(x) number(x))", "number(3)", "planet(Venus)")axioms \leftarrow \text{c("all x -(planet(x)} \leftrightarrow \text{ number(x))", "number(3)", "planet(Venus)")}

goal"Venus != 3"goal \leftarrow \text{"Venus != 3"}

prove(axioms,goal)prove(axioms, goal)

Output: THEOREM PROVED

QED.

Posted by: Jeffrey Ketland on March 14, 2020 6:09 PM | Permalink | Reply to this

Re: Type Theory and Propositions

I asked my theorem prover:

Axiom Planet : Type.
Axiom Venus : Planet.

Goal ~(Venus = 3).

Error: The term "3" has type "nat" while it is expected to have type "Planet".
Posted by: Mike Shulman on March 14, 2020 7:47 PM | Permalink | Reply to this

Re: Type Theory and Propositions

Haha. Touché…

Posted by: Jeffrey Ketland on March 14, 2020 8:46 PM | Permalink | Reply to this

Re: Type Theory and Propositions

Jeffrey:

Ask any normal speaker about the planet Venus and the number 3. Ask—are these the same thing? They’ll likely say, “No”—just as Brandom predicts.

David:

The question ‘Are Venus and 3 the same?’ is not a question that can arise.

These could both be true. (Other than the question arising in the study of language or philosophy or something.) And if the question doesn’t arise, a formal language can deal with it however’s convenient. Maybe untyped logic really is a good match for philosophy, simply because it will entertain any question, no matter how silly. ;)

Posted by: Matt Oliveri on March 14, 2020 5:23 PM | Permalink | Reply to this

Re: Type Theory and Propositions

I would like to remind the participants (especially Mike) the title of David’s book, which lead to this conversation: “Types in Natural Language”. I know mathematicians don’t ordinarily need their language to compete with natural language on expressiveness, but given the context, I think it’s been claimed that HoTT can help explain features of natural language.

Mike says:

(The mathematical objects discussed by mathematical theories like FOL and MLTT can’t, of course, literally be things like cups or planets.)

But the objects referred to by expressions of natural language can, of course, literally be things like cups and planets. From Jeffrey’s comment, it looks like he is expecting this capability from type theory.

Personally, I’ve wondered what proponents of intrinsically typed language think about this claim of natural language: “Everything is a thing.” To me, this is equivalent to the tautological “Every thing is a thing.” But this doesn’t feel like the tautological metalinguistic claim you could make about a type system; it feels like a tautological ontological claim. I hasten to note that I know of no ontological claims that are not “operationally” (that is, understood in terms of their effects) the same as reflective claims about one’s way of thinking. And the latter seem to be essentially metalinguistic. But the fact remains that in English, they seem like different types of claim.

Posted by: Matt Oliveri on March 14, 2020 2:20 AM | Permalink | Reply to this

Re: Type Theory and Propositions

I would like to remind the participants (especially Mike) the title of David’s book, which lead to this conversation: “Types in Natural Language”.

No, it isn’t. It’s

Modal Homotopy Type Theory: The prospect of a new logic for philosophy

‘Types in Natural Language’ was the title of the post.

Regarding its usefulness in talking about our everyday dealings with the world, our ordinary language, etc., I did provide a quotation there from Ranta suggesting that Martin-Löf was sceptical (as he was of first-order logic). But I was just shown yesterday a transcript of a talk he gave ‘Truth of Empirical Propositions’. I’ll find out if this will become publicly available.

Posted by: David Corfield on March 14, 2020 8:39 AM | Permalink | Reply to this

Re: Type Theory and Propositions

Oh right. Wrong post. Stupid of me.

Posted by: Matt Oliveri on March 14, 2020 8:55 AM | Permalink | Reply to this

Re: Type Theory and Propositions

Good grief! Now I see why philosophers get so confused.

Applicable mathematics is about modeling the real world with mathematical objects. A rectangle of string laid out by a surveyor is not literally a mathematical rectangle consisting of a set of ordered pairs of real numbers — but Euclidean geometry is still indispensable to the surveyor. Water flowing through a pipe does not literally obey the Navier-Stokes equations — yet the equations are still a useful mathematical model. And so likewise, the elements of mathematical sets or types don’t have to (and can’t) “literally be” things like elephants or left-handed people in order for set- and type-theoretic mathematical to be a useful formal system that tells us things about reality — including natural language.

Surely there are philosophers who have taken this (to me self-evident) view.

Posted by: Mike Shulman on March 14, 2020 4:23 AM | Permalink | Reply to this

Re: Type Theory and Propositions

And see that this kind of modelling is going on even when simply applying propositional logic to the world. When I say that it is true that is raining today, the element of the logical/mathematical type, 1\mathbf{1}, is not the element of the proposition ‘It is raining today’, an element we might call ‘the fact that it is raining today’.

Posted by: David Corfield on March 14, 2020 8:52 AM | Permalink | Reply to this

Re: Type Theory and Propositions

Assuming I understand this right, using your proposed truth predicate, I can construct a diagonal sentence

(SS) The type 1\mathbf{1} is an element of SS.

Is the type 1\mathbf{1} is an element of SS?

Posted by: Jeffrey Ketland on March 14, 2020 1:24 PM | Permalink | Reply to this

Re: Type Theory and Propositions

You do not understand right. What on Earth did anyone say that made you think you can make a recursive definition like that? Even if arbitrary recursive definitions were allowed, that attempted definition is nonsense, because there’s no “element of” relation.

Posted by: Matt Oliveri on March 14, 2020 3:02 PM | Permalink | Reply to this

Re: Type Theory and Propositions

Probably David’s remark

… the element of the logical/mathematical type, 1\mathbf{1}, is not the element of the proposition ‘It is raining today’ …

Given any formula ϕ(x)\phi(x), there is some sentence SS such that QSϕ(S)Q \vdash S \leftrightarrow \phi('S'), where S'S' is the godel name of SS and QQ is Robinson arithmetic which is clearly interpretable in HoTT. It will work independently of what the claimed semantic relationship is. All you need is some predicate applied to sentences/formulas, and then you can diagonalize.

Posted by: Jeffrey Ketland on March 14, 2020 3:52 PM | Permalink | Reply to this

Re: Type Theory and Propositions

OK.

… the element of the logical/mathematical type, 1\mathbf{1}, is not the element of the proposition ‘It is raining today’ …

That is a metatheoretic statement, like your

Given any formula ϕ(x)\phi(x), there is some sentence SS such that …

.

Also, type theory has a distinction between judgments and propositions. “Element of” is a judgment form, but not a relation. So if someone is reasoning about element-of, or other judgments, you can tell right away that this is not actually taking place inside the theory.

… and QQ is Robinson arithmetic which is clearly interpretable in HoTT.

That is fine. Is that really what you meant? Why do you bring it up?

Posted by: Matt Oliveri on March 14, 2020 5:02 PM | Permalink | Reply to this

Re: Type Theory and Propositions

Because this isn’t really just propositional logic itself, but rather meta-theory. And the semantic property involved here, expressed by the relevant meta-linguistic predicate, will raise questions of self-applicability, though I’m unsure how to formulate that. That said, I’ve never seen anyone work out a properly formalized version of BHK semantics (e.g. for MLTT, but also more generally), so I don’t quite know how it goes.

(Edit: having written that a while ago, I just looked this up and noticed some papers/talks by Sergei Artemov including “Explicit Provability and Constructive Semantics” (2001) on this topic.)

Posted by: Jeffrey Ketland on March 14, 2020 6:58 PM | Permalink | Reply to this

Re: Type Theory and Propositions

If you’re interested in how incompleteness and MLTT get along together, there’s this MO question.

In the paper Sundholm mentions in his answer, naturally the constructivist position emerges looking good from the encounter.

Posted by: David Corfield on March 15, 2020 9:31 AM | Permalink | Reply to this

Re: Type Theory and Propositions

Ah, thanks. The diagonalization I gave earlier didn’t make sense, and that’s all clearer to me now.

I now looked up the proof-theoretic strength of MLTT, as set out in a nice 2018 survey article by Michael Rathjen (“Proof Theory of Constructive Systems: Inductive Types and Univalence”). By Theorem 6.5 (page 20), the following theories prove the same Π 2\Pi_2 sentences (and have the same consistency strength):

1. T 0 i+ nU nT^i_0 + \bigcup_n U_n (intuitionist version of Feferman’s explicit mathematics, with universes)

2. CZF plus Inacc(n) for all n > 0 (Aczel’s constructive ZF, with inaccessibles).

3. The extensional type theory MLTT extMLTT^{ext}.

4. MLTT.

5. Σ 2 1AC\Sigma^1_2-AC + BI plus Beta(n), for all n > 0 (a system of 2nd order arithmetic)

6. Kripke-Platek set theory KP plus for every n > 0 an axiom asserting that there are at least n-many recursively inaccessible ordinals.

For exactly the same arithmetic content, the list is a bit different.

Posted by: Jeffrey Ketland on March 16, 2020 12:41 AM | Permalink | Reply to this

Re: Type Theory and Propositions

Let me offer my explanation of what I think David was talking about:

… the element of the logical/mathematical type, 1\mathbf{1}, is not the element of the proposition ‘It is raining today’ …

and how far it is from what you seem to be thinking of.

In HoTT, as in set theory, propositions are reflected internally as subsets of some chosen singleton. In set theory, that singleton would typically be {}\{\empty\}; in HoTT it would be 1\mathbf{1}. The subset contains the unique element of the singleton iff the proposition is true.

So you have ():1()\;:\;\mathbf{1} in HoTT, corresponding to {}\empty \in \{\empty\} in set theory. These are the mathematical versions, in the respective systems, of the trivial proof of the logical constant “true”. David was saying that this judgment is not the same as the informal judgment

‘the fact that it is raining today’ : ‘it is raining today’

which witnesses the fact that it’s raining today, because the formal is mathematical and the latter is not. He did not bring up any metamathematical truth predicate or even a formal quoting of formulas.

Posted by: Matt Oliveri on March 14, 2020 7:39 PM | Permalink | Reply to this

Re: Type Theory and Propositions

Well something of the form a:Aa:A is not a proposition, so the construction makes no sense as it stands.

We can judge that the type 1\mathbf{1} belongs to TypeType. Up to issues to do with universes this is the only type it belongs to. We might form by separation some subtype of types that satisfy some property of types. Then asking whether 1\mathbf{1} belongs to that subtype would be to ask whether 1\mathbf{1} satisfies that property.

But I don’t see how I arrive at your construction.

In a similar vein, I mention ‘This sentence is false’ in my book. I suggest a similar answer, which is more or less a Wittgensteinian one, I believe, that I shouldn’t introduce the term ‘this sentence’ until I’ve been presented with one.

Posted by: David Corfield on March 14, 2020 3:38 PM | Permalink | Reply to this

Re: Type Theory and Propositions

FWIW, I agree with all that. Natural language still seems untyped to me though. Typed language can be perfectly adequate and still seem unnatural to many people.

Posted by: Matt Oliveri on March 14, 2020 9:08 AM | Permalink | Reply to this

Re: Type Theory and Propositions

I doubt that Quine, Putnam, Lewis, Burgess and so on are confused! I’ll bat it back and say your view (a form of nominalism) is the confused one.

Applicable mathematics is about modeling the real world with mathematical objects.

Applicable mathematics is about impure sets of physical things, and impure relations of physical things, and mixed functions from physical things to mathematical values (measurement scales, scalar and tensor quantities, etc). One must be able to talk of impure sets of physical objects, and relations amongst them, to apply mathematics. One must be able to talk of mixed functions from some physical objects to, e.g., \mathbb{R}, to do measurement theory—e.g., “the temperature of this coin is 200K”. When a physicist says “Ψ\Psi is a complex-valued function on spacetime” this means “Ψ\Psi takes spacetime points as arguments, and complex numbers as values”. When I apply the Pigeonhole Principle to, e.g., left-handed and right-handed people, I must be able to talk of the set of the former, the set of the latter and functions between them. Without this there is no applied mathematics at all!

(It doesn’t matter if an equation is an approximation, a common phenomenon. For “Schrodinger’s equation is approximate” (which is true) doesn’t imply “The wavefunction doesn’t exist”.)

Here’s a similar example to the above. I reason from some premises about there being 15 people here and 10 handouts to

(P) There is no injection from the set of people here to the set of handouts I made

And that’s true. Suppose ff is a function from the people to the handouts—say, f(p)f(p) is the handout that person pp will look at. It follows that there are two distinct people p 1,p 2p_1, p_2, such that f(p 1)=f(p 2)f(p_1)=f(p_2). So, I can reason from true premises to true conclusions and it’s done by applied mathematics. There is no confusion here. It is correct.

It’s the naive denial which is confused. If one denies, for philosophical reasons, that there is a set of people, a set of handouts, etc., then the assumption that there are such impure sets is false. But one then has to account for the reasoning involving them. Why would false assumptions lead to true conclusions? Or, to put it more simply, is (P) false?

If you can’t account for applicability of mathematics, you don’t have a foundational position that makes contact with science. To do this, you need to assume various comprehension principles for impure sets, relations and mixed functions (or, some cases, assume some system of mathematical objects, along with mixed primitive predicates relating them to the physical objects of interest, along with axioms for those).

Posted by: Jeffrey Ketland on March 14, 2020 12:47 PM | Permalink | Reply to this

Re: Type Theory and Propositions

After all, unless one has urelements, one doesn’t have applicable mathematics.

For the sake of this conversation eventually leading to some agreement, I was hoping you didn’t literally mean that. But then:

Applicable mathematics is about impure sets of physical things, and impure relations of physical things, and mixed functions from physical things to mathematical values.

What a ridiculous assertion. You should realize that there’s a difference between applicable mathematics, and a formal model of the application of mathematics. Only the latter actually needs a logic that distinguishes between “mathematical objects” and “real objects”. And this distinction is only for bookkeeping purposes: to formal logic, all objects are hypothetical, and are reasoned about using assumptions.

If you can’t account for applicability of mathematics, you don’t have a foundational position that makes contact with science. To do this, you need to assume various comprehension principles for impure sets, relations and mixed functions.

Logic is unable to account for the applicability of mathematics to the real world, because objects of a logical theory are not real objects, even if their role is to represent real objects. The applicability of mathematics is a perception about the real world.

What your “impure” gadgetry is doing is at best modeling the thoughts people have when applying mathematics.

So you are confused. I don’t know about Quine, Putnam, or anybody else. You might’ve just misunderstood them.

Posted by: Matt Oliveri on March 14, 2020 2:55 PM | Permalink | Reply to this

Re: Type Theory and Propositions

I’m basically quoting Quine, Putnam, Field, Burgess, et al.

In order to be able to apply any postulated abstract entities to the physical world, we need impure abstract entities, e.g. functions that map physical objects to pure abstract entities. Such impure abstract entities serve as a bridge between pure abstract entities and the physical objects; without the bridge, the pure objects would be idle. Consequently, if we regard functions as sets of a certain sort, then the mathematical theories we should be considering must include at least a minimal amount of set theory with urelements (a urelement being a non-set which can be the member of sets). (Field 1980: 9)

and Quine,

Another example of applied mathematics is the use of number in measurement. In terms of physical testing procedures we describe a Fahrenheit temperature function whose arguments are place-times and whose values are real numbers. Fahrenheit temperature is a class of pairs of pure real numbers and concrete place times. Similarly distance in metres is a class of triples, each comprising one pure real number and two concrete localities. Mathematical objects and concrete objects are thus in perpetual interplay, participating in the same triples and pairs. Mathematical vocabulary and empirical vocabulary are in perpetual interplay, participating in the same sentences. We see this already at the most primitive level of applied mathematics, when we say that there are fifty people in this room: the pure abstract number, fifty, is how many concrete people there are in this concrete room. I see pure mathematics as an integral part of our system of the world. (Reply to Parsons 1986)

Here’s Tim Bays discussing Potter’s 2004 book

From a purely technical perspective, three things make Potter’s treatment unusual. First, Potter allows urelements in his basic axiomatization. This is quite handy for philosophical purposes, as it lets us talk about sets of individuals—people, atoms, space-time points, etc.—without employing awkward set-theoretic surrogates. (Bays 2005)

Posted by: Jeffrey Ketland on March 14, 2020 4:07 PM | Permalink | Reply to this

Re: Type Theory and Propositions

Well I don’t really care which of them were confused. But I note that none of those quotes mentions “applicable”, which is quite different from “applied”. The Bays quote doesn’t mention “applied” or “apply” either. The Quine quote has:

Mathematical vocabulary and empirical vocabulary are in perpetual interplay, participating in the same sentences.

The use of the word “vocabulary” makes it sound like he might’ve deliberately been only modeling language pertaining to applying mathematics, which is what I originally thought you were getting at. Quine and Bays sound pretty sensible. Maybe Field was confused.

Posted by: Matt Oliveri on March 14, 2020 5:01 PM | Permalink | Reply to this

Re: Type Theory and Propositions

I think I’ve lost the thread of this argument. Of course one may speak of mappings between any kinds of types whether empirical or pure.

Here’s someone doing this for quantum gauge field theory.

Posted by: David Corfield on March 14, 2020 4:40 PM | Permalink | Reply to this

Re: Type Theory and Propositions

The good thing about philosophers is that whatever your view is, they can give it a name and refer to others who have espoused that view.

The bad thing about philosophers is that with so many different views having been espoused by so many famous people, they often have trouble with the idea that one of those points of view might be right and all the others wrong.

The only other thing I have to say is that it’s a pleasant change to be on the same side of an argument as Matt. (-:

Posted by: Mike Shulman on March 14, 2020 7:50 PM | Permalink | Reply to this

Re: Type Theory and Propositions

Well, obviously my view is correct! To be bit more serious though, for a view similar to yours (the usual name is “if-thenism”), try Mary Leng Mathematics and Reality (2010), and Penelope Maddy just has put a piece Enhanced If-Thenism online, which I don’t know is published. If you’re quarantined and bored, you can look at a draft “Foundations of Applied Mathematics I”, I put online at academia.edu a week or two ago, though it contains some typos and things I’m a bit unsure about. You might want to take a look at Andreka et al axiomatizations of special & general relativity too (eg “A Logic Road from Special Relativity to General Relativity” 2012, Synthese).

Posted by: Jeffrey Ketland on March 14, 2020 9:19 PM | Permalink | Reply to this

Re: Type Theory and Propositions

We could take one of the simplest cases to see the difference, the axiom of the empty set and the formation of the empty type.

In the set-theoretic case, either as an axiom or as a theorem we have

xy¬(yx). \exists x\, \forall y\, \neg (y \in x).

It certainly sounds as though we’re being told that a certain entity exists.

In the type-theoretic case, we have for the empty type:

Type formation

:Type\frac{ }{\emptyset\colon Type}

No terms to be introduced. Then as elimination rule

e:abort C(e):C\frac{ }{e\colon \emptyset \vdash abort_C(e)\colon C}

Then an η\eta-conversion rule, which says that for any term e:c:Ce\colon \emptyset\vdash c\colon C in a context including a term of type \emptyset, we have

abort C(e) ηc. abort_C(e) \;\leftrightarrow_\eta\; c.

Alternatively, we can form the empty type as a kind of inductive type. In Coq syntax:

Inductive empty : Type :=
.

As I was trying to suggest above, there might be an inferentialist reading of such type formation rules.

Posted by: David Corfield on March 11, 2020 10:18 AM | Permalink | Reply to this

Re: Type Theory and Propositions

Yes, but it seems to me that

(1) We can form the empty type \varnothing

(2) We can assert the existence of the empty set \varnothing

are just notationally different syntactic sugar on the same thing.

On the issue of inferentialism, one can certainly replace the induction axiom (scheme) by induction rules, and one can replace various reflection axioms by reflection rules, and truth axioms by truth rules. These possibilities sometimes have different outcomes. A well-known example is extending PAPA with truth introduction and elimination rules. This is a conservative extension of PAPA. However, if you extend it with truth introduction and elimination schemes, the result is inconsistent. A similar kind of situation can happen when one considers proof predicates. For example, adding to PAPA a rule “Given a proof of Prov PA(ϕ)Prov_{PA}('\phi'), conclude ϕ\phi” is conservative. But adding the scheme Prov PA(ϕ)ϕProv_{PA}('\phi') \to \phi is non-conservative.

Here’s a recent paper “Induction rules in bounded arithmetic” by Emil Jerabek on induction rules vs schemes.

Posted by: Jeffrey Ketland on March 14, 2020 4:46 PM | Permalink | Reply to this

Re: Type Theory and Propositions

TT is ontologically committed to FFs iff TT implies “there exists an xx such that F(x)F(x)”.

If by “theory” you mean “set of axioms in first-order logic”, then this makes sense. But it doesn’t seem adequate to me for talking about the ontological commitments of a foundational theory, where by “theory” we actually mean a deductive system such as “first-order logic” or “dependent type theory”: there is no Archimedean point from which to give meaning to statements that such a system “implies” anything.

Posted by: Mike Shulman on March 9, 2020 8:29 PM | Permalink | Reply to this

Re: Type Theory and Propositions

It makes sense for pure first-order logic over some fixed language: this implies x(x=x)\exists x (x=x) and no more. In other words, the ontological commitment of the set of theorems of first-order logic (with some fixed signature) is as small as possible. (One can even get rid of this, by restricting the substitution rules, and allowing empty models; but it’s a bit annoying & pointless to do this – see Quine 1954 “Quantification and the empty domain”) A foundational theory of some kind—set existence axioms, comprehension axioms, maybe type or higher-order comprehension—is then built up by adding further assumptions/axioms about various objects, including sets, types, second-order objects, properties, etc.

This is connected, as David mentioned above, to Field’s nominalist programme (Field 1980 “Science without numbers” ). In particular, his conservativeness result for applied set theory that I sketched above (excuse the typo that Matt noticed). Applied set theory with some non-mathematical signature (say ZA σZA_{\sigma} over some signature σ\sigma with predicates like “xx is an apple”, “spacetime point yy is between points xx and zz”, …) implies, by comprehension, the existence of sets of ur-elements (atoms), like the set of chairs, the set of applies, etc. But it doesn’t imply anything contingent about these chairs, applies, etc., how many there are, etc. Suppose ϕ\phi is a sentence purely about chairs, etc. (i.e., ϕ\phi does not contain \in). Then:

If ZA σϕ AZA_{\sigma} \vdash \phi^A, then ϕ\vdash \phi.

(where the A^A superscript on ϕ A\phi^A means we’ve relativized all the quantifiers in ϕ\phi to “xx is an atom/ur-element”)

So, the ontological commitments of applied set theory for the non-set-theoretical sector is mimimal (i.e, just x(x=x)\exists x \ (x=x)). As Field joked, if applied mathematics/set theory implied as a theorem that the Paris Commune was defeated, we’d find that a good reason to modify it. But in fact applied mathematics is consistent with any consistent non-mathematical theory one might combine it with.

For the case of the two apples that David mentioned, then clearly applied set theory does not imply “there are exactly two apples”. This is a contingent claim. We’d write that contingent sentence as

xy(xyApp(x)App(y)z(App(z)(z=xz=y))\exists x \exists y \ (x \neq y \wedge App(x) \wedge App(y) \wedge \forall z \ (App(z) \to (z = x \vee z = y))

abbreviated as 2xApp(x)\exists_2 x \ App(x) (one can generalize this recursively to define all quantifiers nx\exists_n x).

However, the equivalence between that sentence and “the number of applies = 2” is a theorem of applied set theory (as Putnam noted, back in 1967; Putnam says it’s a theorem of Principia, which is of course a type theory; but it’s also really a fragment of Z\mathsf{Z} set theory with urelements). If that is taken to be, say, ZA σZA_{\sigma}, where the non-mathematical signature σ={App}\sigma = \{App\}, then:

ZA σ 2xApp(x)|{xApp(x)}|=2\ZA_{\sigma} \vdash \exists_2 x \ App(x) \leftrightarrow |\{x \mid App(x)\}| = 2.

Posted by: Jeffrey Ketland on March 10, 2020 9:29 AM | Permalink | Reply to this

Re: Type Theory and Propositions

Right. (Except that the IMHO-correct formulation of first-order logic also makes sense for empty domains, so it doesn’t even imply x.(x=x)\exists x.(x=x).)

My point is that the foundational system of dependent type theory (including HoTT) is not built up from pure first-order logic by adding axioms. Instead, first-order logic is a derived structure within the deductive system of type theory. So to talk about the ontological committments of type-theory-based foundations one needs a different definition of “ontological committment”.

Posted by: Mike Shulman on March 11, 2020 1:20 AM | Permalink | Reply to this

Re: Type Theory and Propositions

More or less by definition, the range of a quantifier depends on its interpretation, because “range” and “interpretation” are semantic notions:

MxϕM \models \exists x \phi iff there is something adom(M)a \in dom(M) such that M a xϕM^x_a \models \phi

This doesn’t imply the interpretation of some language includes everything. It might, for all I know. I might not. One can’t settle complicated questions by erecting a Verboten sign and just banning things. There’s a lively debate about this topic. E.g., Absolute Generality and Everything, More or Less. The best thing to do is to read this literature.

One can relativize quantifiers if one likes, as might be needed for some result. (I gave an example above: if ZFA σϕ AZFA_{\sigma} \vdash \phi^A, then ϕ\vdash \phi, where ϕ A\phi^A has relativized quantifiers.) One can use many-sorted logic, if one likes. Second-order arithmetic is, in practice, a first-order two-sorted theory (e.g., Xn(nXϕ(n))\exists X \forall n(n \in X \leftrightarrow \phi(n))). But, for a certain class of subsystems, the secondary sort can be reduced to the first. For example, ACAACA is bi-interpretable with CTCT, and the set quantifiers in ACAACA are reinterpreted as number quantifiers, but with an additional truth predicate. Roughly, nXn \in X is translated as Tr(m X,n)Tr(m_X,n) (mm codes the predicate XX, which is true of nn).

But, out of curiosity, what should replace the verboten x(x=x)\forall x \ (x=x). Maybe (x:U)(x=x)(\forall x: U) \ (x=x)? How do I know what UU is? The sentence “Everything is identical to itself” really is an English sentence. So if its formalization is (x:U)(x=x)(\forall x: U) \ (x=x), where does this relativization come from? In semantic theory, it is its meta-theoretic truth condition, and that comes from the interpretation of the language.

Posted by: Jeffrey Ketland on March 11, 2020 1:32 PM | Permalink | Reply to this

Re: Type Theory and Propositions

I see I missed this question of how to convey “Everything is identical to itself”.

So, we’ll have for any universe, TypeType, any type A:TypeA:Type and any element a:Aa:A, an element in the identity type, refl a:Id A(a,a)refl_a: Id_A(a, a). These pairs (A,a)(A, a) are elements of the aforementioned Type^\widehat Type.

Which means we have

refl: (X,x):Type^Id X(x,x). refl: \prod_{(X, x): \widehat Type} Id_X(x,x).

One might render this judgement as claiming the truth of “Everything is identical to itself”.

Posted by: David Corfield on March 15, 2020 9:14 AM | Permalink | Reply to this

Re: Type Theory and Propositions

What about

refl: x:Type^Id Type^(x,x)refl\;:\;\prod_{x:\widehat Type} Id_{\widehat Type}(x,x)

?

Posted by: Matt Oliveri on March 15, 2020 6:52 PM | Permalink | Reply to this

Re: Type Theory and Propositions

Instead, first-order logic is a derived structure within the deductive system of type theory.

Yes, but it’s not the untyped first-order logic they imbibe in Logic for Philosophy 101.

Posted by: David Corfield on March 11, 2020 9:50 AM | Permalink | Reply to this

Re: Type Theory and Propositions

“Yes, but it’s not the untyped first-order logic they imbibe in Logic for Philosophy 101.”

Or, for that matter, the untyped first-order logic they imbibe in Mathematical Reasoning 101 in every mathematics department in the world. Untyped first-order logic is used by mathematicians and logicians throughout the world. E.g., this recent resolution of the disjunctive correctness question for CT CT^{-}. Or any standard textbook or research monograph on mathematical logic, proof theory, recursion theory, model theory, complexity theory, subsystems of analysis, etc. It’s taught to mathematicians, philosophers, computer scientists, linguists, etc., in much the same way that the notion of a Turing machine or a register machine is taught in computer science. One can then learn about advanced techniques like interpretability, definability, sequentiality, reflection, truth definitions, speed-up, many-sorted & higher-order logic, modal operators, Kripke models, types, admissible sets, infinitary logic, free logic, intuitionistic logic, minimal logic, substructural logic, Gentzen proof systems, resolution, computational complexity, SAT-solvers, etc. later.

You seem ultimately to want to say that, when one formalizes

(1) “There is a black hole at the centre of each galaxy”,

one should write

(2) (x:Galaxy)(y:Black hole)at-centre-of(y,x)(\forall x: \text{Galaxy}) (\exists y : \text{Black hole}) \ \text{at-centre-of}(y,x)

instead of

(3) x(Galaxy(x)y(Black hole(x)at-centre-of(y,x)))\forall x \ (\text{Galaxy}(x) \to \exists y \ (\text{Black hole}(x) \wedge \text{at-centre-of}(y,x)))

I consider (2) and (3) synonymous: they’re inter-translatable.

Posted by: Jeffrey Ketland on March 11, 2020 2:49 PM | Permalink | Reply to this

Re: Type Theory and Propositions

Untyped first-order logic is used by mathematicians and logicians throughout the world.

Well, it’s used by logicians and set theorists. Ordinary mathematicians may, if they happen to have recieved some logical training (which many haven’t), think “on Sundays” that they are using untyped first-order logic. But if you look at what they’re actually doing in practice, almost without exception it is much closer to typed first-order logic, and some of what they do is more natural to formalize in dependent type theory (e.g. proving a theorem that says “there exists an isomorphism” and then using the details of the construction of that isomorphism later on).

Posted by: Mike Shulman on March 11, 2020 5:35 PM | Permalink | Reply to this

Re: Type Theory and Propositions

I think I’d call it many-sorted first-order logic. I do think first-year maths student at pretty much any university (certainly at Oxford and Cambridge both of which I know) will get a standard course including an explanation that xϕ(x)\forall x \ \phi(x) means “for any xx, ϕ(x)\phi(x) holds.” and xϕ(x)\exists x \ \phi(x) means “there is some xx such that ϕ(x)\phi(x) holds”. I take your and David’s point entirely though—in practice, these are always restricted to a sort, type, etc.

Posted by: Jeffrey Ketland on March 11, 2020 6:42 PM | Permalink | Reply to this

Re: Type Theory and Propositions

(2) (x\forall x:Galaxy)(y:Blackhole\exists y:Black hole)at-centre-of(y,x)(y,x)

This is looking promising. Let’s turn it into a type:

x:Galaxy y:BlackHoleat-centre-of(y,x). \prod_{x: Galaxy} \sum_{y: Black \;Hole} \text{at-centre-of} (y,x).

This will have as elements functions that assign to a galaxy a black hole and evidence that it’s at the centre of that galaxy.

It seems that some galaxies, such as 4C+37.11, have two supermassive black holes at their centres, so I may decide to truncate the dependent sum if I really want the whole type to be a proposition.

Even if truncated, there are differences from (3) just by virtue of appearing in a dependent type theory, such as that its elements are functions.

Posted by: David Corfield on March 11, 2020 6:06 PM | Permalink | Reply to this

Re: Type Theory and Propositions

This will have as elements functions that assign to a galaxy a black hole and evidence that it’s at the centre of that galaxy.

So, let’s call this proposition, sentence, etc., α\alpha. The above strongly suggests:

(V) If α\alpha is true, there is evidence for α\alpha.

Is this built-in to your preferred type theory/version of MLTT? Can a sentence not be true, without any evidence for it?

Posted by: Jeffrey Ketland on March 11, 2020 7:42 PM | Permalink | Reply to this

Re: Type Theory and Propositions

I wouldn’t say that I had a preferred type theory. As you’ll know, there are many variants even of MLTT: extensional/intensional, univalence axiom, higher inductive types, LEM (excluded middle for propositions), etc. Then one can look to add in modalities.

I don’t feel inclined to follow Dummett and look to establish a single constructive system, although I’m interested to see how far a constructive/computational approach can be pushed. But understanding what the addition of LEM does for HoTT (as they do in e.g. 10.4 in the HoTT book) is a perfectly reasonable pursuit.

Without trying to pin down a single system of type theory, I’d encourage any interested philosophers to explore what it would mean to employ some or other variant of dependent type theory to represent our everyday reasoning, in particular the core dependency forms of dependent sum and product.

I think there’s a plausible Brandomian argument for logical pluralism, but the core of dependent type theory seems to me to help make explicit some basic aspects of our common inferential practice.

(I challenge anyone with a grasp of dependent type theory to read ‘Making it Explicit’ without shouting at it “Use type theory!”, Chap. 6 in particular on substitutability and anaphora.)

Something I’ve tried to do in my book (especially Chap. 2) is to think about the core dependent type theory in everyday settings. In the galaxy case above, one could imagine improving the story to bring in further dependency. It’s not that there’s some type of galaxies and a type of black holes and that then there happens to be a spatial matching. Naturally, we expect there to be a story of galaxy formation in which central supermassive black holes form. There’s a dependency of the formation of a black hole on aspects of the formation of its host galaxy. The astrophysicist’s model showing robustness under variation in initial conditions is pointing to something modal or lawlike, which the element (function) of that dependent product is gesturing towards.

Perhaps the suggestions I make about event structure in Chap. 2 are worth pursuing here, along with the modal thoughts of Chap. 4.

Posted by: David Corfield on March 12, 2020 10:09 AM | Permalink | Reply to this

Re: Type Theory and Propositions

Perhaps the suggestions I make about event structure in Chap. 2 are worth pursuing here, along with the modal thoughts of Chap. 4.

You may have described them before, but if so, I missed them (but I do sort of recall something about modality from a couple of years back, but I forgot).

What’s your take on event structure and what on modality? There’s a large literature on events, including what events are (whether they are spatio-temporal particulars (Russell, Quine, Davidson), whether they are property-like (Kim, Lewis), or whether they are fact-like) and how how natural language sentences about events are regimented (the classic paper on this topic is Davidson 1967).

Posted by: Jeffrey Ketland on March 12, 2020 7:59 PM | Permalink | Reply to this

Re: Type Theory and Propositions

I’ll say something about these things as I put up new posts on material from my book. Those with access to it (supposedly Oxford Online Scholarship will make it available shortly) can take a look at section 2.6 and Chap. 4.

For the latter, an earlier version is available at PhilSci Archive. The book version has quite a few changes made, but not any substantial ones.

Posted by: David Corfield on March 13, 2020 9:55 AM | Permalink | Reply to this

Re: Type Theory and Propositions

It’s interesting that you bring up free logic. I’ve gotten somewhat interested in free logic somewhat recently, since its use in Feferman’s Explicit Mathematics makes clear that it’s related to the computation/value distinction in computational type theory. The outer domain corresponds to computations, and the inner domain to values. But I think being “defined” should really mean being well-typed, for some useful type, and not just having a computational normal form, which is generally something bizarre and foreign to mathematics. So there should really be many inner domains, since, for example, “prime” is a well-defined predicate on numbers, but not a well-defined predicate on rabbits. Reasoning about definedness is (should be) reasoning about well-typedness of computations! (Terms can be understood as degenerate computations.) I have some sketchy plans of interpreting computational type theory as a free-logic-like conservative extension of ordinary (mathematical values only) type theory.

But another use case of free logic is to make description and choice operators better behaved by making them undefined in case their presupposition is false. I brought this up in another current thread, and I even considered mentioning free logic. IMPS’ logic sure seems to be a free logic. There’s a SEP article for free logic.

Posted by: Matt Oliveri on March 10, 2020 11:10 PM | Permalink | Reply to this

Re: Type Theory and Propositions

Well, over 80 comments – some light, some heat generated. Thanks to the contributors. I wonder what onlookers made of it.

Some lessons for me:

  1. There are two kinds of people – those who believe ‘Venus = 3’ (without any trappings, taggings or such like) makes sense as a proposition, and those who don’t.

  2. I’ve grown to like Type^\widehat Type quite a bit more, useful as it is for pooling elements while maintaining type-discipline.

  3. It would be good to lay out side by side, type-theoretic and first-order/set-theoretic version of some pieces of applied mathematics, including logical reasoning, arithmetic, geometry, and so on, right up to QFT.

  4. Persuading analytic philosophers to give up untyped first-order logic for dependent type theory is not going to be easy.

Posted by: David Corfield on March 15, 2020 3:35 PM | Permalink | Reply to this

Re: Type Theory and Propositions

I suspect, after some of this “heat”, that this weird idea that one can form sets whose elements actually are things like Venus is a big part of what keeps people attached to untyped FOL, since it’s difficult to defend a view that in the “real world” every object has a unique type. Do we have Venus:PlanetVenus : Planet or Venus:SolarSystemObjectVenus : SolarSystemObject? Once you realize that any mathematical system is just a model that captures some aspects of reality and omits others, it makes more sense to think of type discipline as a mathematical way to represent the order imposed on the universe by human minds, since depending on the particular application we could choose to impose that order in different ways, with no one model privileged over another.

I wonder whether the “extrinsically typed” systems that Matt likes might be an easier sell, since they have the benefit of dependent types and yet allow for the idea of “collecting pre-existing things” into a type.

Posted by: Mike Shulman on March 15, 2020 5:57 PM | Permalink | Reply to this

Re: Type Theory and Propositions

… weird idea that one can form sets whose elements actually are things like Venus is a big part of what keeps people attached to untyped FOL, since it’s difficult to defend a view that in the “real world” every object has a unique type.

There are two main things here. The first bit, I’d insist, isn’t weird at all. It’s simply applied mathematics, and concerns how we explain collecting things, discussing relations and functions between them, Venn Diagrams, etc. One might want to discuss the binary relation {(a,b)older(a,b)}\{(a,b) \mid older(a,b)\} on humans, and say its not a linear order (some a,ba,b are as old as each other). We can say the set of cars outside, with its parking-order, is isomorphic to a linear order. We can say the set of bridges, set of land-areas, and connection relation at Konigsberg is a multigraph (since each vertex has odd degree, it has no Euler cycle). We say there is a square-integrable function Ψ\Psi, assigning a complex number Ψ(x,t)\Psi(\mathbf{x},t) to each spacetime point with co-ordinates (x,t)(\mathbf{x},t), and for the system we are interested in (a particle of mass mm under a central potential V(r)V(r)), this satisfies the equation

22m 2Ψ+V(r)Ψ=EΨ-\frac{\hbar^2}{2m} \nabla^2 \Psi + V(r) \Psi = E \Psi

When we work out its solutions, we obtain a discrete eigenspectrum (E n1n 2E_n \propto \frac{1}{n^2}) – which, converting energies to wavelengths, is precisely the measured spectroscopic data for hydrogen.

I don’t see any difficulty in discussing, e.g., {Venus}\{Venus\}, or {3}\{3\}, or {Venus,3}\{Venus,3\}. Or in saying |{Venus,3}|=2|\{Venus, 3\}| = 2. This is a trivial theorem of set theory with atoms/urelements ZAZA (over a signature containing “Venus”, etc.): since At(Venus)At(Venus) is an axiom, and ¬At(3)\neg At(3) is a theorem of ZAZA.

The second part (about “types” of “real-world things”) is, so far as I can see, partly a linguistic issue, although “concrete” and “abstract” can be used as a 2-sorted basis for analysis of the examples mentioned above. This is how Burgess does things, and is how I do things too in some papers. There’s a gigantic literature on natural kinds, causal laws, various puzzles, Goodman’s “grue” puzzle, the Newman Objection, etc.

I’ll explain the last mentioned, as I believe I’m the first person to work out the details (“Empirical adequacy and ramsification”: if you read the details, you’ll see it uses second-order two-sorted logic). Russell, in Analysis of Matter (1927), suggested that “our knowledge of reality” consisted in acquaintance with a mathematical structure MM and the claim that “MM is isomorphic to the world WW”. Max Newman pointed out (in a review in 1928 in Mind of Russell’s book) that this is a nearly trivial claim so long as the world has enough objects. I.e., “MM is isomorphic to the world WW” is equivalent to “the world contains |M||M| objects”. A closely related problem afflicts Ramsey sentences, as explained by Demopoulos & Friedman in 1985. This is now what is called “Newman’s objection”. If a scientific theory TT’s underlying predicates are classified as theoretical and observational, the result of quantifying out the theoretical ones with (second-order) existential quantifiers, leaving the observational ones alone, is called the theory’s Ramsey sentence:

R 1R nT(R 1,,R n)\exists R_1 \dots \exists R_n \ T(R_1, \dots, R_n).

But, one can show that, so long as there are enough objects out there, a Ramsey sentence for a theory TT is equivalent to TT’s empirical adequacy. In this reasoning, one considers sets and relations of unobservable “real-world” objects.

One standard response to this is to suggest the second-order existential quantifiers range only over natural properties/relations. But no one knows how to make this work. I.e., it requires there be a type, NatRel\mathbf{NatRel} and the typed Ramsey sentence is then:

(R 1:NatRel)(R n:NatRel)T(R 1,,R n)(\exists R_1: \mathbf{NatRel}) \dots (\exists R_n : \mathbf{NatRel}) \ T(R_1, \dots, R_n).

But what is NatRel\mathbf{NatRel}?

Posted by: Jeffrey Ketland on March 15, 2020 11:48 PM | Permalink | Reply to this

Re: Type Theory and Propositions

The only response I have is to repeat what I already said and Matt repeated. (In case this is what’s confusing you, it’s true that when we use mathematical objects to represent real-world ones we often borrow the name of the real-world object for the mathematical one. But the fact that we call a four-manifold “spacetime” does not mean that its points actually are points in the real world, etc.) No matter whether or not it seems weird to you, it’s inconsistent with the way applied mathematics is actually done, and (as we’ve seen) leads to all kinds of strange philosophical problems.

Posted by: Mike Shulman on March 17, 2020 2:28 PM | Permalink | Reply to this

Re: Type Theory and Propositions

Looking back, I don’t think I was very clear when I wrote:

Logic is unable to account for the applicability of mathematics to the real world, because objects of a logical theory are not real objects, even if their role is to represent real objects.

There is the (hopefully) obvious sense that logical objects can’t be real, just like a character in a story isn’t a person. (E.g. you can’t start a conversation with them.) But a story can still be nonfiction, and so its characters are intended to be real people. And you can also have historical fiction with real and fake people as characters.

The intended interpretation of a logical object can be a real object. I maintain that this ultimately boils down to conventions, bookkeeping, and informal interpretation, but I’m open to the intended interpretation of a set theory having sets with real objects for elements. I find this perfectly natural and intuitive, but I’m not so sure it’s useful for rigorous reasoning.

Logic is language, and of course we’d be in trouble if we couldn’t talk about real things. I’m not sure though whether it helps to formally reason about objects representing real things.

It might at least avoid potential confusion when combining different theories intending to model the same aspects of reality. But you might already run into trouble figuring out “same aspects of reality”. But if not, then you give a “neutral” model of those aspects with no predictive power on its own, and so it’s vacuously an accurate model. Then you mathematically relate the useful models to the neutral one, somehow. Very sketchy, I know.

Posted by: Matt Oliveri on March 17, 2020 5:39 PM | Permalink | Reply to this

Re: Type Theory and Propositions

I see what you mean. I raise briefly the extrinsic/intrinsic issue in the book, but there’s much more to say. An absurdly strict form would have me ban forming the identity between ‘this man’ and ‘that person’.

If we want to keep with an intrinsic story, I think we’d need to head down the route of considering our comprehension of portions of experience. I’ve brought a couple of Husserl tomes home with me. Perhaps the imminent lockdown will be the occasion to read them.

There’s also something to be said about perception through invariance, so type-theoretically working in the context of a looped group. I touch on this in Chaps. 3 and 4, but there’s much more to say. We see invariant colour, shape, and size of entities through continuous variation.

Plenty to think about.

Posted by: David Corfield on March 15, 2020 8:48 PM | Permalink | Reply to this

Re: Type Theory and Propositions

Dependent type theory and categorical would be more useful than untyped first order logic for philosophy that follows structuralism. Unfortunately most analytic philosophers seem to be materialists rather than structuralists.

Posted by: Madeleine Birchfield on March 17, 2020 7:14 PM | Permalink | Reply to this

Re: Type Theory and Propositions

There is a position called structural realism, which particularly concerns theories in physics. Some interest in type theory/category theory is shown there.

Even in ‘fruit on my desk’ situations, one can think structurally.

To the extent that I am justified in taking the apples on my desk as a set (i.e., a type which is a set), and likewise the oranges there, then I can combine them to form a type which will also be a set. Cardinalities add. I can reason about distributing fruit to a group of children. And so on.

Treating apples as a set, I am committing to it being a yes-no question of whether any two specified apples are the same. I’m also relying here on a time-independence (or else I should be working with time-dependent types).

The reasonableness of the set supposition is based on the boundary stability, non-interpenetration, non-spontaneous (dis)appearance, etc. of entities like pieces of fruit, where I shouldn’t suppose these for raindrops on my window.

We now know that there is deep physics behind these properties, including the stability of matter.

Posted by: David Corfield on March 18, 2020 11:06 AM | Permalink | Reply to this

Re: Type Theory and Propositions

The reasonableness of the set supposition is based on the boundary stability, non-interpenetration, non-spontaneous (dis)appearance, etc. of entities like pieces of fruit, where I shouldn’t suppose these for raindrops on my window.

This contradicts the conservativeness theorem given by Field, for which I sketched a model-theoretic proof above; which shows that, if one assumes, for each ur-element primitive predicate, there is a corresponding set (by separation), then these “suppositions” imply nothing contingent and certainly nothing about “boundary stability, non-interpenetration, non-spontaneous (dis)appearance, etc”. In fact, the same result can be obtained for type theory. The mere assumption of types Aardvark, Raindrop, Galaxy, etc., will generate no theorems whatsoever of a contingent nature.

Again I’ll go through the details. Let ZA σZA_{\sigma} be formalized set theory with atoms, over the relevant signature σ\sigma (maybe it has “xx is a cup”, “xx is a raindrop”, “point pp lies between points qq and rr”, etc.). Then ZA σZA_{\sigma} implies there is a set of raindrops, a set of pieces of fruit, etc. But ZA σZA_{\sigma} does not imply ϕ\phi unless ϕ\phi is a logical truth (where ϕ\phi is a sentence in the language containing just these predicates; strictly, one should relativize to atoms, but I’ll gloss over that).

Clearly, sentences about “stability”, “disappearance” etc., are not logical truths. Hence, they are not implied by ZA σZA_{\sigma} (or type theory, for that matter).

This, incidentally, is the whole point of Field’s programme. To show that the assumption of abstract entities like sets, relations and functions does not imply anything at the non-mathematical level (unless such a sentence is a logical truth). So, the claim above is contradicted by an established mathematical result.

If one doesn’t wish to use the predicate “xx is a piece of fruit”, then replace it with “xx is a piece of fruit at time tt”. Exactly identical considerations will apply with type theory.

Posted by: Jeffrey Ketland on March 19, 2020 3:32 PM | Permalink | Reply to this

Re: Type Theory and Propositions

Two thoughts:

  1. It matters what set theory you use. For example, it has to be consistent to be conservative. But there are probably other restrictions on which set theories work. Likewise for type theory.

  2. It sounds like Field’s result is conservativity relative to a theory of untyped FOL=. It may already presume too much that untyped equality applies to real objects. I think that’s what David was getting at.

Posted by: Matt Oliveri on March 19, 2020 4:30 PM | Permalink | Reply to this

Re: Type Theory and Propositions

Conservativeness is pretty robust with respect to variations here: it will apply to the many-sorted case; it will apply if the comprehension is type-theoretic. (But yes, one needs consistency to prove the result.) In fact, this should be congenial to a formalist, or a nominalist, or a fictionalist, etc.

As Wittgenstein put it,

Indeed in real life a mathematical proposition is never what we want. Rather, we make use of mathematical propositions only in inferences from propositions that do not belong to mathematics to others that likewise do not belong to mathematics. (In philosophy the question, “What do we actually use this word or this proposition for?” repeatedly leads to valuable insights.) (Tractatus, Sc 6.211)

The logical empiricist Carl Hempel makes a similar point:

Thus, in the establishment of empirical knowledge, mathematics (as well as logic) has the role of a theoretical juice extractor: the techniques of mathematical and logical theory can produce no more juice of factual information than is contained in the assumptions to which they are applied; but they may produce a great deal more juice of this kind than might have been anticipate upon a first intuitive inspection of those assumptions which form the raw material for the extractor. (“On the Nature of Mathematical Truth”: 391)

(However, I’m not a formalist, etc. I am a Platonist, as one can probably tell….)

What is happening is that the higher-level stuff pertaining to sets or types is sort of “disentangled” from the lowest-level stuff.

As Burgess, Moschovakis and Kripke responded to Field before his book was published, one can obtain non-conservativeness, if one lets the theories interact more closely. Suppose I treat PAPA as a theory of urelements. Then “adding” standard axiomatic set theory actually is conservative. That would sound odd to most mathematical logicians, because, in set theory, you can clearly prove Con(PA)Con(PA), and Con(PA)Con(PA) is not a theorem of PAPA. So what is happening?

There are two different versions of Con(PA)Con(PA) here. One, Con (PA)Con_{\in}(PA), is in the set-theory language

There is no set which is a sequence of sets encoding a syntactical derivation of 0=1 in PA

and the other, Con A(PA)Con_{A}(PA), is in arithmetical language

There is no number encoding a sequence of numbers encoding a syntactical derivation of 0=1 in PA.

The incompleteness theorem says that Con A(PA)Con_{A}(PA) cannot be proved in PAPA.

And here, the required biconditional (that would link the two),

Con (PA)Con A(PA)Con_{\in}(PA) \leftrightarrow Con_{A}(PA)

can’t be proved unless one extends the induction scheme of PAPA to allow all formulas in the extended language (i.e., those containing \in). Then set theory + PAPA + extended induction proves Con A(PA)Con_A(PA); and is therefore non-conservative over PAPA.

Field’s setup in his book (his basic theory NN to which he adds set theory) is geometric. Burgess, Moschovakis and Kripke responded to Field’s point about conservativeness by noting that since the geometric system NN interprets arithmetic, the combined theory (i.e., with set theory) will prove an encoded version of Con(N)Con(N) in the geometric language itself—so long as axiom schemes inside NN are extended. Some of the details are spelt out in Shapiro’s “Conservativeness and Incompleteness”, 1983).

But I’ve modified the example so as to focus on arithmetic, rather than geometry. Analogous results hold for axiomatic truth theories.

Posted by: Jeffrey Ketland on March 19, 2020 7:45 PM | Permalink | Reply to this

Re: Type Theory and Propositions

We’re evidently engaged in very different projects, as Mike and Matt realised long before, ours being one that concerns our ability to reason about what we perceive about the world so as to predict and act.

I’m not contradicting Field’s conservativeness results, as I’m not working with the assumptions of Field’s project.

Odd to cite Wittgenstein who came to see that the Tractatus picture of the world as a line of a truth table, countless atomic sentences being either true or false, was wholly misguided. In the final parenthetic comment, he’s pointing us off in the inferentialist direction that he goes on to develop. I take this to be a more promising direction.

Let’s face it, the later Wittgenstein would have been appalled by almost all of the philosophy of mathematics of the past 60 years.

Posted by: David Corfield on March 20, 2020 11:47 AM | Permalink | Reply to this

Re: Type Theory and Propositions

I’ll just repeat the relevant mathematical point here. (None of this is connected to anything about type theory or set theory per se. Obviously, philosophers use type theory, higher-order logic, many-sorted logic, etc., all the time. Articles about semantics and linguistics routinely invoke lambda-abstraction. This is all standard, widely used stuff. The only real controversy is about constructivism. That is the sticking point. It has nothing to do with FOL. That is a windmill being tilted at. An imaginary, non-existent opponent introduced for propaganda reasons.)

The philosophical claim above, about set theory entailing contingent claims about “boundary stability, non-interpenetration, non-spontaneous (dis)appearance, etc”, contradicts the conservativeness of set theory (type theory, etc.). To see this, let 𝕄𝕒𝕥𝕙𝕤\mathbb{Maths} be some formal system of applied mathematics containing various comprehension axioms (set-existence axioms; higher-order or type-theoretic comprehension: it doesn’t matter). Let EE be the formal regimentation of, say, “raindrops interpenetrate and are temporally unstable”. Then 𝕄𝕒𝕥𝕙𝕤E\mathbb{Maths} \nvdash E. The proof is this: EE is not logically true: there’s a model M¬EM \models \neg E. So, there’s a model M +𝕄𝕒𝕥𝕙𝕤+¬EM^{+} \models \mathbb{Maths} + \neg E. By soundness, 𝕄𝕒𝕥𝕙𝕤E\mathbb{Maths} \nvdash E. (I’m simplifying a bit by omitting relativization to individuals, urelements, etc.)

If one’s favourite 𝕄𝕒𝕥𝕙𝕤\mathbb{Maths} is set-theoretic, the model M +M^{+} is a kind of von Neumann universe over MM. If your favourite 𝕄𝕒𝕥𝕙𝕤\mathbb{Maths} is simple theory of types, just take a standard model with all finite types, with the elements of MM as individuals. If 𝕄𝕒𝕥𝕙𝕤\mathbb{Maths} is just (unary) second-order comprehension, then M +=(M,S)M^{+} = (M,S), where SS is the set of all subsets of dom(M)dom(M). (If your favourite 𝕄𝕒𝕥𝕙𝕤\mathbb{Maths} is constructive, then it’s more complicated, and would involve Kripke models or a proof-theoretic reduction. That said, I’m pretty sure it works.)

Posted by: Jeffrey Ketland on March 20, 2020 5:06 PM | Permalink | Reply to this

Re: Type Theory and Propositions

The only real controversy is about constructivism. That is the sticking point.

If by “constructivism” you mean proof relevance (that proofs are mathematical objects), then HoTT is necessarily constructive. Otherwise, it’s not.

It has nothing to do with FOL. That is a windmill being tilted at. An imaginary, non-existent opponent introduced for propaganda reasons.

I’m sorry if it seems that way to you. If it’s because of what I said, the real issue I was talking about is not first-order specifically, but the idea that equality is a predicate. In HoTT, it generally isn’t.

You considered predicates like “xx is a cup” and “xx is a raindrop”, so I thought your point might rest on the assumption that the theory, to which Field’s result is applied, would be in an untyped predicate logic. While you can indeed get similar conservativity results to Field’s for all sorts of languages, you keep using examples from untyped predicate logic, without any argument that that’s the right choice. Field-like results do not address this choice. You seem to be trying to apply Field’s result to informal reasons against using such and such a theory. You only get to apply Field once you’ve picked a theory.

For example:

The philosophical claim above, about set theory entailing contingent claims about “boundary stability, non-interpenetration, non-spontaneous (dis)appearance, etc”, contradicts the conservativeness of set theory (type theory, etc.).

David did not claim that set theory entails anything. He said:

The reasonableness of the set supposition is based on the boundary stability, non-interpenetration, non-spontaneous (dis)appearance, etc. of entities like pieces of fruit, where I shouldn’t suppose these for raindrops on my window. [emphasis added]

By “set supposition”, I’m guessing he meant that equality is a predicate. This is not something that you can “unsuppose” in predicate logic. Since then, the discussion should’ve been about choice of language, not entailment within some language. (Unfortunate it is that categorical logicians decided to redefine “set”. And then HoTTists redefined it again.)

Posted by: Matt Oliveri on March 20, 2020 9:33 PM | Permalink | Reply to this

Re: Type Theory and Propositions

The philosophical claim above, about set theory entailing contingent claims about “boundary stability, non-interpenetration, non-spontaneous (dis)appearance, etc”, contradicts the conservativeness of set theory (type theory, etc.).

Are you claiming I made such a claim? Where? Surely you recognise the difference between entailment and presupposition.

I was saying that the proper application of mathematics presupposes certain things.

If you tell me that you believe there to be 4 particles confined in some vacuum, since 2 were already there and 2 more have been added, I have good reason to doubt you - what if you added positrons to electrons, and so on.

You are only entitled to take some sort of thing to be a set if you are previously entitled to certain presuppositions holding. Type theory is very good at making explicit such presuppositions.

Posted by: David Corfield on March 21, 2020 10:24 AM | Permalink | Reply to this

Re: Type Theory and Propositions

Maybe we should forget about raindrops for a while and talk about higher-dimensional mathematical objects, which are definitely not objects of any theory of FOL=. This is because equality of higher-dimensional objects is, by definition, a binary type family that is not a binary predicate. (That is, higher-dimensional objects are elements of HoTT types that are not h-sets.)

One could complain (as I have) that this is not a real notion of equality. But I’ve tentatively changed my mind. By what rules does it not count? I do not know of any philosophical argument against it. (Of course, I’m no philosopher.) It is both highly unintuitive and technically nightmarish. But so what? The people around here really like it, and it sure seems an awful lot like equality.

So once you admit mathematical objects that do not arise in FOL= theories, and if you’re interested in mathematically modeling reality, it seems unwise to assume that real objects will always be described usefully by FOL=.

Posted by: Matt Oliveri on March 20, 2020 1:36 AM | Permalink | Reply to this

Re: Type Theory and Propositions

But I’ve tentatively changed my mind.

Welcome to the light! I’m sure that if you stick with it, you’ll be able to train your intuition to find it as intuitive as the rest of us around here do, and come to see that HoTT turns the nightmare into a vision. (-:

Posted by: Mike Shulman on March 20, 2020 4:44 PM | Permalink | Reply to this

Re: Type Theory and Propositions

Thanks, I guess. I changed my mind a year or two ago, noticing that if presentation independence of HoTT works out, it seems analogous to independence of set theory from the details of the axiom set. Set theory relies on a formal axiomatization, and this doesn’t detract from an intuitive understanding of the objects. Hopefully the dependence of HoTT on a set theoretic presentation doesn’t detract from the natively higher-dimensional understanding.

HoTT definitely has at least one vision behind it. But I think it will remain a nightmare in my estimate until coherence issues are understood much better. It’s a fascinating nightmare. I think I’ll stick around.

Posted by: Matt Oliveri on March 20, 2020 9:46 PM | Permalink | Reply to this

Re: Type Theory and Propositions

What do you mean by “dependence of HoTT on a set theoretic presentation”?

Posted by: Mike Shulman on March 21, 2020 5:14 AM | Permalink | Reply to this

Re: Type Theory and Propositions

Huh?? Like judgmental equality, the rest of the judgment level, and all the pretype machinery, if applicable.

Posted by: Matt Oliveri on March 21, 2020 3:30 PM | Permalink | Reply to this

Re: Type Theory and Propositions

I don’t know what “pretype machinery” is, and I don’t know what is “set-theoretic” about the judgment level of HoTT.

Posted by: Mike Shulman on March 22, 2020 5:58 AM | Permalink | Reply to this

Re: Type Theory and Propositions

I too am puzzled by your description of HoTT, Matt. I don’t know much about (homotopy) type theory, but I thought one of the fundamental points was that it doesn’t depend on anything set-theoretic.

Posted by: Tom Leinster on March 22, 2020 2:42 PM | Permalink | Reply to this

Re: Type Theory and Propositions

Mike:

I don’t know what “pretype machinery” is,

I mean the language features that involve non-fibrant types, for those languages that have them. (So, not Book HoTT.)

and I don’t know what is “set-theoretic” about the judgment level of HoTT.

The proofs (derivations) are not mathematically relevant. So they’re like proofs in set theory.

Tom:

I don’t know much about (homotopy) type theory, but I thought one of the fundamental points was that it doesn’t depend on anything set-theoretic.

Here by set-theoretic, I mean that proofs are irrelevant, not that there’s some entirely separate theory of sets.

Posted by: Matt Oliveri on March 22, 2020 9:42 PM | Permalink | Reply to this

Re: Type Theory and Propositions

Here by set-theoretic, I mean that proofs are irrelevant

In that case, this conversation has gone into territory where I’m completely without map or compass. I’d naively understood “set-theoretic” to mean “concerning the theory of sets” :-) And I’ve never heard a set theorist say that “proofs are irrelevant”!

Posted by: Tom Leinster on March 23, 2020 4:08 PM | Permalink | Reply to this

Re: Type Theory and Propositions

OK, yeah sorry. I guess my description was too sloppy without some background. The formal proof that two expressions denoting elements of a set are equal is not itself considered to denote a nontrivial mathematical object. This is related to the definition of h-set in HoTT, which is a type SS such that there’s at most one element of the equality type between any two elements of SS.

In material set theory, proofs of membership in a set also do not denote nontrivial objects.

Now consider HoTT in general. Equality “proofs” or “witnesses” are elements of equality types. They generally are nontrivial objects. This is not set theoretic. But a formal system for HoTT will also have judgmental equality (or some other strict equality), which is applicable to all terms, and its notion of proof is formal derivations, which don’t denote anything. So the judgment level, with its equality judgment, is an alternative view of everything formalized, which is thoroughly set theoretic.

(Years ago, I contended that this meant HoTT was essentially taking place within set theory. But it’s only the presentation that’s set theoretic.)

Posted by: Matt Oliveri on March 23, 2020 7:12 PM | Permalink | Reply to this

Re: Type Theory and Propositions

You do realize that HoTT includes a subuniverse of h-sets and h-props in which proofs are irrelevant like in set theory? So the fact that the metatheory involves h-sets says nothing about the “dependence” of HoTT on anything non-HoTT.

Posted by: Mike Shulman on March 24, 2020 12:46 AM | Permalink | Reply to this

Re: Type Theory and Propositions

Indeed. HoTT’s dependence on set theory is not a dependence on something non-HoTT, just like set theory’s dependence on syntax is not a dependence on something non-set-theoretic. But that’s irrelevant. The metatheory of HoTT doesn’t depend in any special way on <random mathematical object definable in HoTT>, so why shoud it depend in a special way on sets? Because it depends on a presentation, technically. But why is that OK? Not “Why is that a good idea?”; it doesn’t make sense to ask whether it’s a good idea, because it seems inevitable.

If the metatheory of HoTT inevitably involves a presentation, which has a set theoretic notion of equality, why isn’t that equality, end of story? That is, why isn’t judgmental equality the real equality? I know the reason why HoTTists don’t want that to be equality, but equality is a fundamental thing, so I figure you can’t just change your mind about what it is. The traditional idea is that equality should be respected by everything in sight. The judgments are in sight, and they do not respect the equality type; they respect judgmental equality, the presentation equality. To me, there needed to be a reason why you can say that doesn’t count. Just like there’s a good reason why syntactic equality isn’t what counts in set theory (or HoTT).

Posted by: Matt Oliveri on March 24, 2020 2:56 AM | Permalink | Reply to this

Re: Type Theory and Propositions

I don’t understand your question. What do you mean by “OK”? Why wouldn’t it be OK? Nobody changed their mind; we never wanted judgmental equality to be the real equality. Judgments are not in sight within the theory, and metatheoretic constructs (like syntax) do not generally respect object-language equality.

Posted by: Mike Shulman on March 24, 2020 9:59 AM | Permalink | Reply to this

Re: Type Theory and Propositions

I don’t understand your question. What do you mean by “OK”?

It was a rhetorical question. I already said I think it’s OK as long as HoTT is presentation independent.

But basically, “OK” in this case meant that the equality/identity type is the right notion of equality, despite the presence of a stricter presentation equality.

Why wouldn’t it be OK? Nobody changed their mind; we never wanted judgmental equality to be the real equality.

First of all, if it isn’t OK, then nobody having changed their mind just means they were wrong all along. :) So I don’t know why you made that point.

Second, category theorists seem to have a habit of changing the meaning of words. So even if the equality type is not equality, I figure most HoTTists do not care.

It is ostensibly not “OK” because the nature of presentation equality does affect users of HoTT, and it’s not just a matter of syntactic formulation; the presentation equality is in the semantics. At least when using the traditional notion of semantics. And that’s the key to why it might be OK: there’s an additional layer: a higher-dimensional semantics distinct from the presentation’s semantics.

Judgments are not in sight within the theory,

I suspect you cannot currently defend this claim rigorously. What notion of theory are you using, which excludes the judgments, and how do you interpret such theories?

I think defending this claim would be substantially the same as demonstrating presentation independence. And of course I think that would be a great thing to do.

and metatheoretic constructs (like syntax) do not generally respect object-language equality.

Right. But it’s not currently obvious that judgments are only metatheoretic. In fact, in a sense, they are not only metatheoretic: they are a fundamental part of the theory which includes the presentation. And it seems that that is the only kind of theory we can actually interpret. Same issue yet again: the presentation has both syntax and semantics, and you’d like to ignore both, when identifying mathematical objects.

Posted by: Matt Oliveri on March 24, 2020 7:42 PM | Permalink | Reply to this

Re: Type Theory and Propositions

I don’t have access to Field’s book, but insofar as his result is a mathematical one, the ur-elements appearing therein must already form a set (or type, or whatever the relevant notion of “collection” is in the metatheory). Thus, it cannot contradict any observations about the failure of mathematics to apply to reality.

Posted by: Mike Shulman on March 20, 2020 4:52 PM | Permalink | Reply to this

Re: Type Theory and Propositions

Yes, but I think that doesn’t quite touch the point at issue. Suppose we have at our disposal some basic urelement predicates “xx is a raindrop”, “ll is the wordline of xx”, “timeinstantt 2time instant t_2 is later than t 1t_1”, “ll intersects tt”; call this system of predicates σ\sigma; and in addition, we have the predicates “xx is an atom” and “xyx \in y” to formulate applied mathematics.

Let EE be the sentence:

x(raindrop(x)(wordline(,x)t 1t 2(t 1t 2later(t 2,t 1)int(,t 1)¬int(,t 1)))\forall x \ (raindrop(x) \to \exists \ell \ (wordline(\ell,x) \wedge \exists t_1 \exists t_2 \ (t_1 \neq t_2 \wedge later(t_2,t_1) \wedge int(\ell, t_1) \wedge \neg int(\ell, t_1) ))

This expresses

“each raindrop has a worldline (\ell) such that for two distinct time instants, the wordline intersects the first but not the second”.

Suppose E AE^A is the result of relativizing EE’s quantifiers to “xx is an atom”.

Then: ZFA σE AZFA_{\sigma} \nvdash E^A.

If someone then says that presupposition of sets, etc, is based on assumptions about stability, etc., this isn’t so. Those presuppositions (i.e., comprehension/separation axioms inside ZFA σZFA_{\sigma}) imply no sentences which are not logical truths.

Posted by: Jeffrey Ketland on March 20, 2020 6:03 PM | Permalink | Reply to this

Re: Type Theory and Propositions

The presupposition in question is that your urelements form a set. By saying that the raindrops are (represented by) particular urelements, you’re committing to having a set of raindrops, and therefore having some notion of “raindrop” that is well-defined independent of time and can be distinguished from each other. This has nothing to do with any notions of “worldline” or “time” that you additionally put into the object language. It’s that in order to even formulate mathematically precise statements about “a raindrop”, including the one you can’t prove about worldlines, you need to decide exactly what you mean by “a raindrop”.

Posted by: Mike Shulman on March 21, 2020 5:16 AM | Permalink | Reply to this

Re: Type Theory and Propositions

raindrop (n): a single drop of rain.

When one observes rain, one notices that, instead of a gigantic vertical waterfall, the water falls in drops. This because, when water vapour in the air condenses, it forms droplets—a cloud. When it rains, these drops fall: raindrops. One can observe all this by looking at a pavement or a window, when it’s raining. If one has a sheet of paper and it’s raining, one can place it outside for a few seconds and count the hits, as each raindrop makes a little wet splodge. If one did this experiment over 10 seconds, say, and got, say, 27 hits, I am happy to say the set of raindrops that hit the paper during those 10 seconds, has 27 elements. Apparently, there may be 100 million droplets in a cloud. So, you can count them, at least approximately.

I agree there is no exact definition and the predicate is technically vague. But exactly the same considerations apply to notions like atom, molecule, ion, etc. And that doesn’t imply one can’t count the set of atoms in, eg, an oxygen molecule—under non-extreme circumstances. It is two and is usually written O2. (There’s a large literature on vague predicates, and also a large literature on individuation.)

More generally, I can’t quite fathom the animus against basic discrete mathematics of sets (and relations & functions), that is taught to teenagers at secondary school: Venn diagrams, simple statistics, the mean of a set of observations, a histogram, how to count the number of ways to shuffle a pack of cards, etc. If a political demographer discusses, e.g., the set of Clinton voters in 2016 and the set of Trump voters in 2016, they mean it. These sets can be counted—an election!

Posted by: Jeffrey Ketland on March 24, 2020 4:51 AM | Permalink | Reply to this

Re: Type Theory and Propositions

And that doesn’t imply one can’t count the set of atoms in, eg, an oxygen molecule—under non-extreme circumstances.

Of course it doesn’t. It just means that by choosing to apply mathematical set theory to such atoms, you are implicitly restricting consideration to such non-extreme circumstances. The set theory itself thereby yields no conclusions about the extreme circumstances – as implied by the conservativity result you’ve cited – but the reason is that it choosing a particular mathematical model for reality you’ve excluded those circumstances by fiat from the model.

I can’t quite fathom the animus against basic discrete mathematics of sets

You are misinterpreting what we are saying. No one has any animus against it. The only point is that, like all mathematics, it is only a model of reality.

Posted by: Mike Shulman on March 24, 2020 11:15 PM | Permalink | Reply to this

Re: Type Theory and Propositions

I brought up the subject of raindrops earlier as a kind of entity with less evident individuation properties than pieces of fruit on a desk. I was originally imagining them trickling down a window pane, merging tracks, etc., but let’s stay with clouds.

My idea was that, if someone proposes an arithmetic of cloud raindrops, I have every right to be suspicious. If they tell me that there are mm drops in one cloud and nn drops in another, then I have serious doubts about a claim that when the clouds merge there will be m+nm+n drops. I may even have questions about what it means to say there are precisely mm drops in a cloud. There’s no doubt some complicated dynamic evaporation-condensation processes occurring, requiring dust particles to act as condensation nuclei. Rapid temperature and pressure changes will affect these processes.

But just maybe for a very brief interval of time some sense can be given to there being mm drops in one cloud and nn in another. Then to the extent that this is reasonable, it would be fine to say of the two clouds that they jointly contain m+nm+n drops.

I should imagine that this timescale is too brief to allow cloud merging. Even then, I don’t know what effect the increase in water density, if indeed there is any, will have on the raindrop number in the merged cloud.

We may as well learn something about cloud dynamics while we’re on the subject, such as this:

Rain falls when gaseous water vapour in clouds condenses, forming tiny water droplets about 15 µm in diameter that must grow to about 100 µm before they fall as rain. Once the droplets reach around 40 µm in diameter they start to move down through the cloud and collide and merge with other droplets, increasing in size. But, neither condensation nor gravitational collisions effectively explain how the size of droplets increases from 15–40 μm. This is known as the “size-gap problem”.

It seems that turbulence forces these smaller droplets to cluster.

Anyway, from my position, applying mathematics to the world is a tentative business. Modelling assumptions are always open to challenge. The real cloud physics is evidently a complicated field. But where assumptions to take collections as sets are justified, then of course addition of set cardinalities will work as it should.

I certainly wouldn’t want to countenance some grand set of all ur-elements.

Posted by: David Corfield on March 24, 2020 10:40 AM | Permalink | Reply to this

Re: Type Theory and Propositions

If they tell me that there are m drops in one cloud and n drops in another, then I have serious doubts about a claim that when the clouds merge there will be m + n drops.

Can you provide a citation for any such assertion? After all, it’s obviously false, as children know. And the confusion here is the same one that Mill made and that Frege explained quite carefully. A number is a second-level property of a set, and not a first-level property of physical object. (Frege said “concept” (begriff) but it amounts to the same thing here.)

The physical combination of physical objects has nothing to do with the cardinal operation + on natural numbers or the \cup and \cap operations on sets. These are all distinct concepts. + (here) is a binary operation on the cardinal numbers of sets, and the relevant relationship is:

|XY|=|X|+|Y|+|XY||X \cup Y | = |X| + |Y| + |X \cap Y |

The operations \cup and \cap are binary operation on sets. I have no idea what “John \cup Ringo” might mean; but I know exactly what “{John,Ringo}{Paul,George}\{John, Ringo\} \cup \{Paul, George\}” means.

Doing the relevant applied mathematics: if XX is the set of water drops in cloud A and YY is the set of water drops in cloud B, and XY=X \cap Y = \varnothing, then in fact |XY|=|X|+|Y||X \cup Y| = |X| + |Y|. This has nothing to do with “merging”, or time, etc. \cup is a mathematical operation of sets, and doesn’t involve anything like “moving”, “merging”, etc. Suppose we perform two raindrop counting experiments. Suppose 13 raindrops fell on the counter in experiment A and 27 fell on the counter in experiment B, and no raindrop in either experiment fell in the other. Then 40 raindrops in all fell.

One needs to distinguish between the physical behaviour of physical objects and mathematical operations on sets, functions, etc. If you pay careful attention to how mathematics is applied—as Frege, for example, did—you will see how to analyse this correctly. Another example he discusses is a pack of cards on a table. This is not a set. It is a physical object—spread out in space & time. At some fixed time instant, one may consider the set CC of cards. But this set is not the physical object. One may consider the set AA of atoms in the cards. But this set is not the physical object. One may consider the set QQ of queens in the cards. But this set is not the physical object either. And all these sets, C,AC, A and QQ have different cardinalities.

Posted by: Jeffrey Ketland on March 24, 2020 4:32 PM | Permalink | Reply to this

Re: Type Theory and Propositions

Oops, typing too quickly. Typo. That should say,

|XY|=|X|+|Y||XY||X \cup Y| = |X|+|Y|-|X\cap Y|

Posted by: Jeffrey Ketland on March 24, 2020 4:47 PM | Permalink | Reply to this

Re: Type Theory and Propositions

The logician Arthur Prior, in the context of traditional logic (as logic over type theory), said that ‘every statement includes an implicit assertion of its own truth’, and in practice mathematicians usually interpret logical statements in such a manner. However, this isn’t exactly true in homotopy type theory, because a statement such as ‘for all terms aa in AA, P(a)P(a)’ and ‘for all terms aa in AA, P(a)P(a) is true’ for a predicate or type family PP would be equivalent in traditional logic, but the first statement would be rendered as a:AP(a)\prod_{a:A} P(a) while the second statement would be rendered as a:AisContr(P(a))\prod_{a:A} isContr(P(a)) as contractible types (or inhabited propositions) represent ‘true’ in homotopy type theory.

This becomes somewhat important in algebra, in the sense of the study of types equipped with terms, functions, and identities, as a statement such as the associative identity for a binary operation could be expressed as either ‘for all terms aa, bb, and cc in AA, a(bc)a \cdot (b \cdot c) is equal to (ab)c(a \cdot b) \cdot c’, or ‘for all terms aa, bb, and cc in AA, the statement that a(bc)a \cdot (b \cdot c) is equal to (ab)c(a \cdot b) \cdot c is true’. To the average mathematician, both statements would seem to be equivalent to each other. However, in homotopy type theory, the first identity would be written as a:A b:A c:Aa(bc)=(ab)c\prod_{a:A} \prod_{b:A} \prod_{c:A} a \cdot (b \cdot c) = (a \cdot b) \cdot c while the second identity would be written as a:A b:A c:AisContr(a(bc)=(ab)c)\prod_{a:A} \prod_{b:A} \prod_{c:A} isContr(a \cdot (b \cdot c) = (a \cdot b) \cdot c) Now, these two identities are not equivalent; many times the first identity is untruncated or merely nn-truncated for a natural number nn, while the second identity is always a proposition. Furthermore, if a magma (A,)(A,\cdot) came with the first identity, then AA would be akin to something like a non-unital A 3A_3-space from algebraic topology, while if that same magma (A,)(A,\cdot) came instead with the second identity, then AA would be more like a pre-semigroup, in the same sense that a pre-order is an untruncated (partial) order and a pre-category is a category whose type of objects is untruncated.

Thus, in addition to the distinction between the bracket higher inductive type |A|\vert A \vert and AA itself, the disjunction higher inductive type ABA \wedge B and the binary coproduct inductive type A+BA + B, and the existential quantifier higher inductive type (a:A)P(a)\exists (a:A) P(a) and the dependent sum inductive type (a:A)P(a)\sum (a:A) P(a), one should also speak of the distinction between isContr(a=b)isContr(a = b) and a=ba = b, as an identity type a=ba = b in homotopy type theory behave differently from the equality a=ba = b in traditional logic, while isContr(a=b)isContr(a = b) behaves more like the equality a=ba = b in traditional logic.

Posted by: Madeleine Birchfield on February 14, 2022 1:43 AM | Permalink | Reply to this

Re: Type Theory and Propositions

In addition, isContr(A)isContr(A) is useful for defining the uniqueness quantifier for a type AA and a predicate PP, in the following manner: !(a:A)P(a)isContr( a:AP(a))\exists!(a:A) P(a) \coloneqq isContr\left(\sum_{a:A} P(a)\right) rather than the mere existential quantifier as the bracket type of the dependent sum type: (a:A)P(a)| a:AP(a)|\exists(a:A) P(a) \coloneqq \vert\sum_{a:A} P(a)\vert

Posted by: Madeleine Birchfield on February 14, 2022 2:07 AM | Permalink | Reply to this

Re: Type Theory and Propositions

The logician Arthur Prior, in the context of traditional logic (as logic over type theory), said that ‘every statement includes an implicit assertion of its own truth’, and in practice mathematicians usually interpret logical statements in such a manner. However, this isn’t exactly true in homotopy type theory, because a statement such as ‘for all terms aa in AA, P(a)P(a)’ and ‘for all terms aa in AA, P(a)P(a) is true’ for a predicate or type family PP would be equivalent in traditional logic, but the first statement would be rendered as a:AP(a)\prod_{a:A} P(a) while the second statement would be rendered as a:AisContr(P(a))\prod_{a:A} isContr(P(a)) as contractible types (or inhabited propositions) represent ‘true’ in homotopy type theory.

That statement by Prior is still true in homotopy type theory if one restricts the type families to be valued in propositions: a:AisProp(P(a))\prod_{a:A} isProp(P(a)) is inhabited iff a:AisContr(P(a))\prod_{a:A} isContr(P(a)) is inhabited. In the context of algebra, one could simply use isProp(A)isProp(A) and isContr(A)isContr(A) interchangeably, as for the dependent product type to be inhabited, each individual isProp(A)isProp(A) would have to be inhabited, making it equivalent to isContr(A)isContr(A).

Posted by: Madeleine Birchfield on February 14, 2022 2:49 AM | Permalink | Reply to this

Post a New Comment