David Corfield



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, H/W\mathbf{H}/W is a subobject of WW. So if WW 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 1\mathbf{1} (HoTT book, p. 41). So when we say ‘PP is true’, this is to state an identity of types. In the context of propositional extensionality, ‘PP is true’ means PP= True: Type, and so by the univalence axiom P1P \simeq \mathbf{1}. False is the abstract proposition 0\mathbf{0}.

‘Everything John says is true’, P:Prop(says(John,P)P=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:Nn: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\|A\| for a type AA.

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

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

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

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

Negative facts

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

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

Last revised on November 17, 2020 at 02:52:25. See the history of this page for a list of all contributions to it.