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.
45.15 (The Key Theorem)
Any consistent first order theory has a denumerable model.
45.17 (Godel’s Theorem)
Any consistent set of wffs of a first order theory is simultaneously satisfiable in a denumerable domain.
Lemma 1: If Γ is a consistent set of a first order theory K, and K′ is a first order theory that results from merely adding denumerably many new individual constants to K, then Γ is a consistent set of K′.
Lemma 2: Let A be a wff in which some variable v has one or more free occurrences. Let c be a constant that does not occur in A or in any proper axiom of K. Then if Ac/v is a theorem of K, A is a theorem of K.
45.18 (Lowenheim-Skolem Theorem)
If a first order theory has a model, then it has a denumerable model.
45.19
If there is an interpretation I for which every proper axiom of a first order theory K is true, then K has a model.
45.20 (The compactness theorem for K)
If every finite subset of the set of proper axioms of a first order theory K has a model, then K has a model.
45.21
If A is a syntactic consequence of Γ in K, and v does not occur free in Γ, then ∧vA is a syntactic consequence of Γ in K. (An extension of 45.4)
45.22
If v has no free occurrence in B, then ∧v(A ⊃ B) ⊃ (∨vA ⊃ B) is a theorem of K.
45.23
If a variable u does not occur in A, then ∨vA ⊃ ∨uAu/v.
45.25
If t is a closed term of K, then At/v ⊃ ∨vA is a theorem of K.
46.1 (The Semantic Completeness Theorem for QS)
Every logically valid formula of Q is a theorem of QS.
46.2 (The Strong Completeness Theorem for QS)
If A is a semantic consequence of Γ in Q, then A is a syntactic consequence of Γ in QS.
46.4
QS is negation-complete.
47.1
QS= is consistent.
47.2
If K is a consistent first order theory with identity, then K has a countable normal model.
47.3
Any formula of Q that is true for every normal interpretation of Q is a theorem of QS=.
48.2
If M and M′ are isomorphic models of a first order theory of K, then a formula A of K is true for M iff it is true for M′.
48.3
If all normal models of a first order theory with identity are isomorphic, then the theory is negation complete. In other words, if a first order theory with identity is 2-categorical (All its normal models are isomorphic, then it is negation-complete).
