MMJ Name (Abbreviation Usage) 
MetaMath.pdf Name/Standard Usage 
MObj 
Math Object, parent class of Sym and Stmt. Created only because in a few places unrelated to the "core" lang processing, it is convenient to be able to hold an array or collection containing a mixture of Sym's and Stmt's. The database sequence numbe, "seq" is now stored in MObj. In theory, new objects that might be added later to enable persistent storage of the LogicalSystem object might be added as subclasses of MObj (example, Scope, for one.) 
Sym 
Math Symbol 
Cnst 
Constant (aka $c) (Note: "const" is a Java keyword and "con" is a device name.) 
Var 
Variable (aka $v) 
varHypArray 
Internally
computed, provides
the unique variable hypotheses referenced in an assertion's
expression (it is a processing byproduct that is saved for later use.)
The variable hypotheses are stored in the array in order of their
appearance in the database  i.e., by seq. Example: ax1 expression "( ph > ( ps > ph ) )" has 2 unique variable hypotheses, named, "wph" and "wps" in set.mm. 
Expr 
Expression. Refers to the 2nd through "n"th Sym's in a Formula. May be of zero length itself. 
ExprRPN 
Reverse Polish Notation version
of expression, if it exists (it is assumed in MMJ that identification
of "syntax constructors" such as "wi" and "wn" axiomatic assertions
will enable automatic conversion of Expr's to ExprRPN's.) These RPN
versions are further differentiated by content: they refer only to
labels! For example, theorem "id" would be expressed in RPN as "wph wph
wi"; this embeds variable type information in the expression and avoids
namespace ambiguity (Cnst/Var's are not guaranteed to be different than
labels.) 
Formula 
The Metamath "statement"
consisting of 1 Cnst Sym followed by 0 to m Cnst or Var Sym's. Defined
as an array of 0 to n Sym's, the Cnst at the beginning is referred to
as the Typ (type) of the statement. This class is outside of the
MObj>Sym/Stmt hierarchy and is stored as an attribute of Stmt. The
intent in separating the Formula into its own class was to facilitate
processing of formulas and expressions that are not part of a Stmt (for
example in proof verification  see mmj.verify.) 
LogicFormula 
LogicFormula is an attribute of
both LogHyp (Logical Hypothesis) and Assrt (Assertion). It is differentiated
from VarHypFormula because, although every Metamath statement can be
treated as a "Formula", VarHyp formulas consist of exact 1 Cnst Sym
followed by 1 Var Sym, and thus, the handling is different in a few
places; the other problem faced was that LogHyp is a subclass of Hyp but
contains a LogicFormula, and Assrt also contains a LogHyp. 
VarHypFormula 
Variable Hypothesis Formula. See LogicFormula. 
Syn 
Syntax, normally used in reference to Syntax Axioms and/or VerifySyntax. 
Vhe 
VariableHypothesized
Expression. This is a quirky, experimental thing derived from an
Expression: each Var in the Sym[] array is replaced by the
corresponding VarHyp for the Var in that specific Expression; the
VarHyp is *then* expanded into its component Type (a Cnst) and Var. The
Vhe and variations are used in Syntax Verification processing for
pattern matching. There are several variations for printing, sorting
and verifying. The quirkiest one of all is the MObjVhe[] which contains
a mixture of Cnst's and VarHyp's (the VarHyp's are not expanded.) Also
very quirky is the SynVhe, which stands for Syntax Axiom Vhe 
in this variation the Var is
replaced with null (the reason being that for insertion into the
SynTree the variable name is irrelevant  as it is in all Syntax
Axioms, except to establish sequence of the hypothesis in
VerifyProof. All in all, an ugly business... 
Typ 
= 1st Constant in Metamath $e, $f, $a and $p statements (i.e. statement "type code"). The first entry in the Formula Sym array. 
Opt 
Optional (note that names of
sets/lists of variables and/or disjoint variable hypotheses,
unless the name is prefixed with "Opt" it refers to Mandatory
Variables, as in Mandatory Variable Type Hypotheses.) 
Stmt 
Statement 
DjVars 
Disjoint Variable Restriction
(aka $d, note that in Frames, unless prefixed with "Opt", refers to a
Mandatory Variable Disjoint Variable Restriction) 
Hyp 
Hypothesis 
VarHyp 
Variable Type Hypothesis (aka
$f, note that in Frames, unless prefixed with "Opt", refers to
Mandatory Variable Variable Type Hypothesis) 
LogHyp 
Essential (aka $e aka "Logical") Hypothesis 
Assrt 
Assertion 
Axiom 
Axiomatic Assertion (aka $a) 
Theorem 
Provable Assertion (aka $p) 
MandFrame 
Mandatory
Frame  attribute of every Assrt, both Axiom and Theorem. Contains the
"mandatory" hypotheses and disjoint variable restrictions of the
assertion. "Mandatory" refers to variables and hypotheses used in the
assertion's own statement and logical hypotheses' statements (see
OptFrame). 
OptFrame 
Optional Frame  only Theorems
have OptFrames. Whereas Axioms have only a MandFrame, Theorems have
both MandFrame and OptFrame. OptFrame contains variable hypotheses and
disjoint variable restrictions needed for assertions referenced in the
Theorem's proof. 
1. In the 3rd column, "Abstract/NA", "NA"
means the item is not actually coded as a separate Java class but is
provided in the table as a logical entity; "Y" means that the
Class is an abstract "super" class that cannot be instantiated (turned
into a
real "object" by itself), but its properties and attributes are
inherited by its subclasses.
For example, "Assrt" is Abstract Class whose nonabstract
subclasses are AxiomaticAssrt and ProvableAssrt; an assertion must be
either an axiomatic assertion or a provable assertion, but both types
of assertion share common properties and attributes.
2. The
4th column, "Unique Key Attributes" identifies which, if any,
components of the Class comprise a unique key, whether for sorting or
for duplicate checking.
For lack of a better name, "Id" is used in several places as a key;
it is the character string that was used in the MetaMath.mm file to
define the entry. For example, the value of Id for the socalled
"turnstile" symbol is "".
MMJ Entity:Java Name (note: the *list names may not be coded as actual classes)  Relationships: "ISA" means SubClass Of "HAS" means contains "0n" means Zero to "n" occurrences. 
A b s t r a c t / NA 
Unique Key A t t r i b ______________ 
Nonkey A t t r i b _______________________ 
MObj 
Y 
int seq 

Sym  ISA MObj 
Y 
String id 

Cnst  ISA Sym 
boolean isVarTyp etc. (lots of stuff, including items created by and used by mmj.verify.Grammar.java) 

Var  ISA Sym 
boolean active VarHyp activeVarHyp 

Label  NA 
String label 

Expr 
HAS 0M Sym 
NA 
sym[1]>[n] of Formula 

ExprRPN  HAS 0M Stmt (references) 
NA 
Stmt[] exprRPN  
UnknownLabel (= "?") 
ISA Label 
NA 
(converted to null in proof table)  
Typ  HAS 1 Cnst 
NA 
sym[0] 
sym[0] of Formula 
Formula 
HAS 1 Typ HAS 1 Expr 
int cnt Sym[] sym 

VarTyp  ISA Typ 
NA 

ExprTyp  ISA Typ 
NA 

ProofStep 
HAS 01 Label HAS 01 UnknownLabel 
NA 

Proof  HAS 1M ProofStep 
NA 
Stmt[]  
DjVars  HAS 2 Var 
Var varLo Var varHi 

Stmt  ISA MObj HAS 1 Label HAS 1 Formula HAS 1 ExprRPN  Y  String label  Formula formula Stmt[] exprRPN 
Hyp  ISA Stmt  Y  boolean isActive  
VarHyp  ISA Hyp HAS 1 Var  Var var  
LogHyp  ISA Hyp HAS 1 Expr HAS 1 ExprRPN  Sym[] expr Stmt[] exprRPN VarHyp[] varHypArray  
Assrt  ISA Stmt HAS 1 Expr HAS 1 ExprRPN HAS 1 MandFrame  Y  Sym[] expr Stmt[] exprRPN VarHyp[] varHypArray MandFrame mandFrame  
Axiom  ISA Assrt  
Theorem  ISA Assrt HAS 1 Proof HAS 1 OptFrame  Stmt[] proof OptFrame optFrame  
DjVarsArray  HAS 0M DjVars 
NA 
DjVars[] djVars 

OptDjVarsArray  HAS 0M DjVars 
NA 
DjVars[] optDjVars  
HypArray  HAS 0M Hyp 
NA 
Hyp[] hypArray 

OptHypList  HAS 0M Hyp  NA  Hyp[] optHypArray  
MandFrame  HAS 1 HypArray HAS 1 DjVarsArray 
Hyp[] hypArray DjVars[] djVarsArray  
OptFrame  HAS 1 OptHypArray HAS 1 OptDjVarsArray  Hyp[] optHypArray DjVars[] optDjVarsArray  
=================== (OTHER) CONTENTS OF "LogicalSystem.java" follow: =================== 
====================== ====================== 
=== === 
=========== =========== 
======================== Notes? ======================== 
ScopeDef 
HAS ArrayList Var HAS ArrayList VarHyp HAS ArrayList LogHyp HAS ArrayList DjVars 
"active" statements in current scope 

scopeDefList 
HAS ArrayList ScopeDef 
NA 
ScopeDef definitions at a scope level (global scope = 0, followed by 1, 2, ...) 

symTbl 
HAS Map 
NA 
String Sym.id 
Map symTbl (mandatory table: keep unused symbols from garbage coll.) 
stmtTbl 
HAS Map 
NA 
String Stmt.label 
Map stmtTbl 