Words 
Explained in 
Comment 
Mathematics ; mathematical logic 
1.1 
wikipedia mathematical logic 
theory 
1.1, 1.3, 1.A 
Ref 
content / components of a theory 
1.1, 1.3 
My own words. Wikipedia did not seem to notice that a theory is more than a set of axioms, or a set of statements (axioms and theorems). 
system 
1.1, 1.3, 1.4, 3.1, 3.2 
= a set with structures, interpreting given
types and structure symbols. Could not call this its officially name of structure which I left to its other standard meaning which sounds better. 
model 
1.1, 1.A 
= interpretation of a theory. See also (Mod, Tru) in 4.8 
model theory 
1.1, 1.31.7, 1.9... 
ref 
foundation, primitive 
1.1 
Ref : wikipedia Primitive notion 
development 
1.1, 1.3, 4.8, 4.9 
Did not find this concept made explicit
elsewhere. 
axiom 
1.1, 1.3, 1.5, 1.10, 1.A 
Ref axiom  axiomatic system 
statement 
1.1, 1.5, 1.9  The syntactic difference (1.9) making them
not particular formulas seems original, the special syntax
of binders in set theory (1.8) being absent from traditional
presentations (ZF). 
set theory 
1.11.4, 1.7, 1.8, 1.10... 
Usually meant as only accepting sets, or sets and urelements, or sets and classes. Not found elsewhere primitively accepting functions (nor under any other name). 
theorem, proof, provable, proof theory, (in)consistent 
1.1, 1.6, 1.9, 1.F, 4.6, 5.7 
see also "refutation". Ref proof theory  consistency 
logical framework 
1.1, 1.3, 1.A  This concept is of course crucial but not
named elsewhere this way, maybe not any other way, but
specific ones are named by the word "logic" with adjectives. 
constant (symbol) 
1.2, 1.4  Ref  mathworld. Also called individual constant 
value (of a variable) 
1.2  
variable (symbol) 
1.2, 1.5, 4.1  
fixed variable 
1.2, 1.3 

free variable bound variable 
1.2, 1.8 
Ref: wikipedia 
range ; range over 
1.2  
element 
1.2, 1.7 

urelement  1.2, 1.7  Ref;
elsewhere called atom, while the latter word
has another standard meaning 
set  1.2, 1.7, 1.E 
Original quote from Cantor in German. Reference in English  Reference with both languages 
function, argument, domain, value of a function  1.2, 1.10 
ref 
functor 
1.2, 1.4, 1.D, 1.E 
Not found this named elsewhere. Not the concept of functor in category theory (particular case, not named in this work but implicitly used such as in actions of categories). 
operation 
1.2, 1.10, 2.3 

arity ; nullary ; unary; binary... 
1.2 
See also: tuple, operation, relation. Ref 
notion 
1.3, 1.7 
here precisely defined in a way not seen
elsewhere 
object of a theory 
1.3  To not confuse with objects of a category. Don't know any math reference (maybe a too obvious concept to be named). Ref in philosophy 
onemodel theory 
1.3  Did not see it named nor conceived elsewhere. 
firstorder logic generic theory 
1.3  see also: model theory 
[T,M]  1.3 
only used in 1.B and 1.7; invented notation
(how else would you write that?) 
meta(notions of onemodel theory) metaobject 
1.3  Not sure if named elsewhere. (See other def for notions of set theory below) 
type (abstract type, interpreted type) 
1.3  Rarely mentioned in other works,
where it is also called sort
(other ref), but that latter word does not require them to be disjoint (see "ordersorted logic") 
Language Structure symbols 
1.3, 3.1 
List of structure symbols. Others call it "signature" or "vocabulary", while including in the "language" all symbols beyond structures, or even the whole range of expressions. 
Structures 
1.3, 1.4 
here only firstorder structures (operators and predicates) 
secondorder structures 
(1.4) 5.1  Coined this phrase 
interpretation (of a theory into set theory)  1.4 
Insertion in set theory = choice of a model in the universe. Ref 
generic interpretation 
1.4  Coined phrase. (Others can't imagine this as they don't believe in urelements) 
standard 
1.4, 1.D, 4.7 
The general ref (nonstandard model) is vague ; commonly used in practice for secondorder logic ("standard semantics"), arithmetic, and set theory. 
universe 
1.4, 1.D, 1.F, 5.3 
Ref wikipedia 
an article 
operator symbol type type of result 
1.4 
No standard terminology found for what I call "operator" as a model theoretical concept as opposed to "operation" or even "function" as set theoretical concept. Ref 
Boolean 
1.4 
Logicians use
this name in some ways but elsewhere call it propositional,
while in ordinary math "proposition" is synonymous with
theorem, which is different. 
paraoperator 
1.4 
I coined that name to distinguish it from "operator" in absence of any clear standard 
(logical) connective 
1.4, 1.6 
Ref 
predicate 
1.4 
Ref. 
∈  1.4, 1.7 

f(x) evaluator Dom 
1.2, 1.4 
I coined the name "evaluator" as I am not
aware of any standard name for this. 
ZF 
1.4 
I only comment it here, not use it (though it is the standard elsewhere), but only
discuss its consistency in 5.B.
See also 1.D (axiom schema of specification) 
expression, formula 
1.5 
This definition of "expression" as "term or
formula" just seems to be an implicit
standard. 
term, occurrence, root  1.5, 4.1 
Ref for "term". I lost the ref for "root" and failed to find one by google though it appeared standard somewhere. Somehow here. 
binder  1.5, 1.8  I coined it, for what seems to be elsewhere
called "Variablebinding operator" as I give "operator"
another meaning and cannot see how else to do. 
equality = 
1.5 
see below "axioms of equality" 
logical symbols 
1.5 
called elsewhere logical constant 
type of an expression 
1.5 

variable structure 
1.5 

definition, abbreviation 
1.5, 4.8 

parameter 
1.5 
see also : constructions 
invariant  1.5, 3.1, 3.3, 3.6, 4.8, 5.1 
This conception (1.5) seems unrelated with the official one but
these are deeply related concepts as explained later. 
ground 
1.5 
Ref. 
tautology logically valid formula Boolean algebra 
1.6 
Ref: tautology  logical validity  Boolean algebra 
⇔ , ¬ , ≠ , ∉, ⇎ 
1.6 
equivalent, not (negation), different, not in, inequivalent (exclusive or) 
∧ , ∨  1.6 
conjunction, disjunction (all connectives can be found on wikipedia) 
implication ⇒ necessary condition sufficient condition contrapositive, converse 
1.6 
I took the notation ⇒ from the French, though it seems written → in English. Wikipedia looks funny, claiming that ⇒ is used for logical consequence while not actually using it there (seems that calling "logical consequence" A⇒B just means "(A→B) is logically valid", which I see no point to give a special notation for). 
∴  1.6 
Therefore. This notation seems standard but I
only found it in lists of html symbols, not in math texts. Wikipedia says it only serves as natural language abbreviation, while I use it in formulas as synonym of ∧ (but not of ⇒). 
chain of conjunctions chain of disjunctions chain of implications 
1.6 
Did not see these officially declared
elsewhere though they are so much needed. 
⊢ refutation, refutable, decidable, lemma, proposition, corollary 
1.6 
see also "theorem" 
meta(notions of set theory)  1.7 

relation 
1.8, 2.1, 2.3 
ref 
axioms of equality 
1.9 
References : wikibooks
 Encyclopedia
of math. Used in 4.6 (proof of the completeness
theorem) 