David Corfield logic-mathematics

Idea

Wittgenstein claimed that logical constants are just part of the grammar of language, that they don’t refer. This agrees with the expressivist idea that they make explicit aspects of our inferential practices. He made similar claims for counting numbers – the shopkeeper’s five apples.

Now think of the following use of language: I send someone shopping. I give him a slip of paper marked “five red apples”. He takes the slip to the shopkeeper, who opens the drawer marked “apples”; then he looks up the word “red” in a chart and finds a colour sample next to it; then he says the series of elementary number-words - I assume that he knows them by heart - up to the word “five”, and for each number-word he takes an apple of the same colour as the sample out of the drawer. – It is in this and similar ways that one operates with words. – “But how does he know where and how he is to look up the word ‘red’ and what he is to do with the word ‘five’?” – Well, I assume that he acts as I have described. Explanations come to an end somewhere. - But what is the meaning of the word “five”? - No such thing was in question here, only how the word “five” is used. (Philosophical Investigations, §1.)

If what is logical incurs no referential costs, then perhaps whether mathematics incurs such costs depends on where the logical end and the mathematical begin. Natural numbers can be expressed in HoTT. Is everything that HoTT expresses logical? But it expresses many constructions from homotopy theory, group actions, …

And yet

The fundamental groupoid of a space is a logical construction… Logical methods suffice in principle to capture a great deal of homotopy theory. (Awodey, Homotopy type theory, Logic Colloquium 2011, slides, 72)

This relates to the idea of logic and invariance (Mautner-Tarski), and HoTT as invariant under equivalence.

Details

If we accept the claim that logical terms are punctuation, part of the grammar, and so non-referential, why not carry this over to all of HoTT?

If the narrowly logical is articulated by FIEC (formation-introduction-elimination-computation) rules, is everything articulated by FIEC logical? If not, where is the division? Just the propositional? But why there if propositions are just some types?

If HITs cover dependent sums and natural numbers, why should one be seen as logic and the other not? On the other hand, perhaps the question of ‘logic’ is less important and the real question is one of reference.

Some HITs have as inputs other types (dependent sum), others do not (the natural numbers). It would be strange that the latter are taken as referential on that ground.

Why is the passage from $A: \mathcal{U}$ and $B: A \to \mathcal{U}$ to $\sum_{x:A}B(a): \mathcal{U}$ logical, but the passage from nothing to $\mathbb{N}: \mathcal{U}$ not?

In natural language, the former is the ‘and’ of ‘A person and one of their documents’, or ‘This is a Bordeaux and a very good one at that’.

This is close to the idea of axioms as rules without premises. But there’s a difference between axioms without FIEC rules (e.g., univalence in Book HoTT), and as part of a general HIT formation process, which just happens not to rely on existing types.

Constructs

• $A \wedge B$ for propositions, $A \times B$ for sets.

• Dependent sum, how could the ‘and’ differ referentially between ‘It is raining and it is windy’, ‘It’s raining and doing so heavily’, ‘A place and a time’, ‘A parent and one of their children’?

• What of the types 0 and 1, corresponding to “False” and “True”? When I say there aren’t any $A$s, don’t I mean $A = 0$? These can be seen as (nullary) operations, included in the:

“natural correspondence between logical operations on propositions, expressed in English, and type-theoretic operations on their corresponding types of witnesses.” (HoTT book, p. 41)

These are pure propositions.

(In the HoTT book sometimes the elements of 2, $0_2$ and $1_2$ are called “false” and “true”.)

• $A: \mathcal{U}$ to $||A||: \mathcal{U}$. A HIT. Not unreasonably a logical construction, like $\neg$. Note the proximity of prop truncation and double negation.

• $A: \mathcal{U}$ to $List(A):\mathcal{U}$, inductive type. $List(\mathbf{1})$ is equivalent to $\mathbb{N}$. List is a unary operation.

• Natural numbers as HIT.

• $||-||$ is propositional truncation, the modality $Loc_{S^0}$. Localization modalities as logical?

Applied logic

We get to see an applied logic readily. So we teach propositional logic and have our students apply it to the world. Some propositions are empirical: It is raining and it is warm, therefore it is raining.

With first-order logic we consider instances where the domain of variation includes empirical entities. Metaphysicians claim that ‘everything exists’, meaning anything their variables range over.

We have hardly ever seen an applied HoTT. Book HoTT is pure. We would need to add in some empirical types for an applied HoTT.

Natural numbers

Before we get to $\mathbb{N}$ as HIT, simple forms of counting rely on providing equivalences to ordered sets of body parts, see Body-part counting system, Numeral Bases. In any case, the dominant decimal and less common vigesimal systems clearly arose through digits.

Material recordings of number, such as clay tokens.

Early counting establishes equivalence between types. Counting words abstracted from material types to a pure type of numbers. But this also occurs in logic with the pure propositions of ‘True’ and ‘False’. We start by comparing propositions to known facts or non-facts, ‘Sure as I’m standing here’, ‘then I’m a Dutchman’. Then we abstract away to the pure ‘True’ and ‘False’, $1$ and $0$.

Now saying that a proposition, $P$, is true is saying $P \simeq 1$. This is no less committing to the abstract then saying that I have 5 apples.