<<

. 104
( 107 .)



>>

Variable assignment: A function assigning objects to some or all of the
variables of a ¬rst-order language. This notion is used in de¬ning truth
of sentences in a ¬rst-order structure.

Well-formed formula (w¬ ): W¬s are the “grammatical” expressions of
fol. They are de¬ned inductively. First, an atomic w¬ is any n-ary
predicate followed by n terms. Complex w¬s are constructed using con-
nectives and quanti¬ers. The rules for constructing complex w¬s are
found on page 231. W¬s may have free variables. Sentences of fol are
w¬s with no free variables.




Glossary
General Index
=, 25, 37 § Intro, 144
=, 68 ∨ Elim, 150
§, 71 ∨ Intro, 148
∨, 74 ¬ Elim, 155, 161
¬, 68 ¬ Intro, 155
⊥, 137, 155, 157 ⊥ Elim, 159
’, 178 ⊥ Intro, 156
”, 181 ’ Elim, 206
∀, 228, 230 ’ Intro, 206
∃, 228, 230“231 ” Elim, 209
” Intro, 209
∈, 37, 406 ∀ Elim, 342
⊆, 413 ∀ Intro, 343
…, 412 ∃ Elim, 348
©, 415 ∃ Intro, 347
∪, 415
„˜, 429 Ana Con, 60, 61, 114, 115, 158,
| b |, 437 272, 286
FO Con, 115, 158, 271, 272, 286,
”, 83 524
F , 54, 142, 342 Taut Con, 114“116, 158, 171, 221,
FT , 215, 470 272
T , 470

M, 498 absolute complement, 419, 440
H, 532 ac, 436
g… , 501 Aczel, Peter, 441, 465
addition, 129
, 6, 7 afa, 441
‚, 6, 7 a¬rming the consequent, 203, 212
‚|, 6 alternative notation, 40, 66, 89, 90,
,7 196, 255“256
ambig-w¬s, 444
Reit, 56
ambiguity, 4, 79, 307
= Elim, 50, 51, 56
and context, 304
= Intro, 50, 51, 55
and inference, 308
§ Elim, 143



573
574 / General Index


Ana Con, 60, 61, 114, 115, 158, In¬nity, 436
272, 286 Powerset, 436
analytic consequence, 60 Regularity, 436, 440, 441
Replacement, 436
antecedent of a conditional, 178
Separation, 435
strengthening, 203, 212
Union, 435, 440
anti-foundation axiom, 441
Unordered Pair, 435
antisymmetry, 422
axiomatic method, 283, 287, 288
appropriate variable assignment, 501
and presuppositions, 287
arbitrary individual, 348
axioms, 47, 288
argument, 41, 44
of Peano arithmetic, 456“457
of a predicate, 21
of set theory, 435
sound, 43, 44, 140
shape, 285, 338“340
valid, 42, 44, 140
completeness of, 512
Aristotelian forms, 239“242
Aristotle, 3, 239
background assumptions, 287
arithmetic
Barber Paradox, 333, 362
¬rst-order language of, 38
base clause
arity, 21, 23, 25
of inductive de¬nition, 444, 445
of function symbols, 33
basis
arti¬cial language, 2“4
of proof by induction, 449
associativity
between, 25
of §, 118
biconditional, 181, 198
of ∨, 118
elimination, 199, 209
assumption
introduction, 209
for conditional proof, 200
binary
for existential instantiation, 322
function symbol, 33
for general conditional proof,
relation symbol, 308
324, 343
truth-functional connective, 190
for indirect proof, 136
Boole, 5“10, 100
for proof by cases, 132
Boole, George, 67
asymmetry, 422
Boolean searches, 91
atomic sentences, 19, 23, 23, 25, 32 Boolos, George, 555
atomic w¬, 228“229, 231 bound variable, 232, 282
automated theorem proving, 312 boxed constant, 343, 347
Axiom
Anti-foundation, 441 cancellability test, 188
Choice, 436 Cantor, Georg, 406, 437, 467
Comprehension, 406, 409, 408“ Carroll, Lewis, 268
410, 433, 435 Cartesian product, 421, 440
Extensionality, 407, 406“408, cases
435 proof by, 131“134


