## August 23, 2020

### Formal and Material Inference

#### Posted by David Corfield

A distinction is made within philosophy between 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.

A classic example of a formal inference is $A \& B$, therefore $A$. Substitute any propositions for $A$ and $B$ and the inference goes through. The conjunction $\&$ is a piece of logical vocabulary. By contrast, the thinking goes, that $C$ is west of $D$ implies that $D$ is east of $C$ is a piece of material inference, relying on the relation between the non-logical concepts, ‘east’ and ‘west’. Substitute ‘older’ for ‘east’ and ‘larger’ for ‘west’ and the inference fails.

The philosopher Wilfred Sellars famously asserted that in such cases we’re not merely employing a tacit proposition, i.e., here ‘If $X$ is west of $Y$, then $Y$ is east of $X$’, instantiating it and then using modus ponens. For Sellars, and those following him, like Robert Brandom, material inference is primary; only for a limited portion of our inferential practices has humankind managed to extract formal inference schemas.

But then how to decide what is ‘logical’ and what ‘non-logical’? As an adherent of dependent type theory, can’t I hold any inference carried out in that system to be formal?

Say I have judged $j: P$ and $f: \neg (\sum_{x: P}H(x))$, where $H$ is a predicate on $P$. Then defining for $x: H(j)$, $g(x):\equiv f(j, x)$, I can now judge $g: \neg H(j)$, using standard type-theoretic rules.

Rewriting this inference in something closer to English, we find the syllogism:

$j$ is a $P$, No $P$s are $H$, therefore $j$ is not $H$.

As a valid syllogism, any substitution should do, so let’s choose a type, $P$, say $Person$. $j$ is an element of $P$, so let’s say Jane. $H$ is a property of people, let’s say ‘being in this house’.

Then we have the inference

Jane is a person. No people are in the house. Therefore Jane is not in the house.

OK, why this example?

Because it, or something very like it, appears already in the literature:

• González de Prado Salas, J., de Donato Rodríguez, X. & Zamora Bonilla, J. 2017. Inferentialism, degrees of commitment, and ampliative reasoning. Synthese. (paper)

if I am committed to endorsing the proposition ‘The house is empty,’ I will also be committed to endorsing ‘Jane is not in the house.’

…if one wants to characterize inferentially the content associated with non-logical vocabulary, one has to consider inferences that are not formally good, but that are made good by the content of the (non-logical) concepts they involve–that is, materially good inferences (like the inference about the empty house mentioned above).

Surely it can’t be that the translation between ‘No people are in the house’ and ‘The house is empty’ changes the inference from being formal to being material. When I learn to say of a house that it’s empty, I know that it’s defined to mean that they’re aren’t people in the house. I must learn that the presence of doors within doesn’t count. And I’d better know that Jane is a person. I wouldn’t have concluded from the house’s emptiness that just anything is not in the house.

Another case of claimed material inference, one given by Sellars himself, is that from ‘This is red’ to ‘This is colored’. On p. 17 of Chapter 1 of my book, which OUP has now made available, I sketch a type-theoretic account. To be able to use such language, to know that there is a type of colours, that red is a colour, that some things have a colour, when all this is written type-theoretically, I don’t see why we can’t take it too as a piece of formal inference.

Posted at August 23, 2020 10:20 AM UTC

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

### Re: Formal and Material Inference

The red ball case is, I claim, an instance of a general inference scheme which says that if we have two types, $A$ and $B$, which are sets, and a relation between them, $R$, then given $a:A$, $b:B$ and that $R(a,b)$ is the case, then $\sum_{x: B}R(a,x)$ is inhabited, and so the propositional truncation $||\sum_{x: B}R(a,x)||$ is true.

So, for some choices of the components of this set-up we have special words to employ for the latter proposition: the object $a$ is colored; the person $a$ is a parent; the item $a$ is used; the house $a$ is occupied; the number $a$ is composite, and so on.

To insist that such instances of the inference scheme are to be counted as material will require a difficult line to be drawn as to acceptable rewriting. Presumably all allow the rewriting that enables us to consider the inference from ‘Jill is happy, and Jack is too’ to ‘Jack is happy’ as formal.

Posted by: David Corfield on August 23, 2020 2:43 PM | Permalink | Reply to this

### Re: Formal and Material Inference

Something to resolve for any formal/material inference distinction is what to do with judgmental equality (definitional equality).

