|Mathematics ; mathematical logic
||1.1, 1.3, 1.A
||1.1, 1.3, 1.4,
| = a set with structures, interpreting given
types and symbols.
Could not call this its officially name of structure which I left to its other standard meaning which sounds better.
|| = interpretation of a theory.
See also (Mod, Tru) in 4.8
|content / components of a theory
||Ref : wikipedia Primitive notion
||1.1, 1.3, 4.8, 4.9
||Did not find this concept made explicit
||1.1, 1.3, 1.5,
||1.1, 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
|theorem, proof, provable,
proof theory, (in)consistent
|1.1, 1.6, 1.9,
1.F, 4.6, 5.7
|see also "refutation"
|value (of a variable)
||1.2, 1.5, 4.1|
|range ; range over
|pure element||1.2, 1.7||elsewhere called urelement or atom, while
the latter word has another
|set||1.2, 1.7, 1.E
|function, argument, domain||1.2, 1.10
|value of a function
|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
||1.4, 1.10, 2.3
|arity ; nullary ; unary; binary...
||See also: tuple, operation, relation
||here precisely defined in a way not seen
|object of a theory
||1.3||to not confuse with objects of a category
||1.3||Did not see it named nor conceived elsewhere.
||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.
|1.3||see also: model theory
||only used in 1.B and 1.7; invented notation
(how else would you write that?)
|meta-(notions of one-model theory)
|meta-(notions of set theory)||1.7
|type (abstract type,
|1.3||Hardly ever mentioned in the math literature,
where it is also called sort,
but that latter word does not require them to be disjoint
(see "order-sorted logic")
||= list of structure symbols|
||here only first-order structures : operators
|interpretation (of a theory into set theory)||1.3
||designates a model in the universe
||1.3||I coined that name
||1.3, 1.D, 4.7
||1.3, 1.D, 1.F, 5.3
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
||I coined the name "evaluator" as I am not
aware of any standard name for this.
||Only commented here, not described nor used.
See also 1.D (specification) and 5.B
|ground, expression, formula
||This definition of "expression" as "term or
formula" just seems to be an implicit
|term, occurrence, root||1.5, 4.1
|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.
||see also : constructions
|invariant||1.5, 3.1, 3.3,
3.6, 4.8, 5.1
logically valid formula
|⇔ , ¬ , ≠ , ∉, ⇎
||equivalent, not (negation), different, not in, inequivalent (exclusive or)|
|∧ , ∨||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
||Did not see these officially declared
elsewhere though they are so much needed.
refutation, refutable, decidable,
lemma, proposition, corollary
||see also "theorem"
|axioms of equality
||References : wikibooks
of math. Used in 4.6 (proof of the completeness