Classical Logic

[John Tang Boyland]

Certain limited use of classical logic can be accepted in SASyLF.

[John Tang Boyland]

For infinite syntax, I think we can create a bijection to the natural numbers.
This will permit an "unequality" relation that should be standard,
along with an equality relation and proofs of disjointness.

So every new nonterminal N would generate judgments N = N and N ≠ N' where the latter judgment is equivalent to "not N = N" (see later topic).

[John Tang Boyland]

For judgments, some judgments can be negated. See [discussion:extensions/Negation]