“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.
随便看	bridgeware Bridgewater Treatises bridgmanite bridgmanite-enriched mantle structure Bridgman, Percy William (1882–1962) Bridgman, Percy Williams Bridgman, Percy Williams (1882–1961) Brier score Brigantes Brigantian Briggs, Henry Briggs, Henry (1561–1630) brighteners Bright, John (1811–89) bright nebula brightness temperature bright spot Bright Star Catalogue Brillat-Savarin, Jean Anthelme (1755–1826) Brillinger, David Ross (1937– ) Brillouin spectroscopy Brillouin zone brine Brinell hardness Brinell hardness number