|Mathematics ; mathematical logic
||wikipedia mathematical logic|
||1.1, 1.3, 1.A
|content / components of a theory
||My own words. Wikipedia did not seem to notice that a theory is more than a set of axioms, or a set of statements (axioms and theorems).|
||1.1, 1.3, 1.4,
| = 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 standard meaning which sounds better.
|| = interpretation of a theory.
See also (Mod, Tru) in 4.8
||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,
|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
|Usually meant as only accepting sets, or sets and urelements, or sets and classes. Not found elsewhere primitively accepting functions (nor under any other name).|
|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|
||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.2, 1.4||Ref - mathworld. Also called individual constant|
|value (of a variable)
||1.2, 1.5, 4.1|
|range ; range over
elsewhere called atom, while the latter word
has another standard 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
|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|
||here precisely defined in a way not seen
|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). Ref in philosophy
||1.3||Did not see it named nor conceived elsewhere.
|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)
|1.3||Not sure if named elsewhere. (See other def for notions of set theory below)|
|type (abstract type,
|1.3||Rarely mentioned in other works,
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. Others call it "signature" or "vocabulary", while including in the "language" all symbols beyond structures, or even the whole range of expressions.|
||here only first-order structures (operators and predicates)
||(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|
||1.4||Coined phrase. (Others can't imagine this as they don't believe in urelements)
||1.4, 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 -
type of result
||No standard terminology found for what I call "operator" as a model theoretical concept as opposed to "operation" or even "function" as set theoretical concept. Ref|
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 standard|
||I coined the name "evaluator" as I am not
aware of any standard name for this.
||I only comment it here, not use it (though it is the standard elsewhere), but only
discuss its consistency in 5.B.
See also 1.D (axiom schema of specification)
||This definition of "expression" as "term or
formula" just seems to be an implicit
|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 standard 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.
||see below "axioms of equality"|
||called elsewhere logical constant|
|type of an expression
||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
||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)|
||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. 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"
|meta-(notions of set theory)||1.7
||1.8, 2.1, 2.3
|axioms of equality
||References : wikibooks
of math. Used in 4.6 (proof of the completeness