Words 
Explained in 
Comment 
Mathematics ; mathematical logic 
1.1 
wikipedia mathematical logic 
theory 
1.1, 1.3, 1.9 
Ref 
content / components of a theory 
1.1, 1.3 
My own words. Wikipedia authors (thus their
references) missed the fact 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.2, 3.3 
= 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 usual meaning which sounds better. 
Model 
1.1, 1.9, 1.10 
= interpretation of a theory (1.3). See also (Mod, Tru) in 4.10 
Model theory 
1.1, 1.31.7, 1.9, 1.10... 
ref 
Foundation 
1.1 

Primitive (component) 
1.1 
Ref : wikipedia Primitive notion 
Development 
1.1, 1.3, 1.4, 1.D, 4.10 
Either a proof, a definition or a construction. Did not find this concept made explicit elsewhere. Used in 1.A. 
Definition, abbreviation 
1.1, 1.5, 4.10 

Construction 
1.D, 2.2, 2.B, 4.11 

Axiom Statement 
1.1, 1.3, 1.9, 1.10, 1.11, 2.1 
Ref axiom  axiomatic
system. The syntactic difference between set
theoretical statements and ground formulas (2.1), due to the special syntax of binders in set theory (1.8) is not common in basic textbooks. 
Set theory 
1.11.4, 1.7, 1.8, 1.B, 2... 
Usually considered as only accepting sets, or
sets and urelements, or sets and classes; I did not see it elsewhere considered (nor under any other name of theory) as primitively accepting functions as I did. 
Theorem, proof, provable, proof theory, (in)consistent 
1.1, 1.9, 1.10, 1.C, 4.7 
see also "refutation". Ref proof theory  consistency 
Logical framework 
1.1, 1.3, 1.9  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 

