| 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 : 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 |
| 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 | |
|
∁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 |