The n-Category Café

Right. But then surely the next step is to say that a logic is better than another logic when it construes as formal a larger part of what we consider ‘non-ampliative’ reasoning, i.e., reasoning which does not go beyond the information already present.

So far as HoTT goes as a logic, I think we should follow Steve Awodey here and, continuing the Mautner-Tarski approach, take it as a system which expresses invariant reasoning up to equivalence. This will include plenty of mathematical reasoning as ‘logical’.

The thing I really hadn’t thought about before is the role of definitional equality in all this as an integral part of HoTT. This concerns even very low-level reasoning. Is the inference from ‘X is a bachelor’ to ‘X is unmarried’ formal?

No, if one could replace these two for any other predicates. But if ‘is a bachelor’ is provided by definitional equality as the usual conjunction of properties, then Yes. For Martin-Löf, steps involving definitional equality are purely analytic, no construction is needed as in even the simplest case of concluding $P$ is true from $P \& Q$ is true. (See here.) I don’t see how these could compromise logicality.

Perhaps by thinking about how ‘east’ and ‘west’ are defined we could question the inference in the main post as to whether it’s really material.

At the same time it occurs to me that (modal) HoTT being built on Dependent Types may have something to say on this dependence of syntax on semantics. Does the ability of formulas to be made to depend on the world of the speaker, change how one can think of these problems?

Perhaps I should add that I do think one can approach natural language semantics in a type-theoretic way, but one has to build from the ground up in parallel with the syntax, as in the Montague semantics. One cannot just jump in the middle.

E.g. I might define a type Tree. To give that meaning, I need to say how I can construct a tree. I might have a rule that says given a term of Trunk and a term of a type Branches(t) for a trunk t:Trunk, then I can construct a term of type tree. I might leave Trunk and Branches as primitive, in which case non-logical input is required to say what a trunk and what ‘branches’ are (not addressing the question of how many branches are enough). Or I might provide constructors for Trunk and Branches as well. I might provide some kind of generic notion of ‘some X’ which allows me to make sense of ‘branches’ as ‘some Branch’ give a type Branch. Etc.

In summary, there is a balance between non-logical and logical, and how far one goes in the logical direction depends on one’s purpose. But, again, one cannot just jump in the middle, take arbitrary fragments of type theoretic syntax, and make good sense of natural language.

…propose their definitional equality…

In MLTT one doesn’t propose a definitional equality – such an equality is not a proposition, there’s no judgement as to whether it’s true.

Inside the theory, it does not make sense to negate or assume an equality-by-definition; we cannot say “if $x$ is equal to $y$ by definition, then $z$ is not equal to $w$ by definition”. Whether or not two expressions are equal by definition is just a matter of expanding out the definitions; in particular, it is algorithmically decidable (though the algorithm is necessarily meta-theoretic, not internal to the theory). (HoTT book, p. 19)

On the other hand, as the name suggests, one may propose a propositional equality. To establish that this is inhabited requires some deductive work.

…the content of the concept of the house’s being empty.

That assumes there’s a single content.

‘The house is empty’ may be used to express several different propositions depending on how ‘empty’ is to be understood, such as ‘Nobody is currently residing in the house’, ‘Nobody is inside the house at the moment’, or ‘There are no people, no furniture (or other movable objects) in the house.

Which is intended by the speaker is something that needs to be established before we start making inferences from their claim. If it’s ‘Nobody is currently residing in the house’, then inferring that Jane, the estate agent who’s selling the house, is not now in the house is invalid. She may well be measuring the size of the rooms.

It’s not a matter of deducing which version the speaker intends, though we may be able to rule out some options from what they say. I need to ask them what they mean by the claim. They will then reword their claim. If they say ‘I mean that nobody is in the house just now’, we can then nod through the inference to ‘Jane is not in the house’.

This scenario I want to take as formal inference.

(In response to David).

Let me try to make the point in a slightly different way. You wish to deduce from two judgements $j : P$ and $\neg \Sigma_{x : P} H(x)$ that $\neg H(j)$ is inhabited. But to do that, $P$ and $H$ have to be formal: one needs to formally say what it means to make the two judgements that you rely on. You then have two choices: leave $P$ and $H$ to be primitive/axiomatic; or provide rigorous constructors for the types. Since you have not done the latter, we must assume that you are taking the first approach. This means that when you interpret into natural language, you are making a non-logical/material/non-formal decision about how to make the interpretation of the primitive types. Hence the point that nothing is really changing fundamentally in the type-theoretic account.

This is what I was getting at in my first comment. There is nothing formally preventing nonsensical/paradoxical interpretations of the ‘syllogism’ you gave, because it makes formal sense to take $P$ to be something like in the example I gave. Of course I know that I will not be able to judge both that Jane is in this house and that there is nobody in this house, but the point is precisely that this knowledge is material/non-logical as far as your account goes: since you do not provide any constructors for the types involved, there is nothing formal/logical preventing such judgements that would lead to nonsense.

I think there are two issues occurring:

1. With regard to the use of different logical systems such as MLTT, first-order (untyped) classical logic, and any other of Mike’s 2-theories presented via the dependency structure of one of his 3-theories, where should we situate the formal/material divide. Is reasoning with any syntactical 1-theory in a chosen 2-theory to count as formal? Am I allowed definitional rewriting? What to say about the result of interpreting any piece of inference into the world?

2. Whether we find that different 2-theories allow a broader range of inferences to count as formal.

We can’t begin on (2) before settling (1).

Say I choose the 2-theory of classical propositional logic, and I stipulate the 1-theory, that there are two generating propositions, $A$ and $B$, and that $A \to B$ is true. In this 1-theory I may make the inference from $\neg B$ to $\neg A$. All, surely, perfectly formal.

