This post branches from the previous post at the indicated point.
Explain this notation:
\[ \text{Fact} = \lambda w \lambda t [^0 A_{wt} [^0 H_{wt} \ ^0 M_{wt}]] \]
This notation comes from Transparent Intensional Logic (TIL), a higher-order intensional logic developed by Pavel Tichý, which is based on λ-calculus and type theory. The notation expresses a fact as a structured construction, where facts are functions that take a possible world \( w \) and a time \( t \) as arguments and return a truth value.
Breaking Down the Notation
\[ \text{Fact} = \lambda w \lambda t [^0 A_{wt} [^0 H_{wt} \ ^0 M_{wt}]] \]
Each part has a specific meaning:
-
\( \lambda w \lambda t \) → This denotes a function that takes a possible world \( w \) and a time \( t \) as arguments.
- In Possible Worlds Semantics (PWS), truth is relative to a world \( w \) and a time \( t \).
- The expression after these λ-binders defines what this function outputs.
-
\( [^0 A_{wt} [^0 H_{wt} \ ^0 M_{wt}]] \) → This is the core construction that determines the fact in \( w \) and \( t \). It consists of:
- \( ^0 A_{wt} \): The trivialization of the function \( A_{wt} \), which represents a property or relation.
- \( ^0 H_{wt} \): The trivialization of the function \( H_{wt} \), which denotes an entity (e.g., “the highest mountain”).
- \( ^0 M_{wt} \): The trivialization of the function \( M_{wt} \), which denotes another entity (e.g., “Mount Everest” or another mountain).
Understanding the Construction
-
The inner expression: \[ [^0 H_{wt} \ ^0 M_{wt}] \] means that the function \( H_{wt} \) is applied to \( M_{wt} \). This could mean checking whether the object denoted by \( M_{wt} \) (e.g., Mount Everest) satisfies the property \( H_{wt} \) (e.g., being the highest mountain).
-
Then, the outer function \( A_{wt} \) is applied: \[ ^0 A_{wt} [^0 H_{wt} \ ^0 M_{wt}] \] This could represent a further predicate (e.g., "is located in Asia") applied to the constructed result.
-
Finally, \( \lambda w \lambda t \) abstracts over this entire expression, making it a function of world and time.
What This Represents
This expression defines a propositional function that determines whether a given sentence (such as "The highest mountain is in Asia") is true in different possible worlds and times.
For example:
- \( H_{wt} \) could mean “the highest mountain in the world at \( w,t \)”.
- \( M_{wt} \) could denote “Mount Everest”.
- \( A_{wt} \) could mean “is located in Asia”.
- The entire expression constructs the proposition “The highest mountain is in Asia”, whose truth value depends on \( w \) and \( t \).
In short: \[ \lambda w \lambda t [^0 A_{wt} [^0 H_{wt} \ ^0 M_{wt}]] \] defines a function that returns "true" (T) if the highest mountain in world \( w \) and time \( t \) is in Asia, and "false" (F) otherwise.
Would you like a concrete example with specific world-time assignments?