[bvssvni]

I want to reason hypothetically, which is why I don't use syntactic equality. I only use syntactic inequality in a very limited sense, e.g. two symbols `foo'` and `bar'` are symbolic distinct, so one can introduce `sd(foo', bar')`.

The reason is that if I have a proof `((x + x) == (2 * x))^true`, then I can treat objects as if they were definitionally equal.

When definitional equality and syntactic equality are the same, one is assuming `(!(sd(a, b)) == (a == b))^true`, which obtains a proof `!sd(a, a)` for all `a`. This destroys the property of reasoning hypothetically about exponential propositions in Path Semantics. For example, I might want to reason about what if I had `sd(a, a)`, does this imply `a ~~ a` by `q_lift : sd(a, b) & (a == b) -> (a ~~ b)`? Yes!

However, if I already have `!sd(a, a)` for all `a`, then the above reasoning would be the same absurd reasoning.

I can always assume this in order to reason about it, but I don't have to make this assumption a built-in axiom of my theory.

When assuming tautological congruence e.g. `(a == b)^true` in a context, one is not enforcing observational equality. So, it is not the same as requiring the type system to be decidable. I can also make up new notions of equivalences and guard them, e.g. not making them tautological congruent.

[JonChesterfield]

I don't follow. At a guess, my "definitional equality" is your "syntactic equality", but I can't infer what you mean by definitional. Perhaps our terminology is too different to communicate successfully.

(+ X X) is not definitionally equal to (* 2 X), for they are different definitions. Different pictures on the page. A proof that they are equivalent is not a proof that they are equal. A proof that they are equal is evidence that your proof system is unsound.

If you assume a symbol is not definitionally equal to itself, you can indeed prove false, but that doesn't seem particularly important since you cannot prove that a symbol has a different definition to itself.

[bvssvni]

Yeah, this is too imprecise. I tried to translate to your terminology, but failed.

My system uses "tautological equality" and this allows me to treat them the save way for all tautological congruent operators. Ofc, you can't treat them the same if an operator is neither normal nor tautological congruent.

Even if you have a such operator `foo'(x)` you can prove `foo'(x)`, `(foo'(x) == foo'(x))^true` or `foo'(x) == foo'(x)` etc. If this is what you are talking about, then this system supports it.