Index of special words and notations

Explained in
Mathematics ; mathematical logic
wikipedia mathematical logic
1.1, 1.3, 1.A
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).
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 usual meaning which sounds better.
1.1, 1.A
= interpretation of a theory.
See also (Mod, Tru) in 4.8
model theory
1.1, 1.3-1.7,
foundation, primitive
Ref : wikipedia Primitive notion
1.1, 1.3, 4.8, 4.9
Did not find this concept made explicit elsewhere.
1.1, 1.3, 1.5,
1.10, 1.A
Ref axiom - axiomatic system
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.1-1.4, 1.7,
1.8, 1.10...
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.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)
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, 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.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
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).
1.2, 1.10, 2.3

arity ; nullary ; unary; binary...
See also: tuple, operation, relation. Ref
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
1.3 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.B and 1.7; invented notation (how else would you write that?)
meta-(notions of one-model theory)
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")
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.
1.3, 1.4
here only first-order structures (operators and predicates)
second-order 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)
1.4, 1.7, 1.D, 4.7
The general ref (non-standard model) is vague ; commonly used in practice for second-order logic ("standard semantics"), arithmetic, and set theory.
1.4, 1.D, 1.F, 5.3
Ref wikipedia - an article
symbol type
type of result
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
Logicians use this name in some ways but elsewhere call it propositional, while in ordinary math "proposition" is synonymous with theorem, which is different.
I coined that name to distinguish it from "operator" in absence of any clear usual convention
(logical) connective
1.4, 1.6
1.4, 1.7
to not confuse with the use of ∈ as part of the notation of a binder
f(x) evaluator
1.2, 1.4
I coined the name "evaluator" as I am not aware of any official name for this.
I only comment it here, not use it (though it is the norm elsewhere), but only discuss its consistency in 5.B. See also 1.D (axiom schema of specification)
expression, formula
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.
equality =
see below "axioms of equality"
logical symbols
called elsewhere logical constant
type of an expression

variable structure

definition, abbreviation
1.5, 4.8

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.
logically valid formula
Boolean algebra
Ref: tautology - logical validity - Boolean algebra
⇔ , ¬ , ≠ , ∉, ⇎
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
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).
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
Did not see these officially declared elsewhere though they are so much needed.

refutation, refutable, decidable,
lemma, proposition, corollary
see also "theorem"
class, subclass 1.7 see also "subset" (1.8), and "inclusion".
pseudo-finite 1.7, 4.7 see also : standard / non-standard
meta-(notions of set theory) 1.7

Set, Fnc 1.7 (predicate symbols)
definite, d 1.7 Notation coined in lack of external references
Set-builder, subset
{ ∈ | }
1.8, 1.11 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 as a refutation of some candidate formalizations of set theory. Ref
function definer
( ∋ ↦ )
1.8, 1.10
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...)
1.8, 2.1, 2.3
structure definer 1.8

axioms of equality
References : wikibooks - Encyclopedia of math. Used in 4.6 (proof of the completeness theorem)