Vree 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
usual meaning 
set  1.2, 1.7, 1.B, 2.2, 2.B 
Original quote from Cantor in German. Ref. in English  Ref. with both languages 
Function, argument, domain, value of a function 
1.2, 2.1  ref 
functor 
1.2, 1.4, 1.8 
= unary operator = metaobject like a
function but whose domain is a class. 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). See "structure" and "class". 
Operation 
1.2, 2.3, 2.7 

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). objects in philosophy  mathematical object 
Onemodel theory 1MT, MT 
1.3, 1.A  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.A and 1.B; 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.2 
List of structure symbols. Others call it "signature"
or "vocabulary", while including in the "language" all symbols beyond structures, or even all expressions. 
Structures 
1.3, 1.4 
here only firstorder structures (operators
and predicates) 
Interpretation  1.3, 4.1 
Insertion in set theory = choice of a model in the universe. Ref 
Generic interpretation 
1.3  Coined phrase. (Other authors couln't imagine
this concept as they don't believe in urelements) 
Standard 
1.3,
1.7, 1.9, (1.11), 1.B, (1.C, 1.D), 2.A, 4.9 
The general ref (nonstandard
model) is vague ; commonly used in practice for secondorder logic ("standard semantics"), arithmetic, and set theory. 
Universe 
1.3, 1.D, 2.A, 2.B, 5.3 
Ref wikipedia
 an article 
Operator symbol type type of result 
1.4 
No usual 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 usual convention 
(logical) connective 
1.4, 1.6 
Ref 
predicate 
1.4 
Ref. 
∈ (membership predicate)  1.4, 1.7, 2.2  to not confuse with the use of ∈ as part of notations of binders 
Evaluator f(x) Domain functor Dom 
1.2, 1.4, 1.D, 2.2, 2.3 
I coined the name "evaluator" as I am not
aware of any official name for this. 
ZF 
1.4, 1.A, 2.7 
here only commented, not used (though it is
the norm
elsewhere) ; its consistency
is discussed in 5.B. 
expression, formula 
1.5 
This definition of "expression" as "term or
formula" seems to be usual. 
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 normal 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. 
(axioms of) equality = 
1.5, 1.11 
Ref : wikibooks
 Encyclopedia
of math. See also 2.9 (equivalence relations). Used in
4.7 (proof of the completeness theorem). 
logical symbols 
1.5 
called elsewhere logical constant 
type of an expression 
1.5 

variable structure Second order 
1.5, 1.11, 5  
parameter 
1.5 
see also : constructions 
invariant  1.5, 3.2, 3.4, 3.7, 4.10, 5.1 
This concept (1.5) is not the so
officially called one, but both are deeply related as
explained later. 
tautology Boolean algebra 
1.6 
Ref: tautology  Boolean algebra. See also : logically valid formula (logical validity) 
⇔ , ¬ , ≠ , ∉, ⇎ 
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 funnily claims 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. I only found this notation 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. 
class, subclass  1.7  see also "subset" (1.8), and "inclusion". 
meta(notions of set theory)  1.7, 1.D 

Set, Fnc  1.7  (predicate symbols) 
definite, d  1.7  Notation coined in lack of external references 
Setbuilder, subset { ∈  } 
1.8, 2.2  also written { :  } in Z notation.
Shortened from the traditional phrase "Setbuilder
notation". What the heck is a "notation" : a notation for what ? Wikipedia remains strangely silent about anything in common between quantifiers, setbuilder notation and the concept of bound variable... 
Russell's paradox  1.8  Famously discovered by Bertrand Russell in
1901 and written in a letter to Frege in 1902, though also discovered by Zermelo in 1899 without being published. Initially served to refute (show inconsistent) some candidate formalizations of set theory. Ref 
definer ( ∋ ↦ ) 
1.8, 1.D, 2.1, 2.2, 2.3 
Coined these name and syntax of use, modified
from the common style of use of ↦ which lacked any clear and coherent logical status. (Proper format and terminology are missing in usual conventions under the excuse of not accepting functions as primitive objects in ZF set theory...) 
relation 
1.8, 2.3, 2.7 
ref 
ground 
1.9 
Ref. 
logically valid formula  1.9 
Ref: logical validity 
⊨, ⊢, refutation, refutable, decidable, contradiction, lemma, proposition, corollary 
1.9 
see also "theorem" 
sound, soundness  1.9  qualifies the proof theorical part of a
logical framework (see also FOTsound, wich is
different). 
Complete (framework) Completeness theorem 
1.1,1.9, 1.10, 4.7, 1.B, 1.C 
Qualifies the proof theoretical part of a logical framework. 
quantifier ∀(universal) ∃(existential) Existential Introduction Existential Elimination Universal Introduction Universal Elimination 
1.10  
Open quantifiers Bounded quantifiers Bounded formula 
1.10, 1.B, 1.C  See also 1.A (specification schema) also discussed in 2.1, 2.2, 2.A, 2.B 
inclusion (between classes)  1.10  See also "subclass", and ⊂ for sets 
Schema (of statements)  1.11  
Complete (theory)  1.11  
Arithmetic Z_{1} = First order arithmetic 
1.11, 1.A, 4.4, 4.5 
See also wikipedia 
Reflexive (reflexivity) Symmetric (symmetry) Transitive (transitivity) 
1.11, 2.9  Properties of relations. There are similar but different concepts taking those names : refexive sets (2.A), transitive sets (5.4). 
TT = Theory theory 1TT = Onetheory theory (Systems theory) 
1.A 

strength (order) 
1.A, 1.C, 2.C  
Strengthening axioms 
1.A  
Axiom of Infinity  1.A, 4.4, 4,6 

Specification (axioms schema)  1.A  
FOT = finite objects theory FST = finite set theory 
1.A 
Ref: On
Interpretations of Arithmetic and Set Theory by
Richard Kaye and Tin Lok Wong 
Mc Lane set theory Zermelo set theory 
1.A 
Ref : Wikipedia 
⌜ ⌝ Quote  1.B 
Ref : Quasiquotation 
pseudofinite  1.B, 4.9  as opposed to "truly finite". See also : standard / nonstandard 
truth predicate properties (of models) 
1.B  
FOTsound 
1.C 
traditionally called arithmetical
soundness 
Existential (formula, statement, class) Algorithmically defined (class) 
1.C  Elsewhere called Σ_{1} (Lévy
hierarchy) and more precisely Σ^{0}_{1}
(Arithmetical
hierarchy). 
Incompleteness theorems  1.C  Fully proven in 5.7 
Unified framework  1.D  did not find this explanation elsewhere 
Technical axioms (of set theory) Axiom of Extensionality 
2.1  
⊂ Inclusion (between sets) 
2.1  See also "inclusion" for classes 
Set generation principle  2.2  not seen elsewhere 
⋃ (union of a set of set) 
2.2  
Image Im 
2.2  
Target set 
2.2 
usually called codomain or set of
destination 
empty set ∅ empty function ∅_{↦} 
2.2  
singleton {x} pair {x, y} 
2.2  
f : E ↠ F surjectivity, surjection 
2.2  
currying  2.3  ref wikipedia 
tuple ordered pair ( , ) triple ( , , ) quadruple ( , , , ) 
2.3  
projections π_{0}, π_{1} 
2.3  tuples evaluators 
projections π_{i} index notation 
2.3, 2.5  curried evaluator of families 
V_{n}  2.3  Set of n numbers from 0 to n−1
(my own notation, didn't find one from elsewhere) 
∃^{≥2} ! ∃! 
2.4  I added the bare uniqueness quantifier ! and
the short notations !: and ∃!: for sets (not found in the literature) 
℩  2.4, 2.6, 2.8 
inverted iota, first introduced by Peano,
then extended beyond our use, first as Russell's binder of "definite description operator", then as Hilbert's ϵ operator. Ref 1  2 
Conditional connective Conditional operator ( ? : ) 
2.4  I did not see any name or notation for this
in other math texts, which afaik only use it presenting
arguments in separate lines, and with words: (... if ..., (... otherwise 
family  2.5  
extensional definition{ , , } 
2.5  general notation which includes the notations
of singleton and pair as particular cases 
{  ∈ } {  ∈ ∧ } 
2.5  Completes our short list of legitimate uses
of the { } signs after the set builder and the extensional
definition. (Many other authors fail to distinguish such a list, as they may start with a general notation which may be nonsense.) 
constant function  2.5  
∁_{E} complement \ difference ∩ intersection ∆ symmetric difference 
2.5  
gr (class of graphs) ^{t} transpose domain, image of a graph 
2.6  
R⃗ , R⃖ 
2.6 
Curried presentations of a graph, for which I
do not know any notation from other authors 
Gr, functional graph, ℩R⃗  2.6  
fiber, f_{•}  2.6  from elements to sets; usually denoted f^{
1} like for the preimages of sets (from sets to
sets) and the inverses of bijections (from elements to
elements), which I consider incoherent. 
disjoint ∐ (sum of sets, or disjoint union) 
2.6  
R^{⋆} direct image R_{⋆} inverse image, preimage (by a relation) 
2.6  I switched up and down positions of the star
compared to the star
notation sometimes used by others. I took this difficult decision for coherence with the notation of exponentiation, to allow for notations of actions and coactions of categories compatible with both (3.6) 
f[A] = f^{⋆}(A)
direct image f_{⋆}(B) preimage 
2.6  of sets by functions. Special case of preimages by graphs (the graphs of those functions). The same notation f_{⋆} is abusively also used for preimages of relations by functions (2.9). 
× (cartesian) product ∏ product (binder) Powerset ℘ Exponentiation F^{E} 
2.7  between sets 
Cantor's Theorem  2.7  usually expressed in terms of cardinality. Ref wikipedia 
⚬ composition  2.8 

f_{A}  2.8 
restriction of a function f to a set
A 
Inj, ↪, injection f^{ 1} inverse 
2.8 

⥬ canonical ⇌ bicanonical 
2.8 
The literature mentions specific "canonical
bijections" without any general definition or notation. 
natural injections ∐ sum of functions 
2.8 

⊓ product of functions  2.8 
The
literature denotes 〈 , 〉 for products of two
functions, and similarly 〈 , .. , 〉 for finitary ones, but offers no notation for the binder; we also use ⊓ over already formed families of functions, to which the notation 〈 , 〉 cannot adapt. To not confuse with another product of functions using the notation × (which defines products of actions, 3.10) 
E^{2} 
2.9 
Cartesian square 
preimage (of a relation by a function) 
2.9  
Product (of relations) 
2.9  
irreflexive antisymmetric 
2.9 

Preorder, order Comparable elements Strict, total order 
2.9 

Equivalence relation ∼_{f} Class of an element by an equivalence relation 
2.9 

h/f Quotient h/R 
2.9 
between 2 functions, or of a function by an equivalence relation ; I did not see names or notations for this in the literature, which only calls "quotient of a function f" the quotient set (Dom f)/∼_{f} = Im f_{•}. 
Partition E/R Quotient 
2.9 
quotient of a set by an equivalence relation (widespread name and notation) 
AC_{X} AC 
2.10 
While AC is very famous, the expression of AC_{X} does not appear in Wikipedia, except for the special
case of the axiom of countable choice 
Fixed point Idempotent (function) 
3.1 

monotone antitone strictly monotone strictly antitone 
3.1 













Secondorder structures 
(1.4) 5.1  Coined this phrase 