General Index
General Index / 575



chain of equivalences, 120, 128 proof, 199, 203, 206
claim, 24 general, 323, 329, 442
inherently vacuous, 246 conjunction, 67, 71, 129
clause elimination, 129, 143
empty, 489, 524 introduction, 129, 144
for resolution, 488 conjunctive normal form (CNF), 121“
CNF, 124 125, 479
commitment, 79 connectives, truth-functional, 67, 93,
in game, 77, 78 177
binary, 190
commutativity, 146
of §, 119 Boolean, 67
semantics for, 68, 72, 75, 178,
of ∨, 119
182
Compactness Theorem
ternary, 195
for ¬rst-order logic, 527, 548
consequence, 297
for propositional logic, 477
complete analytic, 60
¬rst-order, 267, 266“273
deductive system, 214, 219, 361
set of axioms, 338 FO, 267
logical, 2, 4“5, 41, 42, 44, 46,
truth-functionally, 190, 193
93, 110, 181, 267
completeness
tautological, 110“113, 219
of resolution, 491
in Fitch, 114
Completeness Theorem, 219, 526
consequent of a conditional, 178
for ¬rst-order logic, 527
a¬rming, 203, 212
for propositional logic, 470
strengthening, 203, 212
reformulation of, 472
weakening, 203, 212
use of, 220
complex noun phrase, 243 conservativity, 389“390
constructive dilemma, 203, 212
complex term, 32, 34
Con procedures in Fitch, 61 context sensitivity, 27, 304, 307
conclusion, 41, 44 contradiction, 137, 155
conditional, 176, 178, 198, 398 contradictory
antecedent of, 178 tt-, 138
strengthening, 203, 212 tt-, 158
consequent of, 178 contraposition, 199
a¬rming, 203, 212 contrapositive, 201
strengthening, 203, 212 conversational implicature, 187, 188,
weakening, 203, 212 244“247, 381
contrapositive of, 199 corollary, 218
elimination, 198, 206 correctness
introduction, 206 of axioms, 338



General Index
576 / General Index


DNF sentence, 125
counterexample, 5, 15, 63
¬rst-order, 270 Dodgson, Charles, 268
domain
Date of Birth Lemma, 530 of a function, 427
Deduction Theorem, 535 of discourse, 236, 348, 496
deductive system, 54 of quanti¬cation, 236
de¬nite descriptions domain of discourse, 498
Russellian analysis, 379 dot notation, 90
Strawson™s objection, 381 double negation, 68, 83, 83
DeMorgan laws, 81, 82, 83, 106,
182, 312
elimination rules, 142
and ¬rst-order equivalence, 275“
Elimination Theorem, 528, 534
279
proof of, 538
for quanti¬ers, 279, 355
empty clause, 489, 524
determinate property, 22, 24
empty set, 412
determiners, 227, 364
Enderton, Herbert, 435, 555
anti-persistent, 392
equivalence
general form, 384
¬rst-order, 267
generalized
and DeMorgan laws, 275“279
adding to fol, 388
logical, 93, 106“109, 267
binary, 397
of w¬s with free variables,
logic of, 394
276
semantics of, 387
tautological, 106“109
monotone, 366, 392
equivalence classes, 424“425
decreasing, 391
equivalence relations, 424“425
increasing, 390
Euclid™s Theorem, 332
persistent, 392“394
even number, 200, 242
reducible, 385
excluded middle, 97, 128, 174
discharged assumption, 164
exclusive disjunction, 74, 75
disjunction, 67, 74
existential
elimination, 149
elimination, 322, 347
exclusive, 74, 75
generalization, 320, 321
inclusive, 74
instantiation, 322“323, 329, 332
introduction, 129, 148
introduction, 320, 347
disjunctive normal form (DNF), 121“
noun phrase, 243
125
quanti¬er, 230“231
distributive laws, 122
sentence, 400
of § over ∨, 122, 124
w¬, 450
of ∨ over §, 122, 124
DNF, 124 extended discourse, 306, 307

<<

. 104
( 107 .)



>>