A. Phase I Errors that halt further grammatical processing:

- Input Provable Logic Statement Type Code (i.e. "
`|-`

"'s) grammar parameter does not match any defined Constant.

- Duplicate input Provable Logic Statement Type Code grammar parameters.

- Variable Hypothesis defined with Provable Logic Statement Type Code
`. Disallowing these "Meta-Metamathematical" variables appears, unfortunately, to be necessary to prevent Type Conversion Rules from/to Provable Logic Statement Type Codes and non-Provable Logic Statement Type Codes, not to mention the problems associated with somehow defining "Syntax Axioms" for the "|-" Type Code. This really goes to the heart of the difference between Grammatical and Proof parse trees. Which is not to say the Meta-metamathematical logic cannot be done, but that the grammars cannot be mixed -- at least, not with this algorithm. If desired, a Meta-metamathematical Provable Logic Statement Type code, such as "||-", instead of "|-", but still, the two could not be mixed in the same Metamath database while also using variables for "|-" and treating "|-" as a Provable Logic Statement Type code.`

- A maximum of one Provable Logic Statement Type Codes may be
used (to simplify things a little...the code is in there for multiples
but only one input parameter value is allowed, at this time.)

- A maximum of one Logical Statement Type Code may be used (to simplify things a little...the code is in there for multiples but only one input parameter value is allowed, at this time.)
- Input Logical Type Code (i.e. "
`wff`

") grammar parameter does not match any defined Constant.

- Duplicate input Logical Type Codes parameters.

- A Logical Type Code duplicates a Provable Logic Statement Type Code, either one of the input Provable Logic Statement Type Codes or, if none were given, then the default Type Code ("|-").
- NOTE:
In theory, there may be no Variable Hypotheses defined for a Logical
Type Code. This would be the case if there were other Type Codes
convertible into a Logical Type Code; thus, there could be "wffn" and
"wffx" that convert to "wff". This is not automatically an error even
though it contradicts normal Metamath practice.

- Syntax Axiom Expression is a duplicate of a previous GrammarRule Expression. This would mean that the entire Syntax Axiom would be dropped from the Grammar and would have no effect, which is clearly a significant, reportable error.
- Syntax
Axiom Expression -- or other Formula's expression -- contains a Constant that is used
elsewhere as a Type Code, which includes the set of Variable Type
Codes, Syntax Axiom Type Codes, Logic Statment Type Codes and Provable
Logic Statement Type Codes. This restriction facilitates
creation of a Context Free Grammar from the user's Metamath database by
guaranteeing that the left hand of each "production rule" is not a
"terminal". See http://en.wikipedia.org/wiki/Context-free_grammar

- Syntax Axiom has Disjoint Variable Restriction(s). Note: Syntax
Axioms are, by definition, those Axioms with Type Code not equal to one
of the Provable Logic Statement Type Codes (i.e. "|-"). Thus, either the Syntax Axiom
has an error or the user needs to change the input Grammar Formual Type
Code parameter.

- Syntax Axiom has in-scope Logical Hypothesis.
- Syntax Axiom contains more than one occurrence of the same variable.

- NOTE:
#12 is still under debate -- Nulls Permitted Rules can also generate
Constant Expressions that fit this pattern, and it also appears that
the general problem of proving unambiguousness is way more involved
than can be handled with just a few haphazard restrictions like this...) Syntax Axiom Expression which contains only Constant Symbols (a
Constant Syntax Axiom) has more than one Constant (i.e. 2) and at least
one of those Constants appears in another Syntax Axiom. This
restriction is added not because of theoretical considerations but
because of the additional complexities these constructions bring --
which are beyond what MMJ2 desires to accomodate at this time. Gnarly
problems can result because Named Typed Constants have a mixture of
properties: they are Constants and they substitute for Variables. See
Example #5 in EssentialAmbiguityExamples.html

B. Phase II Errors that halt further grammatical processing:

- Type
Conversion Rule converts Provable Logic Statement Type Code to a
non-Provable Logic Statement Type Code. Note that previous Validation
Error #3, and the method of distinguishing Syntax Axioms from Logical
Statement Axioms should preclude this situation from occuring without
detection; in other words, another error should be reported before
validation even gets to #13.

- Type Conversion Rule creates a loop, either direct or indirect. Example of direct is "
`error1 $a wff ph $.`

", which converts "`wff`

" to "`wff`

". An example of indirect is "`cv $a class x $.`

" + "`error2 $a set A $`

" which converts "`class`

" to "`set`

", but "`cv`

" already converts "`set`

" to "`class`

", thus setting up a loop from "`class`

" to "`class`

" (and "`set`

" to "`set`

".) - A Notation Rule's Expression is a duplicate of another Grammar Rule's expression and the Type Code of the Notation Rule's "base" Syntax Axiom differs from the Grammar Rule's base Syntax Axiom's Type Code. Duplicate Expressions with different associated Type Codes is not a "redundancy" that can be simply ignored, as is the case with "overloading" (ex. "weq" and "wceq" in set.mm.) Each unique Expression must have a unique Type Code. If that is not the case then that means that error A.7 above wasn't invoked, and therefore, a Type Conversion Rule(s) or Nulls Permitted Rule(s) operated on a Syntax Axiom and generated an expression duplicating another Syntax Axiom's rule Expression where those two Syntax Axioms have different Type Codes -- but at a more basic level it means that a given symbol sequence has more than one interpretation, and is inherently Ambiguous.

Y. Consolidated List of Grammatical Validation WARNINGS (Informational Messages)

- The size of the set of Syntax Axiom Type Codes is not equal
to the size of the set of Variable Hypothesis Type Codes. This is a
"warning" that indicates that either a) there is a Variable Hypothesis
Type Code that has no Syntax Defintion (and can therefore be
defined-away as unnecessary -- like "set" in set.mm), or b) there is a
Syntax Axiom with a Type Code that has no matching Variable Hypotheses,
perhaps indicating that the file is incomplete or that the input
parameters providing non-default Provable Logic Statement Type Codes
and Logical Statement Type Codes are in error.

- GrammarRule is parseable using other Grammar Rules.
This means that it is a composite or there is some sort of ambiguity in
the grammar (???). Although it is a clear error, it does not "stop the
show" and is reported as an "Info Message", a Warning in other words
(this edit is distinct from the prohibition on duplicates, which is
sacred, cannot be violated and is treated as a real "error"). Note: we
also treat ambiguous non-grammar statements as "informational" /
warnings, not hard errors.

Z. Consolidated List of Other Validations (for future reference...)

- Theorem Statement ($p aka "Provable Assertion") has Type Code that does
not match one of the user input Provable Logic Statement Codes. WOOPS -- THIS
SHOULD BE ALLOWED, FOR EXAMPLE, wel is provable as a _theorem_
from wcel: wel-theorem $p wff x e. y $= vx cv vy cv wcel $.