Sometimes a judgment that doesn't assume a context and which doesn't depend on a judgment that assumes a context can be algorithmically negated. One could annotate a judgment with @HasNegation to modularly assert this fact (it can be checked). Then one can write "not ..." as a new judgment.
While it seems possible to generate the negation judgment for any judgment without a context (with combinatorial explosion), the crucial excluded-middle lemma cannot be so easily constructed; the problem being that termination cannot be proved.
Last edit: John Tang Boyland 2014-02-28
If you would like to refer to this comment somewhere else in this project, copy and paste the following link:
Requiring the @HasNegation annotation is important for modularity and to avoid expensive compilation since negation explodes (probably exponentially). We don't need to knpw all the rules of a judgment then to know whether we can negate it. It also means people don't naturally assume everything can be negated. Finally, as a side-effect., this means that implicit judgments (such as "and" judgments) cannot be negated, which is probably just as well.
If you would like to refer to this comment somewhere else in this project, copy and paste the following link:
The rules for proving a negation will be generated and hard to use in any case. So we want to allow classical-style logic that can be translated to use the generated judgment.
First of all, we want to allow a prove of a negative to do case analysis analysis on the positive (using keyword else, or some other).
Sometimes a judgment that doesn't assume a context and which doesn't depend on a judgment that assumes a context can be algorithmically negated. One could annotate a judgment with @HasNegation to modularly assert this fact (it can be checked). Then one can write "not ..." as a new judgment.
While it seems possible to generate the negation judgment for any judgment without a context (with combinatorial explosion), the crucial excluded-middle lemma cannot be so easily constructed; the problem being that termination cannot be proved.
Last edit: John Tang Boyland 2014-02-28
Requiring the @HasNegation annotation is important for modularity and to avoid expensive compilation since negation explodes (probably exponentially). We don't need to knpw all the rules of a judgment then to know whether we can negate it. It also means people don't naturally assume everything can be negated. Finally, as a side-effect., this means that implicit judgments (such as "and" judgments) cannot be negated, which is probably just as well.
The rules for proving a negation will be generated and hard to use in any case. So we want to allow classical-style logic that can be translated to use the generated judgment.
First of all, we want to allow a prove of a negative to do case analysis analysis on the positive (using keyword
else, or some other).Then, as a special case, contradiction case analysis can be used if the analysis would have no cases at all:
These would both be implemented as sugar for the following, assuming the "or" judgment extension:
The "excluded middle" justification is sugar for calling the generated lemma that the judgment and its negation partition the possibility space.
Finally, one could use "contradicition" with two arguments that would be negations of each other:
Here this is short for calling the generated lemma that the judgment is disjoint from its negation.