David Corfield proposition

What is a proposition?

A proposition is a type of predicative act (Hanks, Soames)

Certainly a proposition is a type, which as such partakes in judgements. But it’s a type of the obtaining of a state of affairs. There’s a proposition as type, what it means to be inhabited, and the judgement as to it’s being inhabited.

A proposition is a subsingleton, or subterminal object

As a type, a proposition has at most one element, or in other words any two elements are identified.

A proposition is a subset of worlds

A subterminal object, a monomorphism to the terminal object, in the slice topos, $\mathbf{H}/W$ is a subobject of $W$. So if $W$ is a set of worlds, then a proposition is a subset of worlds.

Reference of a sentence is its truth-value

True is an abstract proposition, a name for the unit type $\mathbf{1}$ (HoTT book, p. 41). So when we say ‘$P$ is true’, this is to state an identity of types. In the context of propositional extensionality, ‘$P$ is true’ means $P$= True: Type, and so by the univalence axiom $P \simeq \mathbf{1}$. False is the abstract proposition $\mathbf{0}$.

‘Everything John says is true’, $\prod_{P: Prop} (says(John, P) \to P = True)$.

Is any subsingleton type a proposition?

If the type of apples on my tables has one or no members, do I call it a proposition? No, since it needn’t have been so. In fact I could have a time-dependent or place-dependent type, ‘apples on my table(t)’. Only if the type is forced to be subsingleton at all times do we say ‘proposition’. Is the flag flying today?

There may be subtle variations behind such judgements.

• Prime which are the difference between the squares of two primes.

• Pairs of primes whose squares differ by 5.

The latter looks like it could depend on $n:N$, with varying cardinalities. Once you come to see in a situation that there’s a most one, does judgement of propositional status change.

Proposition formation

• Truncation: $\|A\|$ for a type $A$.

• Implication into a prop: $[A, P]$, in particular $\neg A$.

• $\prod_{x:A} P(x)$ for propositions, $P(x)$ (subsumes latter).

• dependent proposition at a value, $P(a)$, dependent relation at tuple, etc..

• $Id_A(a, b)$ for a set $A$, and two elements.

If a sentence expresses a proposition, and a proposition is a type, then we should be able to think of sentence construction in terms of type formation.

When Frege proposes that the reference of a sentence is a truth value, why not say that a sentence is the name of a type? Then the reference of a true sentence is a type ‘equal’ to the type True.

Is there a difference between

1. A sentence expressing a proposition. The assertion of the proposition is a judgement that the proposition is true/inhabited. These include identity propositions for two elements of a set. (My car is grey. The colour of my car = grey.)

2. A sentence expressing the judgement of an element belonging to a type.

When I assert $a:A$, if it’s the case that $A = \sum_{x:B} C(x)$, then I’m asserting that $\pi_1(A)\;is\;C$.

Or the other way. I assert of an individual, $b:B$, that $p:C(b)$, so I’m asserting $(b, p): \sum_{x:B}C(x)$. Common that we have identified an entity of a basic kind and then specify an attribute holds. Do we never then simply assert $a:A$?

How about dependent product?

Negative facts

What elements can we generate for $\neg P$?

• $Id_A(a, b)$: could find $f: A \to B$, and proof that $\neg(f(a) = f(b))$.

Examples

How fine-grained is the type theory?

The table was covered in crumbs.

I don’t say ‘The war is covered in tunes’.

Flattish entity with small entities or continuous stuff distributed fairly densely and broadly over it. The beach was covered in deckchairs. The child was covered in mud.

Derives from sense of ‘The table was covered with a cloth’.

Bolzano’s Propositions in themselves