Austinian propositions

[BP83] [Gin12]

An Austinian proposition pairs a situation with a situation type and is true iff the situation satisfies the type ([BP83]; [Gin12] Ch. 4, [sit = s, sit-type = T]). Separating the situation from the classifying predicate — rather than carrying a witness by construction — yields propositions that can be false, which is what discourse needs: an asserted content enters FACTS as a checkable claim.

Main declarations

• CheckableAustinian — situation + classifying predicate; truth is isTrue, falsity isFalse
• BCheckableAustinian — the Bool-valued variant for computational use; toBProp evaluates the classifier as an S → Bool

structure Intensional.CheckableAustinian (S : Type) : Type

A checkable Austinian proposition: a situation paired with a classifying predicate ([Gin12] Ch. 4). Truth requires the situation to satisfy the type, but need not hold — unlike a witness-carrying situation–type pair, this proposition can be false.

• sit : S

  The situation being classified

• sitType : S → Prop

  The classifying predicate (situation type)

def Intensional.CheckableAustinian.isTrue {S : Type} (p : CheckableAustinian S) : Prop

A checkable Austinian proposition is true iff the situation satisfies the type.

Equations

• p.isTrue = p.sitType p.sit

def Intensional.CheckableAustinian.isFalse {S : Type} (p : CheckableAustinian S) : Prop

A checkable Austinian proposition is false iff the situation doesn't satisfy the type.

Equations

• p.isFalse = ¬p.sitType p.sit

structure Intensional.BCheckableAustinian (S : Type) : Type

Decidable variant of CheckableAustinian for computational use.

• sit : S
• sitType : S → Bool

def Intensional.BCheckableAustinian.isTrue {S : Type} (p : BCheckableAustinian S) : Bool

Decidable truth check.

Equations

• p.isTrue = p.sitType p.sit

def Intensional.BCheckableAustinian.toBProp {S : Type} (p : BCheckableAustinian S) : S → Bool

Convert a decidable Austinian to S → Bool: evaluate the classifier at each situation.

Equations

• p.toBProp = p.sitType

theorem Intensional.BCheckableAustinian.toBProp_at_sit {S : Type} (p : BCheckableAustinian S) (h : p.isTrue = true) : p.toBProp p.sit = true

A true Austinian proposition's toBProp holds at its situation.