Say we have the judgments $a:A$ and $A \equiv B$, then we may derive the judgment $a:B$.

Presumably if we have a piece of formal inference and then we use a definitional equality to rewrite it, then the inference remains formal.

So say I have a couple of propositions, $P$ and $Q$, and I define $R \equiv P \& Q: Prop$. Then the inference from the judgments $p: P$ and $q: Q$ to $(p, q): P \& Q$ means that we can also conclude $(p, q): R$ formally.

I’m finding it hard to see how any deductively valid inference won’t be formal.

Posted by: David Corfield on August 23, 2020 6:30 PM | Permalink | Reply to this

### Re: Formal and Material Inference

Perhaps it is better to talk about formal and material inference in the context of a certain logic. One statement might be material inference in propositional or first-order logic, but formal inference in dependent type theory or categorical logic.

### Re: Formal and Material Inference

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.

Posted by: David Corfield on August 24, 2020 7:48 AM | Permalink | Reply to this

### Re: Formal and Material Inference

Not necessarily, especially if one is a model theorist studying models of logic and their relationships with each other.

### Re: Formal and Material Inference

Thanks for bringing this up, as I had been wondering myself about the formal/material distinction reading Brandom.

I was thinking of interpreting this with Hillary Putnam’s famous “The Meaning of ‘Meaning’”. Putnam argues very convincingly that words which he called natural kinds such as “Oak Tree”, “water”, (“house”?)… get their meaning from the world. People in the ancient world were able to use the words with only very partial theories of the world by pointing at examples of them. And yet we can now understand them as having spoken about H2O or perhaps soon of an organism with a given genetic code. The natural kinds were then discovered to have certain properties, for which theories such as the one’s you mention above can then be built. But the primary meaning is given by the world, and affects the theories we can build from them.

Perhaps then the distinction is one we also know between syntax and semantics. Since we now also know that these are related by a Galois Connection or in more contemporary terms an Adjunction. This then gives rise to a duality see Maruyama’s work on “The Dynamics of Duality”. If so it won’t be surprising that both these worlds mirror each other. But there may be a difference depending on where one starts. In formal reasoning from the syntactic side, in interaction with the world (being-in-the-world?) with the semantic side. And it is of course very likely that none is primary.

Posted by: Henry Story on August 24, 2020 11:51 AM | Permalink | Reply to this

### Re: Formal and Material Inference

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.

Posted by: David Corfield on August 24, 2020 12:50 PM | Permalink | Reply to this

### Re: Formal and Material Inference

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?

Posted by: Henry Story on August 25, 2020 8:52 AM | Permalink | Reply to this

### Re: Formal and Material Inference

I don’t feel the type theoretic account is really changing anything here. To see this in one way, let P be the type of people who are in this house. We then get a nonsensical interpretation with H.

I think essentially what has happened is just that the non-logical part is moved into the definition and/or intepretation of the types.

Posted by: Richard Williamson on August 24, 2020 1:05 PM | Permalink | Reply to this

### Re: Formal and Material Inference

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.

Posted by: Richard Williamson on August 24, 2020 1:17 PM | Permalink | Reply to this

### Re: Formal and Material Inference

I think the inferentialist would disagree that we can help ourselves to a definitional equality ‘The house is empty’ := ‘No people are in the house’. Why? Because these sentences themselves stand in a relation of material inference to one another that articulates the content of the concept of the house’s being empty. That relation is what allows us to propose their definitional equality without other ‘scorekeepers’ calling us out on having made a nonsense equation (recall that in the account of scorekeepers’ activity, Brandom does not need to appeal to their having mysteriously antecedently available concepts, be they logical or otherwise, that would provide some innate Cartesian light by which to assess proprieties of inference).

In the context of extending type theory to natural language, these background material inferences would be just what is encoded by introduction rules for “empirical” types. I think I am in agreement with Richard Williamson on this point.

Posted by: Matt Earnshaw on August 24, 2020 7:33 PM | Permalink | Reply to this

### Re: Formal and Material Inference

…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.

Posted by: David Corfield on August 25, 2020 8:02 AM | Permalink | Reply to this

### Re: Formal and Material 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.

Posted by: Richard Williamson on August 25, 2020 11:12 PM | Permalink | Reply to this

### Re: Formal and Material Inference

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’.

Posted by: David Corfield on August 26, 2020 1:58 PM | Permalink | Reply to this

### Re: Formal and Material Inference

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.

