“many-sorted logic”的概念、定义、翻译、参考文献-科学参考

many-sorted logic

Logic

An extension of first-order logic in which the domain is partitioned into distinct types—or sorts—of elements. This structure can be imposed as a means of avoiding category mistakes by typing objects, i.e., by placing Caesar and the number $2$ in distinct sorts.
A prominent example is the case of vector spaces, in which vectors and scalars are kept distinct. In the case of classical logic, finitely-sorted logic is typically definable by the addition of unary predicates $S_{i}$ for each sort along with axioms corresponding to the exhaustive partitioning of the domain into these sorts, i.e., an $n$ -sorted logic can be reduced to a one-sorted logic by the axioms:
- • $\forall x \neg (S_{i} (x) \land S_{j} (x))$ for $i \neq j$
- • $\forall x (S_{0} (x) \lor . . . \lor S_{n - 1} (x))$
Quantification over one of the types can then be expressed by restricted quantification, $\exists x (S (x) \land φ)$ and $\forall x (S (x) \to φ)$ , where $S$ is the predicate corresponding to the relevant sort.

Philosophy

A logic in which the variables range over different domains. In classical predicate calculus a proposition like ‘All Fs are G’ is represented as saying: take anything; if it is F, it is G. In a many-sorted logic the representation will be: take any F; it is G. This may accord better with natural language, and it matches traditional syllogistic forms better than the predicate calculus does.

单词	many-sorted logic
释义	many-sorted logic Logic An extension of first-order logic in which the domain is partitioned into distinct types—or sorts—of elements. This structure can be imposed as a means of avoiding category mistakes by typing objects, i.e., by placing Caesar and the number $2$ in distinct sorts. A prominent example is the case of vector spaces, in which vectors and scalars are kept distinct. In the case of classical logic, finitely-sorted logic is typically definable by the addition of unary predicates $S_{i}$ for each sort along with axioms corresponding to the exhaustive partitioning of the domain into these sorts, i.e., an $n$ -sorted logic can be reduced to a one-sorted logic by the axioms: • $\forall x \neg (S_{i} (x) \land S_{j} (x))$ for $i \neq j$ • $\forall x (S_{0} (x) \lor . . . \lor S_{n - 1} (x))$ Quantification over one of the types can then be expressed by restricted quantification, $\exists x (S (x) \land φ)$ and $\forall x (S (x) \to φ)$ , where $S$ is the predicate corresponding to the relevant sort. Philosophy A logic in which the variables range over different domains. In classical predicate calculus a proposition like ‘All Fs are G’ is represented as saying: take anything; if it is F, it is G. In a many-sorted logic the representation will be: take any F; it is G. This may accord better with natural language, and it matches traditional syllogistic forms better than the predicate calculus does.
随便看	cartel Carter, Brandon Carter, James Earl (1924) Carter, Manley Jr (1947–91) Cartesian Cartesian circle Cartesian coordinates Cartesian coordinate system Cartesian distance Cartesian doubt Cartesian dualism Cartesian ego Cartesian plane Cartesian product Cartesian projection Cartesian space Cartesian structure Cartesian tensor Carthage Cartier, Sir George-Etienne (1814–73) cartilage cartilage bone cartilaginous fish cartilaginous fishes cartogram