David Corfield
belief

“One must be careful not to jump to the conclusion that believing something to be so is the same as believing something to be true. What one believes when one believes that something is so is precisely that things are so. What one believes when one believes something to be true is a proposition, statement, assertion, declaration, allegation or announcement to the effect that things are so. For it is the propositions, statements, assertions, declarations, allegations or announcements that are true or false.”

[Hacker, 2013, p 205]

Hacker, P M S (2013), The Intellectual Powers: A Study of Human Nature, Oxford.

Believe that PP

Believe ‘P’ to be true.

Believe that Id(P,T)Id('P', T). But why TT and not T'T'?

So we believe types not names of types. Or do we believe that the type is inhabited? We believe ‘that PP’.

  • believe something to be so
  • believe something to be the case
  • believe something to be a fact
(P=true)(Ptrue). ('P' = 'true') \simeq (P \simeq true) \,.
(P=true)(El(P)El(true)). (P = true) \simeq (El(P) \simeq El(true)) \,.

But some systems prefer to denote the distinction either by

P is a type, so ‘P’: Type

or

P: Type, and El(P) is the type of its elements.

Adopting the former, to say that one believes that P is to affirm an element of P.

To say that ‘P’ is true is to affirm an element of Id_Type (‘P’, ‘True’)

But then by univalence

Id_Type (‘P’, ‘True’) is equivalent to Equiv(P, True), where True is the type 1 with one element.

So to say that ‘P’ is true is equivalently to say that P is inhabited. It’s inhabited by the state of affairs that makes it true.

Last revised on May 27, 2021 at 03:24:00. See the history of this page for a list of all contributions to it.