### Making Life Hard For First-Order Logic

#### Posted by David Corfield

I mentioned in a previous post Sundholm’s rendition in dependent type theory of the Donkey sentence:

Every farmer who owns a donkey beats it.

For those who find this unnatural, I offered

Anyone who owns a gun should register it.

The idea then is that sentences of the form

Every $A$ that $R$s a $B$, $S$s it,

are rendered in type theory as

$\prod_{z: \sum_{x: A} \sum_{y: B} R(x, y)} S(p(z), p(q(z)),$ where $p$ and $q$ are the projections to first and second components. We see ‘it’ corresponds to $p(q(z))$.

This got me wondering if we could make life even harder for the advocate of first-order logic – let’s give them the typed version to be generous – by constructing a natural language sentence which it would be even more awkward to formalise.

One thing to note is that the type above has been formed from a dependency structure of the kind:

$x: A, y: B, w: R(x, y) \vdash s: S(x, y).$

Now I’ve been writing up on the nLab some of what Mike told us about 3-theories back here. Note in particular his comments on the limited dependencies which may be expressed in the ‘first-order 3-theory’:

one layer of dependency: there is one layer of types which cannot depend on anything, and then there is a second layer of types (“propositions” in the logical reading) which can depend on types in the first layer, but not on each other.

So to stretch this 3-theory we should look for a maximally dependent structure. Take something of the form

$x: A, y: B(x), z: C(x, y) \vdash d:D(x, y, z).$

Ideally the types will all be sets.

By the time quantification has been applied, the left hand side swept up into an iterated dependent sum and a dependent product formed, the proposition should be bristling with awkward anaphoric pronouns.

The best I could come up with was:

Whenever someone’s child speaks politely to them, they should praise them for it.

A gendered version with, say, men and daughters would help with the they/them clashes.

Whenever a man’s daughter speaks politely to him, he should praise her for it.

Any better candidates?

## Re: Making Life Hard For First-Order Logic

It seems the first appearance of a donkey sentence was in 1328!

Only six and a half centuries later we had a proper formalism for it.