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.
As a type, a proposition has at most one element, or in other words any two elements are identified.
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.
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)$.
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.
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
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.)
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?
What elements can we generate for $\neg P$?
How fine-grained is the type theory?
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’.
Last revised on January 24, 2022 at 04:25:11. See the history of this page for a list of all contributions to it.