David Corfield dependency

That was fun, talking about the cutting edge of current geometry. I was left hoping clearer category-theoretic story which will make the pyknotic/condensed setting seem inevitable.

Back to more prosaic themes in my book. Woking backwards, Chapter 4 is on modality. Modal logic is big business in analytic philosophy due in large part to the work of Saul Kripke, Ruth Barcan and David Lewis. This marked quite a departure from the early years. I was interested to see this review of a book that explains the early

Thus Frege says clearly in The Foundations of Arithmetic, in an echo of Ueberweg, that a seemingly temporal concept like “inhabitant of Germany” does not express a concept, whereas “inhabitant of Germany at the beginning of the year 1883, Berlin time” does, and belongs to a given number for all time.

How odd! What’s wrong with a time-dependent concept/type?:

$t: Time \vdash$ Inhabitant of Germany$(t)$.

After all we draw graphs of

$t: Time \vdash$ Card(Inhabitant of Germany)$(t)$.

https://en.wikipedia.org/wiki/Demographics_of_Germany#/media/File:Population_of_German_territories_1800_-_2000.JPG

Implicit parameters

Jason Stanley

Context-dependency, domain indices, covert pronomial element, unpronounced syntactic structure.

All truth-conditional effects of extra-linguistic context can be traced to logical form.

If this has any chance of working, it has to be the logical form of dependent type theory.

Indexicals, demonstratives, pronouns

What are unarticulated constituents of utterances

I you here not bindable

p/100.

Why does mathematics adopt the policy of making explicit a variable. Let G be a group, and H a subgroup. Compare with early maths and their us of anaphora.

Any farmer, A, who owns a donkey, B, beats B.

What’s got me excited about Mike’s idea is that it makes sense of why some systems are more expressive than others. The variations he has for 3-theories concern arity and dependency structure.

Arity: this is whether our judgments will take the form one-one, many-one, many-many.

Dependency: this is whether there can be dependency between types/propositions occuring in a judgment. 3 stages here are: no dependency, full dependency of a type on any previous type, and an intermediate one (called ‘first-order’) - one layer of dependency: there is one layer of types which can’t 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.

Full dependency is more expressive than first-order is more expressive than no dependency.

We should see this in how people struggle to express things with first-order logic.

First off, they tend to adopt a single type for the first layer. This forces them to use predicates all over the place.

The can’t say ‘An elephant is a mammal’ without translating to ‘For everything, if it is an elephant then it is a mammal’.

But even if they used a typed first-order logic, they’ll still struggle. That’s why the Donkey sentence is wheeled out

x: Farmer, y: Donkey, z: Own(x, y) |- b: Beat(x, y, z)

If you quantify with type theory, you can send this to a type which reads naturally as

‘Any farmer who owns a donkey beats it’ where the ‘it’ lines up with a piece of syntax.

They have to shift to ‘For any farmer and any donkey, if the farmer owns it then he beats it.’

We should be able to make things worse for the first-order people, find an instance of

x: A, y: B(x), z: C(x, y) |- d: D(x, y, z)

and quantify requiring loads of anaphoric pronouns.

Any parent whose child is rude to them, should rebuke them for it.

That’s the best I have so far. Or

Whenever a parent has a child that is rude to them, they should rebuke them for it.

Gendered pronouns would help, if we’re still allowed them

Whenever a mother has a son that is rude to her, she should rebuke him for it.

First-order we have to do something like:

For all women, all children and all events, if the woman is mother to the child and if the event is one of the child being rude to the woman, then there should be an event which is the mother rebuking the child for the former event.