First-Order Logic
المؤلف:
Chang, C.-L. and Lee, R. C.-T.
المصدر:
Symbolic Logic and Mechanical Theorem Proving. New York: Academic Press, 1997.
الجزء والصفحة:
...
24-1-2022
1358
First-Order Logic
The set of terms of first-order logic (also known as first-order predicate calculus) is defined by the following rules:
1. A variable is a term.
2. If 
is an 
-place function symbol (with 
) and 
, ..., 
are terms, then 
is a term.
If 
is an 
-place predicate symbol (again with 
) and 
, ..., 
are terms, then 
is an atomic statement.
Consider the sentential formulas 
and 
, where 
is a sentential formula, 
is the universal quantifier ("for all"), and 
is the existential quantifier ("there exists"). 
is called the scope of the respective quantifier, and any occurrence of variable 
in the scope of a quantifier is bound by the closest 
or 
. The variable 
is free in the formula 
if at least one of its occurrences in 
is not bound by any quantifier within 
.
The set of sentential formulas of first-order predicate calculus is defined by the following rules:
1. Any atomic statement is a sentential formula.
2. If 
and 
are sentential formulas, then 
(NOT 
), 
(
AND 
), 
(
OR 
), and 
(
implies 
) are sentential formulas (cf. propositional calculus).
3. If 
is a sentential formula in which 
is a free variable, then 
and 
are sentential formulas.
In formulas of first-order predicate calculus, all variables are object variables serving as arguments of functions and predicates. (In second-order predicate calculus, variables may denote predicates, and quantifiers may apply to variables standing for predicates.) The set of axiom schemata of first-order predicate calculus is comprised of the axiom schemata of propositional calculus together with the two following axiom schemata:
 |
(1)
|
 |
(2)
|
where 
is any sentential formula in which 
occurs free, 
is a term, 
is the result of substituting 
for the free occurrences of 
in sentential formula 
, and all occurrences of all variables in 
are free in 
.
Rules of inference in first-order predicate calculus are the Modus Ponens and the two following rules:
 |
(3)
|
 |
(4)
|
where 
is any sentential formula in which 
occurs as a free variable, 
does not occur as a free variable in formula 
, and the notation means that if the formula above the line is a theorem formally deducted from axioms by application of inference rules, then the sentential formula below the line is also a formal theorem.
Similarly to propositional calculus, rules for introduction and elimination of 
and 
can be derived in first-order predicate calculus. For example, the following rule holds provided that 
is the result of substituting variable 
for the free occurrences of 
in sentential formula 
and all occurrences of 
resulting from this substitution are free in 
,
 |
(5)
|
Gödel's completeness theorem established equivalence between valid formulas of first-order predicate calculus and formal theorems of first-order predicate calculus. In contrast to propositional calculus, use of truth tables does not work for finding valid sentential formulas in first-order predicate calculus because its truth tables are infinite. However, Gödel's completeness theorem opens a way to determine validity, namely by proof.
REFERENCES
Chang, C.-L. and Lee, R. C.-T. Symbolic Logic and Mechanical Theorem Proving. New York: Academic Press, 1997.
Kleene, S. C. Mathematical Logic. New York: Dover, 2002.Mendelson, E. Introduction to Mathematical Logic, 4th ed. London: Chapman & Hall, p. 12, 1997.
الاكثر قراءة في المنطق
اخر الاخبار
اخبار العتبة العباسية المقدسة