Now I interpret it into a particular setting in the world. I may know that if a certain light is green, then the engine is running. Then I may reason from the fact that the engine is not running that the light is not green.

It’s my understanding that for Brandom this would also count as formal inference (though I wish he’d say relative to a specific logic). Detection of the logical form relies on our antecedent ability to distinguish logical vocabulary. In this simple case, we’d be looking to pick out ‘if…, then…’ and ‘not’. Substitution of any other pair of propositions will not change the status of the inference as good. This is in line with the Wikipedia entry and the formality of the syllogism of Socrates’s mortality.

What I’d like to know is the effect of definitional rewriting. ‘When the light glows green, the engine is running. The engine is off. Therefore the green light isn’t showing.’

Sellars offers the clear cut case of material inference from ‘It is raining’ to ‘The street will be wet’. I can’t see that anyone’s going to challenge this one.

But what to do with ‘The house is empty. Therefore Jane is not in the house.’? With minor rewriting it becomes formal for DTT and first-order logic.

As to splitting these two logics, perhaps we should throw in a (rather more natural) Donkey sentence to show why we might prefer DTT:

Any customer who has purchased a faulty radio from this shop will receive a refund for it.

The ‘logical vocabulary’ might appear to amount to ‘any’, but I can’t help but see a dependent product and a dependent sum in there, and the chance to represent naturally that anaphoric ‘it’.

Say I choose the 2-theory of classical propositional logic, and I stipulate the 1-theory, that there are two generating propositions, $A$ and $B$, and that $A \rightarrow B$ is true. In this 1-theory I may make the inference from $\neg B$ to $\neg B$. All, surely, perfectly formal.

Now I interpret it into a particular setting in the world. I may know that if a certain light is green, then the engine is running. Then I may reason from the fact that the engine is not running that the light is not green.

To focus just on this, I would say that there are several issues even here. The proposition “If the light is green, then the engine is running” relies on context for its truth (such as that the engine is in a car which is waiting at a traffic light). But your formal setup does not allow for this context. Thus, with respect to your formal setup, your interpretation that “If the light is green, then the engine is running” is true is more or less ‘meaningless’/an arbitrary choice, it doesn’t have anything to do with the logical connection of the propositions “light is green” and “engine is running”. Consequently, we cannot syllogistically deduce that “If the engine is not running then the light is not green”, for this syllogism does rely on the truth of “if the light is green then the engine is running” coming from the logical connection of the propositions “light is green” and “engine is running”.

Suppose that we instead look that “If I can see that the light at this traffic light is green, then I can hear that the engine of the car at this traffic light is running”. We might at first think to be able to regard this as a context-less interpretation of your formal system. But it is not necessarily true that “If I cannot hear that the engine of the car at this traffic light is running, then I cannot see that the light at this traffic is green”: maybe the reason that I cannot hear it is because another car started blaring some loud music. Thus it requires the material consideration that no car is blaring some loud music before I can admit the truth of “If I can see that the light at this traffic light is green, then I can hear that the engine of the car at this traffic light is running”. In some formal systems, we might try to get around this and make it formal by moving ‘no car is blaring loud music’ into the context. In your formal system, we might make the proposition even more complicated: “If I can see that the light at this traffic is green and no car is blaring loud music, then I can hear that the engine of the car at this traffic light is running”.

The point is that there is an infinite regression here. One can try to get away from material considerations by adding more and more things to the context, or by tweaking one’s formal system, but one cannot do this forever: material considerations have to enter somewhere. What I view your type theoretic account as doing is basically just shifting the material considerations a bit in this way.

How about “Socrates is human, humans are mortal, therefore Socrates is mortal”? I would argue that we cannot regard as this a pure interpretation of a syllogism in a formal system. It requires material judgement to know which substitutions are appropriate. E.g. “Jesus is human, humans are mortal, therefore Jesus is mortal” is of questionable truth for a Christian. In other words, we can admit the possibility of syllogistic deductions in natural language, but we can never take a formal system and regard all interpretations of deductions in it as syllogistically valid in natural language; material considerations will always enter in general somewhere. This goes back to the point I was initially making: if one formally defines the constructors of a type, then material considerations cannot enter there, but one has to take some types as primitive, and these will always be subject to material considerations in their interpretation into natural language.

Thanks, Gavin.

…formal and material inference. The first of these operates purely through the logical form of the relevant propositions, whereas the second relies on conceptual content occurring within them.

In MLTT one argues via judgements rather than propositions, so even this vague gloss above will need changing. Maybe,

The first of these operates purely through the logical form of the relevant judgements, whereas the second relies on conceptual content occurring within them.

As you take up later in your comment, what is taken as “logical” here is critical.

If it is logical form that is of interest, then one must antecedently be able to distinguish some vocabulary as peculiarly logical.

I don’t think the logical form of a piece of everyday reasoning has to be worn on the surface by a special logical vocabulary. Some massaging (or desugaring) may be needed first. And then it’s presumably not the case for Brandom that there’s a single logic with its single logical vocabulary. Different inferential systems will have different notions of logical form.

HoTT is certainly putting into question any idea of a boundary between the logical and the mathematical. Awodey writes later in the piece I mentioned:

We can justify the UA [Univalence Axiom] in much the same way: since every construction that one can actually write down in HoTT respects equivalence, i.e. is invariant, we might as well assume that all constructions are invariant – not because we believe in Wittgenstein’s theory about the syntactic nature of logic, though, but because we accept invariance as a reasonable formal model – an explication, if you will – of what it means for a statement, property, or construction to be “logical” in the broad sense (or, if you prefer, “mathematical”). That is to say, we decide to accept the above Tarski-Grothendieck Thesis.