Module prop::sd

Symbolic Distinction

This model is derived from HOOO EP.

When one expresses a == b in logic, there is no way to prove that a and b are symbolic distinct, although they are equal. This is because logic treats symbols and values as the same mathematical objects.

However, it is possible to prove that a is not symbolic distinct from a (not_sd). Furthermore, it is possible to prove that false^(a == b) implies symbolic distinction (para_eq_to_sd).

Symbolic Distinction Sd is defined as:

sd(a, b) := ◇(¬(a == b))

It means, two values are symbolic distinct when it is possible that they are not equal. This is the closest expression in logic that corresponds to symbolic distinction. The definition is based on what can be proved about symbolic distinction.

This logical definition is not what symbolic distinction means in natural language. Symbolic distinction in natural language uses knowledge about symbolic reasoning that is not accessible within logic, since natural language can reflect upon the symbolic level of abstraction as separated from value level of abstraction.

For example, a can never be not equal to a, so one can prove ¬sd(a, a).

On the other hand, if we say a can never be not equal to b, so one can prove ¬sd(a, b), then this is provable if (a == b)^true (tauto_eq_to_nsd). This is because it is not possible for a and b to be not equal to each other. Yet, this is not the same as when reasoning about symbolic distinction, because everybody can tell a is obviously symbolic distinct from b.

Symbolic Distinction is a valid extension of normal logic to reason about symbolic knowledge. An important property of Symbolic Distinction is that logical reasoning about symbolic distinction is limited. The logical reasoning is only sound, that is overlapping with reasoning about symbolic distinction in natural language, when one talks about: Symbolic Distinction.

If this sounds confusing, then remember you are not the only one who get confused by this. The trick is that Symbolic Indistinction is unsound, because if one symbol is not equal to another symbol and yet they are symbolic indistinct, then reasoning is unsound. Under Symbolic Distiction, however, there is no such case where reasoning is unsound. For more information, see paper.

This leads to a case where one can use Symbolic Distinction as a “one sided” theory. The theory has no “other side”, kind of like a Möbius strip. It is sound to introduce new operators to logic which semantics depend on Symbolic Distinction.

In Path Semantics, this is leveraged to lift a == b into a ~~ b when a and b are symbolic distinct (lift_q). This proof relies on the axiom hooo::lift_q which lifts a == b into a ~~ b when there is a theory(a == b).

A theory of equality means that a == b is not provable without making any assumptions and that one can not prove false from a == b. Theory of equality implies symbolic distinction. This is similar to how false^(a == b) implies symbolic distinction, but here one can prove false from a == b. Theory of equality is another way of getting symbolic distinction.

Think about theory(a == b) as saying that a == b is not entirely true, but it is not entirely false either. It depends on the situation under which circumstances a == b is true. From theory(a == b) one can not say which circumstances makes a == b true. One can only deduce that there are some circumstances, but one does not know which circumstances.

Motivation for Symbolic Distinction

In Martin-Löf Type Theory for dependent types, there is a formation rule for reflexivity of the identity type:

A : type(n), a : A |- refl{A} : Id{A}(a, a)

The reflexivity proof is constructive and it requires a well formed type judgement a : A.

Now, one might think that reflexivity is something that is tautologically true, but it is not! Although one can prove (a == a)^true in IPL with HOOO EP, this is not sound as reflexivity in Martin-Löf Type Theory because one must first prove the left side of the turnstile |-. This is necessary to show that the reflexivity proof of identity types is well formed.

This means, there are many circumstances in mathematics where one does not wish to have tautological reflexivity, but more like an intentional equality. An intentional equality is when one has a == b, but they are “made equal” on purpose. This can be expressed in HOOO EP as theory(a == b). The problem with theory(a == b) is that it lacks equivalence properties. This problem is solved by lifting a == b into a ~~ b by theory(a == b). Path semantical quality a ~~ b is a partial equivalence operator, which is total locally. So, once you have a ~~ b you can prove a ~~ a. As a result, Path Semantics can model loops around any proposition with the quality operator, by viewing it as a space of paths. The idea is to bootstrap mathematics from a lower level than Martin-Löf Type Theory.

Functions

• in_left_arg
  sd(a, b) ⋀ (a == c)^true => sd(c, b).
• in_right_arg
  sd(a, b) ⋀ (b == c)^true => sd(a, c).
• lift_q
  (a == b) ⋀ sd(a, b) => (a ~~ b).
• not_left
  sd(¬a, a).
• not_right
  sd(a, ¬a).
• not_sd
  ¬sd(a, a).
• para_eq_to_sd
  false^(a == b) => sd(a, b).
• symmetry
  sd(a, b) => sd(b, a).
• tauto_eq_to_nsd
  (a == b)^true => ¬sd(a, b).
• to_eqq
  sd(a, b) => ((a == b) => (a ~~ b)).
• to_not_tauto_eq
  sd(a, b) => ¬((a == b)^true).

Type Definitions

• Sd
  sd(a, b) := ◇(¬(a == b)).