Index of special words and notations


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.3-1.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.1-1.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 = meta-object 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
One-model theory
1MT, MT
1.3, 1.A Did not see it named nor conceived elsewhere.
first-order 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
one-model theory)
meta-object
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 "order-sorted 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 first-order 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 (non-standard model) is vague ; commonly used in practice
for second-order 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.
para-operator
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 "Variable-binding 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
Set-builder, subset
{ ∈ | }
1.8, 2.2 also written { : | } in Z notation. Shortened from the traditional phrase "Set-builder notation".
What the heck is a "notation" : a notation for what ? Wikipedia remains strangely silent about
anything in common between quantifiers, set-builder 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 FOT-sound, 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
Z1 = 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 = One-theory 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 : Quasi-quotation
pseudo-finite 1.B, 4.9 as opposed to "truly finite". See also : standard / non-standard
truth predicate
properties (of models)
1.B
FOT-sound
1.C
traditionally called arithmetical soundness
Existential (formula,
statement, class)
Algorithmically defined (class)
1.C Elsewhere called Σ1 (Lévy hierarchy) and more precisely Σ01 (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 : EF
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
Vn 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
∪, ⋃ (union of a family of sets) 
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 co-actions 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 FE
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)
E2
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)
ACX
AC
2.10
While AC is very famous, the expression of ACX 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













Second-order structures
(1.4) 5.1 Coined this phrase

Things are running crazy as I look for references and standard terminology to define the concept of "embedding" in concrete categories. It involves a concept of "initial morphism". Usual definitions for this concept of "initial morphism" rely on the concept of "concrete category" being formalized in terms of the functor to the category of sets; therefore this concept of embedding is generalizable to the use of other functors (variants of the concept of concrete category).
https://en.wikipedia.org/wiki/Embedding
https://lup.lub.lu.se/search/ws/files/6360188/4393826.pdf
https://math.stackexchange.com/questions/3399927/intuition-behind-the-definition-of-initial-morphism-and-embedding-as-stated-in-j
https://math.stackexchange.com/questions/3311098/universal-property-of-an-embedding/3975365#3975365
(where the last, short answer is mine).
This use of the phrase "initial morphism" originally comes from the case of topology with its concept of "initial topology", generated by the pullback of the topologies by a family of respective functions to different topological spaces
https://ncatlab.org/nlab/show/weak+topology
The particular case of only one function is more trivial, as the pullback directly fits as topological structure with no need of generating something else. This function between those topological spaces is then an embedding, hence the name "initial morphism" as (almost) synonym for embedding. Now this concept of "initial morphism" for concrete categories (thus leading to the concept of "final morphism" by reversing the arrows), is re-expressible as having a particular format, that of a "universal property", a very general style of properties which has the advantage of making the thing essentially unique. But, not all authors are aware of this equivalent definition (because we need to specify relatively to what these embeddings are essentially unique, otherwise they aren't). Generally a "universal property" consists in something being formalizable as either an "initial object" or a "final object" in some other category to be specified. More precisely, our "initial morphisms" happen to be... final objects in some category. Because the universal property of "initial morphisms" is a final one, not an initial one. Now, there is also a standard description of what a "universal property" is, in some wide generality : not just that it qualifies an initial or final object of simply any other category which needs to be defined case by case, but, for any "universal property" (really ?), this other category hopefully fits some precise format for which a general description is given, in terms of..., you know what ??? these initial or final objects are re-expressed respectively as 2 concepts, abusively called in wikipedia by the same name of "universal morphisms"
https://en.wikipedia.org/wiki/Universal_property
The power of generality for these "universal morphisms" to represent "any universal property" comes from the fact their definition depends on some choice of functor, which is thus what remains to be specified for each "universal property" we can consider.
This expression in terms of "universal morphism" is explicitly given for the construction of the initial topology in Wikipedia
https://en.wikipedia.org/wiki/Initial_topology
Now the confusion of calling both "universal morphisms" is resolved elsewhere
https://renrenthehamster.wordpress.com/2017/06/28/the-basics-of-category-theory-part-5/
https://math.stackexchange.com/questions/3419119/does-initial-morphism-imply-that-the-object-in-the-domain-of-originating-functor
by calling the ones "initial morphisms" and the others "final morphisms". It even seems to have been this way in a former version of wikipedia "Universal property" before, as referred to in some pages
https://math.stackexchange.com/questions/980008/relationships-between-initial-terminal-objects-and-initial-terminal-morphisms-i
https://math.stackexchange.com/questions/941539/natural-numbers-object-via-initial-morphism
https://en.wikipedia.org/wiki/Adjoint_functors

Conclusion:
There are 2 concepts of "initial morphism", and by symmetry 2 concepts of "final morphisms". Each concept is defined by means of some functor. The "initial morphisms" for one definition relative to a given functor are particular cases of "final morphisms" for the other definition relative to a very different functor.
००੦౦০
ᐅ⊳▷▹▻
  ⵁ∅⌀
°ᴼ⁰॰⚬⚪ⵔ৹∘০०੦௦૦о໐ᴏoօ౦๐ ഠܘߋₒo