101.
Skolem Function -- from MathWorld
- Weisstein, Eric W.
Consider a formula in prenex normal form, Q_1 x_1 \dots Q_n x_n N. If Q_i is the existential quantifier (1\leq i\leq n) and x_k, ..., x_m are all the universal quantifier variables such that 1\leq k, m < i, then introduce the new function symbol f and term f(x_k,\dots,x_m). (If i = 1, then f is a constant.) This function is called Skolem function (or Herbrand function). Now replace all occurrences of x_i by this term and remove Q_i. When all existential quantifiers are removed, convert N...
102.
Skolem Standard Form -- from MathWorld
- Weisstein, Eric W.
See: Skolemized Form
103.
Skolemization -- from MathWorld
- Weisstein, Eric W.
See: Skolemized Form
104.
Skolemized Form -- from MathWorld
- Weisstein, Eric W.
A formula of first-order logic is said to be in Skolemized form (sometimes also called Skolem standard form or universal form) if it is of the form \forall x_1 \dots \forall x_n M, where M is a quantifier-free formula in conjunctive normal form known as the matrix of the formula in question. Since M is a conjunction of clauses each of which is a disjunction of literals, M is often viewed as a set of the clauses. The process of placing a formula in Skolemized form is known as Skolemization. ...
105.
Statement Form -- from MathWorld
- Weisstein, Eric W.
An expression built up from statements letters by appropriate application of connectives (Mendelson 1997, p. 13). See also: Connective, Statement Letter
106.
Statement Letter -- from MathWorld
- Weisstein, Eric W.
A symbol used to represent a Boolean statement in logic and that can take on the value either true false. All statement letters are statements forms (Mendelson 1997, p. 13). See also: Literal, Statement Form
107.
Strict Order -- from MathWorld
- Weisstein, Eric W.
A relation < is a strict order on a set S if it is 1. Irreflexive: a < a does not hold for any a \in S. 2. Antisymmetric: a < b and b < a implies a = b. 3. Transitive: a < b and b < c implies a < c. Note that antisymmetry and irreflexivity combined imply that if a < b holds, then b < a does not. A strict order is total if, for any a, b \in S, either a < b, b < a, or a = b. Every partial order \leq induces...
108.
Structure -- from MathWorld
- Weisstein, Eric W.
Let L be a language of the first-order logic. Assume that the language L has the following sets of nonlogical symbols: 1. C is the set of constant symbols of L. (These are nullary function symbols.) 2. \mathcal{P} is the set of predicate symbols of L, and for each P\in\mathcal{P}, \alpha(P) is the arity of P. The symbols in \mathcal{P} are also called relation symbols of the language L. 3. \mathcal{F} is the set of function symbols of L, and for each f\in\mathcal{F}, \alpha(f) is the arity of...
109.
Syllogism -- from MathWorld
- Weisstein, Eric W.
A syllogism, also known as a rule of inference, is a formal logical scheme used to draw a conclusion from a set of premises. An example of a syllogism is Modus Ponens. See also: Conclusion, Deduction, Logic, Modus Ponens, Premise, Propositional Calculus
110.
Symbolic Logic -- from MathWorld
- Weisstein, Eric W.
The study of the meaning and relationships of statements used to represent precise mathematical ideas. Symbolic logic is also called formal logic. See also: Formal Logic, Logic, Metamathematics
111.
Tautology -- from MathWorld
- Weisstein, Eric W.
A logical statement in which the conclusion is equivalent to the premise. If p is a tautology, it is written \models p. A sentence whose truth table contains only 'T' is called a tautology. The following sentences are examples of tautologies: A\land B\equiv !({!A}\lor{!B}) (1) A\lor B\equiv {!A}\Rightarrow B (2) A\land B\equiv !(A\Rightarrow {!B}) (3) (Mendelson 1997, p. 26), where \land denotes AND, \equiv denotes "is equivalent to," ! denotes NOT, \lor denotes OR, and...
112.
Term Rewriting System -- from MathWorld
- Weisstein, Eric W.
Term rewriting systems are reduction systems in which rewrite rules apply to terms. Terms are built up from variables and constants using function symbols (or operations). Rules of term rewriting systems have the form x \to y, where both x and y are terms, x is not a variable, and every variable from y occurs in x as well. A reduction step for term r is defined as follows. If \theta is a unifier for r and x, then r is reduced to y\theta. If \theta is a unifier for r' and x where r' is a subterm...
113.
Theory -- from MathWorld
- Weisstein, Eric W.
A theory is a set of sentences which is closed under logical implication. That is, given any subset of sentences \{s_1,s_2,\dots\} in the theory, if sentence r is a logical consequence of \{s_1,s_2,\dots\}, then r must also be in the theory. See also: Logic, Sentence
114.
Three-Valued Logic -- from MathWorld
- Weisstein, Eric W.
A logical structure which does not assume the law of the excluded middle. Three truth values are possible: true, false, or undecided. There are 3072 such logics. See also: Fuzzy Logic, Law of the Excluded Middle, Logic
115.
Total Function -- from MathWorld
- Weisstein, Eric W.
A function defined for all possible input values. See also: Partial Function
116.
True -- from MathWorld
- Weisstein, Eric W.
A statement which is rigorously known to be correct. A statement which is not true is called false, although certain statements can be proved to be rigorously undecidable within the confines of a given set of assumptions and definitions. Regular two-valued logic allows statements to be only true or false, but fuzzy logic treats "truth" as a continuum which can have any value between 0 and 1. The symbol \curlyvee is sometimes used to denote "true," although "T" is...
117.
Truth Table -- from MathWorld
- Weisstein, Eric W.
A truth table is a two-dimensional array with n+1 columns. The first n columns correspond to the possible values of n inputs, and the last column to the operation being performed. The rows list all possible combinations of inputs together with the corresponding outputs. For example, the following truth table shows the result of the binary AND operator acting on two inputs A and B, each of which may be true or false. A B A\land B F F F F T F T F F T T T The following Mathematica code can be...
118.
Type -- from MathWorld
- Weisstein, Eric W.
Whitehead and Russell (1927) devised a hierarchy of "types" in order to eliminate self-referential statements from Principia Mathematica, which purported to derive all of mathematics from logic. A set of the lowest type contained only objects (not sets), a set of the next higher type could contain only objects or sets of the lower type, and so on. Unfortunately, Gödel's incompleteness theorem showed that both Principia Mathematica and all consistent formal systems must be...
119.
Unifiable -- from MathWorld
- Weisstein, Eric W.
See also: Unification, Unifier
120.
Unification -- from MathWorld
- Weisstein, Eric W.
Consider expressions built up from variables and constants using function symbols. If v_1, ..., v_n are variables and t_1, ..., t_n are expressions, then a set of mappings between variables and expressions \{t_1\vert v_1, \dots, t_n\vert v_n\} is called a substitution. If \eta = \{t_1\vert v_1, \dots, t_n\vert v_n\} and E is an expression, then E\eta is called an instance of E if it is received from E by simultaneously replacing all occurrences of v_i (for 0\leq i\leq n) by the respective t_i. ...
