61.
Interpretation -- from MathWorld
- Weisstein, Eric W.
An interpretation of first-order logic consists of a non-empty domain D and mappings for function and predicate symbols. E very n-place function symbol is mapped to a function from D^n to D, and every n-place predicate symbol is mapped to a function from D^n to the set comprised of two values true and false. The domain D is the range of all variables in formulas of first-order logic, and is called the domain of the interpretation. For a given interpretation, the truth table of any formula is...
62.
Intuitionistic Logic -- from MathWorld
- Weisstein, Eric W.
The proof theories of propositional calculus and first-order logic are often referred to as classical logic. Intuitionistic propositional logic can be described as classical propositional calculus in which the axiom schema \lnot\lnot F \Rightarrow G is replaced by \lnot F \Rightarrow ( F \Rightarrow G ). Similarly, intuitionistic predicate logic is intuitionistic propositional logic combined with classical first-order predicate calculus. Intuitionistic logic is a part of classical logic, that...
63.
Karnaugh Map -- from MathWorld
- Weisstein, Eric W.
In combinatorial logic minimization, a device known as a Karnaugh map is frequently used. It is similar to a truth table, but the various variables are represented along two axes, and are arranged in such a way that only one input bit changes in going from one square to an adjacent square. See also: Truth Table
64.
Knuth-Bendix Algorithm -- from MathWorld
- Weisstein, Eric W.
See: Knuth-Bendix Completion Algorithm
65.
Knuth-Bendix Completion Algorithm -- from MathWorld
- Weisstein, Eric W.
The Knuth-Bendix completion algorithm attempts to transform a finite set of identities into a finitely terminating, confluent term rewriting system whose reductions preserve identity. This term rewriting system serves a decision procedure for validating identities. As defined in universal algebra, identities are equalities of two terms: x = y. Presumably, the values of the two terms are equal for all values of variables occurring in them. A reduction order is another input to the completion...
66.
Knuth-Bendix Procedure -- from MathWorld
- Weisstein, Eric W.
See: Knuth-Bendix Completion Algorithm
67.
König's Lemma -- from MathWorld
- Weisstein, Eric W.
A tree with a finite number of branches at each fork and with a finite number of leaves at the end of each branch is called a finitely branching tree. König's lemma states that a finitely branching tree is infinite iff it has an infinite path. This lemma is used in proofs of completeness in logic. See also: Branch, Fork, Kruskal's Tree Theorem, Tree, Tree Leaf
68.
Law of the Excluded Middle -- from MathWorld
- Weisstein, Eric W.
A law in (2-valued) logic which states there is no third alternative to truth or falsehood. In other words, for any statement A, either A or not-A must be true and the other must be false. This law no longer holds in three-valued logic or fuzzy logic. See also: Bivalent, Fuzzy Logic, Three-Valued Logic
69.
Literal -- from MathWorld
- Weisstein, Eric W.
A statement letter or a negation of a statement letter (Mendelson 1997, p. 30). See also: Conjunctive Normal Form, Disjunctive Normal Form, Negation, Statement Letter
70.
Löwenheim-Skolem Theorem -- from MathWorld
- Weisstein, Eric W.
A fundamental result in model theory which states that if a countable theory has a model, then it has a countable model. Furthermore, it has a model of every cardinality greater than or equal to \aleph_0 (aleph-0). This theorem established the existence of "nonstandard" models of arithmetic. The Löwenheim-Skolem theorem establishes that any satisfiable formula of first-order logic is satisfiable in an \aleph_0 (aleph-0) domain of interpretation. Hence, aleph-0 domains are...
71.
Markov Algorithm -- from MathWorld
- Weisstein, Eric W.
An algorithm which constructs allowed mathematical statements from simple ingredients.
72.
Metamathematics -- from MathWorld
- Weisstein, Eric W.
Metamathematics is the study of mathematics and mathematical reasoning (Hofstadter 1989) in a general and abstract sense itself. Instead of studying the objects of a particular mathematical theory, it examines the mathematical theories as such, especially with respect to their logical structure. Since it mainly concentrates on the way in which theorems are derived from axioms, it is often also called proof theory. The branch of logic dealing with the study of the combination and application of...
73.
Metatheory -- from MathWorld
- Weisstein, Eric W.
The study of the inner structure of a mathematical theory considered as a whole. It deals with the general properties of the rules according to which the objects of a certain theory are combined and linked, and the principles of reasoning on which its argumentation is based. When describing the language of the theory, the metatheory must resort to a different language located on a higher level, since the terms and symbols of the theory are looked at from above, as objects to be described and...
74.
Model -- from MathWorld
- Weisstein, Eric W.
A well-formed formula B is said to be true for the interpretation M (written \models_M B) iff every sequence in \Sigma (the set of all denumerable sequences of elements of the domain of M), satisfies B. B is said to be false for M iff no sequence in \Sigma satisfies B. Then an interpretation M is said to be a model for a set \Gamma of well-formed formulas iff every well-formed formula in \Gamma is true for M (Mendelson 1997, pp. 59-60). See also: Generalized Completeness Theorem, Interpretation...
75.
Modus Ponens -- from MathWorld
- Weisstein, Eric W.
The rule {F, F \Rightarrow G\over G}, where \Rightarrow means "implies," which is the sole rule of inference in propositional calculus. This rule states that if each of F and F \Rightarrow G is either an axiom or a theorem formally deduced from axioms by application of inference rules, then G is also a formal theorem. See also: Propositional Calculus
76.
Natural Independence Phenomenon -- from MathWorld
- Weisstein, Eric W.
A type of mathematical result which is considered by most logicians as more natural than the metamathematical incompleteness results first discovered by Gödel. Finite combinatorial examples include Goodstein's theorem, a finite form of Ramsey's theorem, and a finite form of Kruskal's tree theorem (Kirby and Paris 1982; Smorynski 1980, 1982, 1983; Gallier 1991). See also: Gödel's Incompleteness Theorem, Goodstein's Theorem, Kruskal's Tree Theorem, Ramsey's Theorem
77.
Open Sentential Formula -- from MathWorld
- Weisstein, Eric W.
A sentential formula that contains at least one free variable (Carnap 1958, p. 24). A sentential variable containing no free variables (i.e., all variables are bound) is called a closed sentential formula. Examples of closed sentential formulas include \exists y(x = 2y), which means that x is even (over the domain of integers), and x > 1 \land \forall u \forall v (x \not= (u+2)(v+2)), which means that x > 1 and x is not the product of two numbers (both greater than one), i.e., x is...
78.
P-Symbol -- from MathWorld
- Weisstein, Eric W.
A symbol employed in a formal propositional calculus.
79.
Partial Function -- from MathWorld
- Weisstein, Eric W.
A partial function is a function that is not total. See also: Total Function
80.
Poretsky's Law -- from MathWorld
- Weisstein, Eric W.
The theorem in set theory and logic that for all sets A and B, B=(A\cap \bar B)\cup (B\cap\bar A) \Leftrightarrow A=\varnothing, where \bar A denotes complement set of A and \varnothing is the empty set. The set (A\cap \bar B)\cup (\bar A\cap B) is depicted in the above Venn diagram and clearly coincides with B iff A is empty. The corresponding theorem in a Boolean algebra R states that for all elements a, b of R, b=(a\wedge b')\vee (a'\wedge b)\Leftrightarrow a=0. The version of Poretsky's...
