81.
Predicate -- from MathWorld
- Weisstein, Eric W.
An operator in logic which returns either true or false. See also: AND, False, NAND, NOR, NOT, OR, Predicate Calculus, True, XNOR, XOR
82.
Predicate Calculus -- from MathWorld
- Weisstein, Eric W.
The branch of formal logic, also called functional calculus, that deals with representing the logical connections between statements as well as the statements themselves. See also: Gödel's Incompleteness Theorem, Logic, Predicate, Propositional Calculus
83.
Premise -- from MathWorld
- Weisstein, Eric W.
A premise is a statement that is assumed to be true. Formal logic uses a set of premises and syllogisms to arrive at a conclusion. See also: Conclusion, Deduction, Logic, Propositional Calculus, Syllogism
84.
Prenex Normal Form -- from MathWorld
- Weisstein, Eric W.
A formula of first-order logic is in prenex normal form if it is of the form Q_1 x_1 \dots Q_n x_n M, where each Q_i is a quantifier \forall ("for all") or \exists ("exists") and M is quantifier-free. For example, the formula \exists x \forall y \exists z ( P(x) \vee Q(x,y,z) ) is in prenex normal form, whereas formula \exists x \forall y ( P(x) \vee \exists z Q(x,y,z) ) is not, where \vee denotes OR. Every formula of first-order logic can be converted to an equivalent...
85.
Propositional Calculus -- from MathWorld
- Weisstein, Eric W.
The formal basis of logic dealing with the notion and usage of words such as "NOT," "OR," "AND," and "implies." Many systems of propositional calculus have been devised which attempt to achieve consistency, completeness, and independence of axioms. The term "sentential calculus" is sometimes used as a synonym for propositional calculus. Axioms (or their schemata) and rules of inference define a proof theory, and various equivalent proof theories...
86.
Propositional Connective -- from MathWorld
- Weisstein, Eric W.
See: Connective
87.
Propositional Formula -- from MathWorld
- Weisstein, Eric W.
See: Sentential Formula
88.
Propositional Variable -- from MathWorld
- Weisstein, Eric W.
See: Sentential Variable
89.
Quantifier -- from MathWorld
- Weisstein, Eric W.
One of the operations exists \exists (called the existential quantifier) or for all \forall (called the universal quantifier, or sometimes, the general quantifier). However, there also exist more exotic branches of logic which use quantifiers other than these two. See also: Bound Variable, Existential Quantifier, Exists, For All, Free, Quantified System, Quantifier Elimination, Universal Quantifier
90.
Reduction Order -- from MathWorld
- Weisstein, Eric W.
A strict order > on the set of terms of a term rewriting system is called a reduction order if 1. The set of terms is well ordered with respect to >, that is, all its nonempty subsets contain their least elements, 2. This order is compatible with functions (operations) of the system, i.e., t_i > t'_i \Rightarrow f(t_1,\dots,t_i,\dots,t_n) > f(t_1,\dots,t'_i,\dots,t_n), and 3. For any substitution \theta (cf. unification), s > t \Rightarrow s\theta > t\theta. If x > y...
91.
Reduction System -- from MathWorld
- Weisstein, Eric W.
A system in which words (expressions) of a formal language can be transformed according to a finite set of rewrite rules is called a reduction system. While reduction systems are also known as string rewriting systems or term rewriting systems, the term "reduction system" is more general. Lambda calculus is an example of a reduction system with lambda conversion rules constituting its rewrite rules. If none of the rewrite rules of a reduction system apply to expression E, then E is said...
92.
Regular Expression -- from MathWorld
- Weisstein, Eric W.
Regular expressions define formal languages as sets of strings over a finite alphabet. Let \sigma denote a selected alphabet. Then \varnothing is a regular expression that denotes the empty set and \epsilon is a regular expression that denotes the set containing the empty string as its only element. If c \in \sigma, then c is a regular expression that denotes the set whose only element is string c. If p and q are regular expressions denoting sets L(p) and L(q), then 1. (p)\vert(q) is a regular...
93.
Resolution Principle -- from MathWorld
- Weisstein, Eric W.
The resolution principle, due to Robinson (1965), is a method of theorem proving that proceeds by constructing refutation proofs, i.e., proofs by contradiction. This method has been exploited in many automatic theorem provers. The resolution principle applies to first-order logic formulas in Skolemized form. These formulas are basically sets of clauses each of which is a disjunction of literals. Unification is a key technique in proofs by resolution. If two or more positive literals (or two or...
94.
Rule of Inference -- from MathWorld
- Weisstein, Eric W.
See: Syllogism
95.
Satisfiable -- from MathWorld
- Weisstein, Eric W.
A formula is called satisfiable if it takes at least one true value in some interpretation. See also: Interpretation, Satisfiability Problem, Unsatisfiable
96.
Schema -- from MathWorld
- Weisstein, Eric W.
See: Axiom Schema
97.
Sentence -- from MathWorld
- Weisstein, Eric W.
A sentence is a logic formula in which every variable is quantified. The concept of a sentence is important because formulas with variables that are not quantified are ambiguous. The concept of the sentence can be illustrated as follows (Enderton 1977). The formula \exists(x,\forall(y,y\in x)), in which each variable is quantified, can be translated into English as the complete sentence "There exists a set which has every set as an element." However, the formula \forall(y,(y\in x)),...
98.
Sentential Formula -- from MathWorld
- Weisstein, Eric W.
An expression which is a sentence or which contains variables and becomes a sentence upon appropriate substitutions for these variables (Carnap 1958, p. 24). Sentential formulas are also known as propositional formulas or, for short, simply "formulas." See also: Closed Sentential Formula, Open Sentential Formula, Propositional Calculus, Sentence, Sentential Variable
99.
Sentential Variable -- from MathWorld
- Weisstein, Eric W.
A sentential variable, also called a propositional variable, that can be substituted for in arbitrary sentential formulas (Carnap 1958, p. 24). See also: Sentential Formula
100.
Sequent Calculus -- from MathWorld
- Weisstein, Eric W.
A sequent is an expression \Gamma\vdash\wedge, where \Gamma and \wedge are (possibly empty) sequences of formulas. Here, \Gamma is called the antecedent and \wedge is called the consequent. The informal understanding of sequents is that the sequent A_1, \dots, A_n \vdash B_1,\dots,B_m corresponds to A_1\vee\dots\vee A_n \supset B_1\vee\dots\vee B_m. The initial sequent of all derivations is A\vdash A. The rules of inference for sequent calculus are divided in two categories: structural and...
