Here is my understanding of the definition checker: The $a-statement <label> with typecode |- passes the test if and only if it respects the following five rules. Rule 1: <label> should be a biconditional or an equality (i.e. its root-symbol should be <-> or =). If <label> passes Rule 1, then we can define its definiendum as its LHS and its definiens as its RHS. We define the *defined symbol* as the root-symbol of the LHS. We define a *dummy variable* as a variable occurring in the RHS but not in the LHS. Rule 2: The defined symbol should not occur in an earlier $a-statement with typecode |- or in another place in <label>. Rule 3: No two variables occurring in the LHS should share a DV condition. Rule 4: All dummy variables are required to be disjoint from any other (dummy or not) variable occurring in <label>. Rule 5: If X is a dummy variable, then there should be an earlier justification theorem (I presume this justification theorem is a biconditional (resp. equality) with on the LHS the definiens and on the RHS the definiens with X replaced by some Y of the same type), or, the definition checker should be able to automatically generate one.
Remarks: * The "root-symbol" is the root of the considered tree; it need not correspond to a single token in the database (e.g. w3o or wsb). * "DV" stands for "disjoint variable". * I think that Rule 3 is not necessary. It's true that a definition not satisfying Rule 3 is a bit strange, but Rules 1,2,4,5 seem to suffice for conservativity and eliminability. * In the mmj2 implementation, Rule 5 is actually decomposed into two rules (5 and 6) according to whether X is of type setvar or not. If not, then the definition checker will not try to generate a justification theorem (so there better be one in the database), and if it is of type setvar, then the definition checker, if there is no justification theorem in the database, will try to generate one of the form "|- F/ x definiens" (actually, "|- ( definiens -> A. x definiens )"). * Note that because of Rule 5, "passing the test" may actually depend on the effectiveness of the algorithm trying to generate a justification theorem. * By the way, are there in set.mm any non-setvar dummy variables ? An example would be "df-nul2 $a |- () = ( A \ A ) $." or the former definition ~dftru2 of T. Actually, any non-setvar dummy variable could be replaced by _V (or (/)) or T. (or F.) depending on their type. Benoit -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/cf84497b-b132-473d-9af7-b912cd75e1a1%40googlegroups.com.
