Metatheorems Flashcards
40.1
If A is logically valid, then ~A is not satisfiable.
40.2
If a sequence s satisfies A and also A ⊃ B, then it also satisfies B.
40.3
If A and A ⊃ B are both true for an interpretation I, then B is also true for I.
40.4
If A and A ⊃ B are both logically valid, then so is B.
40.5
A is false for a given interpretation iff ~A is true; and A is true for I iff ~A is false for I.
40.6
A is true for I iff ∧vA is true for I for any arbitrary variable v.
40.7
A is true for I iff any arbitrary closure of A is true for I.
40.8
A is logically valid iff Ac is.
40.9
∨vA is satisfiable for an interpretation iff A is satisfiable for the same interpretation.
40.13
If vk does not occur free in A, then A ⊃ ∧vkA is logically valid.
40.14
Let t and u be terms. Let t′ be the result of replacing each occurrence of vk in t by u. Let s be a sequence, and let us = d. In other words, let the member of D assigned by I to u for the sequence s be d. Let s′ be the sequence that results from substituting d for the kth term of s. Then, t′s = t*s′. In other words, the member of D assigned by I to t′ is the same as the member of D assigned by I to t for sequence s′.
40.15
Let A be a wff, vk a variable, t a term that is free for vk in A. Let s be a sequence, and let s′ be the sequence that results from replacing the kth term of s by t*s. Then, s satisfies At/vk iff s′ satisfies A.
40.16
∧vkA ⊃ At/vk is logically valid if t is free for vk in A.
40.17
If A is a closed wff, then exactly on of A and ~A is true, and exactly one false.
43.5
Every theorem of QS is logically valid.
43.7
If A is a syntactic consequence of Γ in QS, then A is a semantic consequence of Γ in Q.
45.4
If A is a theorem of K, then ∧vA is a theorem of K.
45.5
A is a theorem of k iff Ac is a theorem of K.
45.6
If A is a closed wff of K that is not a theorem of K, then K + {~A} is a consistent first order theory.
45.8
If a first order theory has a model, then it is consistent.
45.11
If K is a consistent first order theory, then the system that results from adding a denumerable set of new individual constants to K, with an effective enumeration of those
constants, is a consistent first order theory that is an extension of K.
45.13
If K is a consistent first order theory, then there is a first order theory K′ that is a consistent, closed, and negation-complete extension of K.
45.14
Any consistent, closed, negation-complete first order theory has a denumerable model. (Alternative in 45.16): Any consistent set of closed wff of a first order theory has a denumerable model.
45.16
Any consistent set of closed wff of a first order theory has a denumerable model.