Some initial thoughts.
Suppose we think of a Tarskian Truth Type T
in terms of Liskov Substitution Principles:
Subtype Requirement: Let
ϕ(x)
be a property provable about objectsx
of typeT
. Thenϕ(y)
should be true for objectsy
of typeS
whereS
is a subtype ofT
.
We might helpfully parse the above in the following way:
S < T
, t ∈ T
, s ∈ S
ϕ(t) → ϕ(s)
Suppose that there is a top-level Tarskian Truth Predicate T*
:
ϕ
(from above) like so: ϕ: T*(s) ↔ s
(letting ϕ
be the T-Schema).T*-1
is a subtype of T*
(T*-1 < T*
). If Liskov Substitution holds for T*-1
, T*
then any paradox from ϕ
would presumably appear in T*-1
.ϕ
must not entail a Contradiction (which it does from the Liar Paradox), Liskov Substitution must not hold, T*-1 < T*
must be False, or ϕ
must be incorrect.I've addressed the fourth (last) option here and the first elsewhere. But what about the other/middle two? Those seem like novel ways to frame the problem and consider the relation of Truth and its Properties.
The original formulation (sketch) of a Truth-Only Logic uses no Type Theory (only some Ordering) and in the light of the above brief considerations, that seems like a good starting point.
TRUTH
) and many composing and ordered Truths: TRUTH :df {T0, T1, T2, ..., Tn}
. Falsehood is trivially mapped to T0
and Boolean True to Tn
.T
can be its own (proper) subtype seems to be usually implied in contexts of Liskov Substitution (noting that Liskov Substitution appears to be compatible with the rule that for every T: T < T
), we observe TRUTH
and Tm | Tm ∈ TRUTH
are distinctive Entities and Types (if were to force a Typology or Typing scheme).Previously, we considered Truth as a rather one-dimensional kind of thing - ordered along one dimension of consideration.
T
, F
, NTF
. It's also common practice to consider the relationship between distinctive Truth, Falsity, and any third Truth Values as Lattices.) On such an approach Truth is identified with the Lattice (or Graph for that matter) not a Vertex, Node, Edge, etc.