Posted by: Richard Williamson on August 27, 2020 10:13 AM | Permalink | Reply to this

### Re: Formal and Material Inference

OK, but at this point you’ve departed from what either of Sellars and Brandom were looking to do with the distinction. For Brandom in Making it Explicit, goodness of material inference, reasoning about the world, is prior. For some parts of this, but very definitely not all, one can understand this goodness in terms of the validity of the logical form of the inference where one has come to see the roles of certain items of logical vocabulary.

An interesting project then, I think, is to understand dependent type theory in such a light.

Posted by: David Corfield on August 27, 2020 1:38 PM | Permalink | Reply to this

### Re: Formal and Material Inference

Hi David. I am not sure that Brandom would agree with your characterisation of formal inference :

“… 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.”

Brandom spends much more time setting up the idea of “formally good inference” than he does “formal inference”. Here he is quite explicit in saying that formally good does not mean logically good, and form does not mean logical form:

“For given a subset of vocabulary that is privileged or distinguished somehow, an inference can be treated as good in virtue of its form, with respect to that vocabulary, just in case

• It is a materially good inference, and
• It cannot be turned into a materially bad one by substituting nonprivileged for nonprivileged vocabulary in its premises and conclusions.

Notice that this substitutional notion of formally good inferences need have nothing special to do with logic. If it is logical form that is of interest, then one must antecedently be able to distinguish some vocabulary as peculiarly logical. That done, the Fregean semantic strategy of looking for inferential features that are invariant under substitution yields a notion of logically valid inferences. But if one picks out theological (or aesthetic) vocabulary as privileged, then looking at which substitutions of nontheological (or nonaesthetic) vocabulary for nontheological (nonaesthetic) vocabulary preserve material goodness of inference will pick out inferences good in virtue of their theological (or aesthetic) form”.

Brandom, Articulating Reasons p.55, my italics.

An inference that is good by virtue of its ethical form might be something like:

$\frac{William is \mathrm{a} virtuous fellow}{William is \mathrm{a} courageous fellow}$

As you have pointed out elsewhere, this is not to be understood as an enthymeme with a suppressed premise of “All virtuous fellows are courageous fellows”.

It’s true that Brandom thinks that material inferences are those inferences the correctness of which cannot be determined solely by virtue of logical form – they are “those whose correctness or incorrectness essentially depends on or articulates the content of the nonlogical concepts that occur in their premises or conclusions” (AR, p.44). But as the block quote above shows, formally good inferences are a species of materially good inferences, and inferences that are good by virtue of logical form are a subspecies of formally good inferences.

So while the phrase “formal inference” does appear throughout Brandom’s Making it Explicit, I think it can only be understood as meaning “an inference made for reasons of goodness of form”, where form isn’t a logical notion.

Hopefully this doesn’t seem like nitpicking. But if these things aren’t kept apart then Brandom’s explanations start to sound very circular.

That actually connects to another part of your post – Brandom relies on a notion of “nonlogical vocabulary” in setting up his definition of material inference (see inline quote above).

Brandom does have an informal demarcation criterion for logical vocabulary – a kind of pragmatically motivated characterisation in terms of what he thinks logical assertions do. MacFarlane has an interesting paper “Brandom’s Demarcation of Logic” where he relates Brandom’s proposal to the work of Popper, Kneale and Hacking. Kosta Došen should probably be in there too. These are all in the Gentzen-inspired, logical inferentialist vein. As you know, I am not convinced that the Brandomian inferentialist account of meaning has any commitments to logical inferentialism. So it would be very interesting to see how well the Tarskian approach that you mention fits with Brandom’s philosophy of logic.

Posted by: Gavin Thomson on August 24, 2020 11:50 PM | Permalink | Reply to this

### Re: Formal and Material Inference

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.

Posted by: David Corfield on August 25, 2020 8:59 AM | Permalink | Reply to this

### Re: Formal and Material Inference

Looking over people’s responses above, I rather think we should be employing Mike’s ideas in What Is an n-Theory? and speaking in terms of syntactic and semantic $n$-theories, for $n = 0,1,2,3$.

Perhaps one only wants to take the higher levels as ‘logical’, e.g, inference in 2-theories such as first-order intuitionistic logic or first-order modal logic or propositional logic.

With the specification of generating types, terms and axioms in a 1-theory, perhaps people sense a loss of subject neutrality.

Posted by: David Corfield on August 25, 2020 10:05 AM | Permalink | Reply to this

Post a New Comment