# Shared Flashcard Set

## Details

Mathematical Logic Final
Final Exam
109
Mathematics
05/07/2013

Term
 propositional language L
Definition
 a set of propositional atoms p, q, r,....   an atomic L-formula is an atom of L
Term
 degree of A
Definition
 the number of occurences of propositional connective in A
Term
 formation sequence
Definition
 a finite sequence A1, A2,...,An such that each term of the sequence is obtained from previous terms by application of one of the rules for the definition of L-formulas.   A formation sequence for A is a formation sequence whose last term is A
Term
 formation tree
Definition
 a finite rooted dyadic tree where each node carries a formula and each non-atomic formula branches to its immediate subformulas   the formation tree for A is the unique formation tree which carries A at its root
Term
 polish notation & reverse polish notation
Definition
 example: (((p → q) Λ (q V r)) → (p V r)) → ¬(q V s)   polish: → → Λ → p q V q r V p r ¬ V q s   reverse polish: p q → q r V Λ p r V → q s V ¬ →
Term
 L-assignment
Definition
 a mapping   M: {p | p is an atomic L-formula} → {T,F}   where L is a propositional language and if L has exactly n atoms then there are exactly 2n different L-assignments
Term
 L-valuation (propositional calculus)
Definition
 Given an L-assignment M, there is a unique L-valuation   vM: {A | A is an L-formula} → {T,F}   given by clauses found on pg. 6
Term
 satisfiable (propositional calculus)
Definition
 A set of formulas S is said to be satisfiable if there exists an assignment M which satisfies S, i.e., vM(A)=T for all A [image] S
Term
 logical consequence (propositional calculus)
Definition
 Let S be a set of formulas. A formula B is said to be a logical consequence of S if it is true under all assignments which satisdy S
Term
 logically valid (propositional calculus)
Definition
 A formula B is said to be logically valid (or a tautology) if B is true under all assignments.   Equivalently, B is a logical consequence of the empty set.
Term
 Remark 1.2.13
Definition
 B is a logical consequence of A1, A2,...,An if and only if (A1 Λ A2 Λ...Λ An) → B is logically valid.   B is logically valid if and only if ¬B is not satisfiable.
Term
 logically equivalent (propositional calculus)
Definition
 Two formulas A and B are said to be logically equivalent, written A≡B, if each is a logical consequence of the other.
Term
 Remark 1.3.2
Definition
 A≡B holds if and only if A↔B is logically valid
Term
 disjunctive normal form
Definition
 A formula is said to be in disjunctive normal form if it is of the form A1 V A2 V...V Am, where each clause Ai, i=1,...,m, is of the form B1 Λ B2 Λ...Λ Bn, and each Bj. j=1,...,n is either an atom or the negation of an atom.
Term
 (un)signed formula (propositional calculus)
Definition
 A signed formula is an expression of the form TA or FA, where A is a formula.   An unsigned formula is simply a formula
Term
 (un)signed tableau (propositional calculus)
Definition
 A signed tableau is a rooted dyadic tree where each node carries a signed formula.   An unsigned tableau is a rooted dyadic tree where each node carries an unsigned formula.   If τ is a (un)signed tableau, an immediate extension of τ is a larger tableau τ' obtained by applying a tableau rule to a finite path of τ.
Term
 closed or open tableau
Definition
 A path of a tableau is said to be closed if it contains a conjugate pair of signed or unsigned formulas, i.e., a pair such as TA, FA in the signed case, or A, ¬A in the unsigned case.   A path is said to be open if it is not closed.   A tableau is said to be closed if each of its paths is closed.   A tableau is said to be open if it has at least one open path
Term
 the tableau method: test for validity
Definition
 to test a formula A for validity, form a signed tableau starting with FA, or equivalently an unsigned tableau starting with ¬A. If the tableau closes off, then A is logically valid
Term
 the tableau method: test for logical consequence
Definition
 to test whether B is a logical consequence of A1,...,Ak, form a signed tableau starting with TA1,...,TAk, FB, or equivalently an unsigned tableau starting with A1,...,Ak,¬B. If the tableau closes off, then B is indeed a logical consequence of A1,...,Ak
Term
 the tableau method: test for satisfiability
Definition
 to test A1,...,Ak for satisfiability, form a signed tableau starting with TA1,...,TAk, or equivalently an unsigned tableau starting with A1,...,Ak. If the tableasu closes off, then A1,...,Ak is not satisfiable. If the tableau does not close off, then A1,...,Ak is satisfiable, and from any open path we can read off an assignment satisfying A1,...,Ak
Term
 the soundness theorem (propositional calculus)
Definition
 if τ is a finite closed tableau starting with X1,...,Xk, then X1,...,Xk is not satisfiable
Term
 replete
Definition
 a path of a tableau is said to be replete if, whenever it contains the top formula of a tableau rule, it also contains at least one of the branches   a replete tableau is a tableau in which every path is replete
Term
 Lemma 1.5.3
Definition
 any finite tableau can be extended to a finite replete tableau
Term
 Lemma 1.5.5
Definition
 let τ be a replete tableau starting with X1,...,Xk. if τ is open, then X1,...,Xk is satisfiable
Term
 hintikka set
Definition
 let S be a set of signed or unsigned formulas. We say that S is a Hintikka set if:   1. S "obeys the tableau rules", in the sense that if it contains the top formula of a rule then it contains at least one of the branches;   2. S contains no pair of conjugate atomic formulas, i.e., Tp, Fp in the signed case, or p, ¬p in the unsigned case
Term
 hintikka's lemma
Definition
 If S is a Hintikka set, then S is satisfiable   proof on pg. 19
Term
 the completeness theorem
Definition
 X1,...,Xk is satisfiable if and only if there is no closed tableau starting with X1,...,Xk
Term
 Corollary 1.5.9
Definition
 A1,...,Ak is not satisfiable if and only if there exists a finite closed signed tableau starting with TA1,...TAk, or equivalently a finite closed unsigned tableau starting with A1,...,Ak
Term
 Corollary 1.5.10
Definition
 A is logically valid if and only if there exists a finite closed signed tableau starting with FA, or equivalently a finite closed unsigned tableau starting with ¬A
Term
 Corollary 1.5.11
Definition
 B is a logical consequence of A1,...,Ak if and only if there exists a finite closed signed tableau starting ith TA1,...,TAk, FB, or equivalently a finite closed unsigned tableau starting with A1,...,Ak, ¬B
Term
 tree
Definition
 a tree consists of: 1. a set T 2. a function l: T → N+ 3. a binary relation P on T   the elements of T are called the nodes of the tree for x [image] T, l(x) is the level of x l(x)=1 is the root of the tree each node other than the root has exactly one immediate predecessor
Term
 subtree
Definition
 a subtree of T is a nonempty set T' [image] T such that for all y [image] T' and xPy, x [image] T'. Note that T' is itself a tree, under the restriction of l and P to T'. Moreover, the root of T' is the same as the root of T
Term
 end node
Definition
 an end node of T is a node with no (immediate) successors
Term
 path
Definition
 a path in T is a set S [image] T such that: 1. the root of T belongs to S 2. for each x [image] S, either x is an end node of T or there is exactly one y [image] S such that xPy   xPy is read "x immediately precedes y"
Term
 finitely branching
Definition
 T is finitely branching if each node of T has only finitely many immediate successors in T
Term
Definition
 T is dyadic if each node of T has at most two immediate successors in T   Note that a dyadic tree is finitely branching
Term
 König's Lemma
Definition
 let T be an infinite, finitely branching tree. then T has an infinite path   proof on pg. 20 & notes
Term
 the compactness theorem, countable case (propositional calculus)
Definition
 let S be a countable set of propositional formulas. if each finite subset of S is satisfiable, then S is satisfiable   proof on pg. 21 & notes
Term
 the compactness theorem, uncountable case (propositional calculus)
Definition
 let S be an uncountable set of propositional formulas. if each finite subset of S is satisfiable, then S is satisfiable
Term
 languages (predicate calculus)
Definition
 a language L is a set of predicates, each predicate P of L being designated as n-ary for some nonnegative integer n
Term
 variables and quantifiers
Definition
 we assume the existence of a fixed, countably infinite set of symbols x, y, z,... known as variables   we introduced two new symbols: 1. the universal quanitifier ([image]) - "for all" 2. the existential quantifier ([image]) - "there exists"
Term
 formulas
Definition
 let L be a language, and let U be a set. it is understood that U is disjoint from the set of variables. the set of L-U formulas is generated as follows:   1. an atomic L-U formula is an expression of the form Pe1e2...en where P is an n-ary predicate of L and each e1, e2,...,en is either a variable or an element of U   2. each atomic L-U formula is an L-U formula   3. If A is an L-U formula, then ¬A is an L-U formula   4. If A and B are L-U formulas, then A Λ B, A V B, A→B, A↔B are L-U formulas   5. If x is a variable and A is an L-U formula then [image]xA and [image]xA are L-U formulas
Term
 degree of a formula
Definition
 the degree of a formula is the number of occurences of propositional connectives ¬, Λ, V, →, ↔ and quantifiers [image],[image] in it
Term
 Remark 2.1.6
Definition
 If U is a subset of U', then every L-U formula is automatically an L-U' formula. In particular, every L-formula is automatically and L-U formula, for any set U
Term
 substitution
Definition
 If A is an L-U formula and x is a variable and a [image] U, we define an L-U formula A[x/a] as follows:   1. If A is atomic then A[x/a]=the result of replacing each occurrence of x in A by a   2. (¬A)[x/a]=¬A[x/a]   3. (A Λ B)[x/a]=A[x/a] Λ B[x/a]   4. (A V B)[x/a]=A[x/a] V B[x/a]   5. (A→B)[x/a]=A[x/a]→B[x/a]   6. (A↔B)[x/a]=A[x/a]↔B[x/a]   7. ([image]xA)[x/a]=[image]xA   8. ([image]xA)[x/a]=[image]xA   9. If y is a variable other than x, then ([image]yA)[x/a]=[image]yA[x/a]   10. If y is a variable other than x, then ([image]yA)[x/a]=[image]yA[x/a]
Term
 free variables
Definition
 an occurrence of a variable x in an L-U formula A is said to be bound in A if it is within the scope of a quantifier [image]x or [image]x in A. an occurrence of a variable x in an L-U formula A is said to be free in A if it is not bound in A. a variable x is said to occur freely in A if there is at least one occurrence of x in A which is free in A
Term
 sentences
Definition
 an L-U sentence is an L-U formula in which no variable occur freely. an L-sentence is an L-Ø sentence, i.e., an L-U sentence where U=Ø, the empty set
Term
 Un is the set of n-tuples of elements of U
Definition
 let U be a nonempty set, and let n be a nonnegative integer. Un is the set of all n-tuples of elements of U, i.e., Un={|a1,...,an [image] U} An n-ary relation on U is a subset of Un
Term
 L-structure M
Definition
 Let L be a language. An L-structure M consists of a nonempty set UM, called the domain or universe of M, together with an n-ary relation PM on UM for each n-ary predicate P of L   an L-structure may be called a structure, in situations where the language L is understood from context
Term
 valuations (predicate calculus)
Definition
 given an L-structure M, there is a unique valuation or assignment of truth values vM: {A | A is an L-UM sentence} → {T,F}   defined on pg. 26
Term
 truth (predicate calculus)
Definition
 let M be an L-structure. let A be an L-UM sentence. we say that A is true in M if vM(A)=T. we say that A is false in M if vM(A)=F
Term
 satisfaction (predicate calculus)
Definition
 let M be an L-structure. let S be a set of L-UM sentences, we say that M satisfies S, abbreviated M [image] S, if all of the sentences of S are true in M
Term
 satisfiability (predicate calculus)
Definition
 let S be a set of L-sentences. S is said to be satisfiable if there exists an L-structure M which satisfies S
Term
 Remark 2.2.8
Definition
 satisfiability is one of the most important concepts of mathematical logic. a key result known as the Compactness Theorem states that a set S of L-sentences is satisfiable if and only if every finite subset of S is satisfiable
Term
 satisfiability in a domain
Definition
 let U be a nonempty set. a set S of L-U sentences is said to be satisfiable in the domain U if there exists an L-structure M such that M [image] S and UM=U
Term
 Remark 2.2.10
Definition
 let S be a set of L-sentences. then S is satisfiable if and only if S is satisfiable in some domain U
Term
 Theorem 2.2.11
Definition
 let S be a set of L-sentences. if S is satisfiable in a domain U, then S is satisfiable in any domain of the same cardinality as U
Term
 parameters
Definition
 fix a countably infinite set V={a1,a2,...,an,...}={a,b,c,...}. the elements of V will be called parameters   if L is a language, L-V sentences will be called sentences with parameters
Term
 (un)signed tableau (predicate calculus)
Definition
 a (signed or unsigned) tableau is a rooted dyadic tree where each node carries a (signed or unsigned) L-V sentence   the tableau rules for the predicate calculus are the same as those for the propositional calculus, with the a few additional rules   rules are found on pp. 31-32
Term
 Remark 2.3.3
Definition
 in the tableau rules, "a is new" means that a does not occur in the path that is being extended. or, we can insist that a does not occur in the tableau that is being extended
Term
 L-V structure
Definition
 an L-V structure consists of an L-structure M together with a mapping Φ: V→UM. if A is an L-V sentence, we write AΦ=A[a1/Φ(a),...,ak/Φ(ak)] where a1,...,ak are the parameters occurring in A. note that AΦ is an L-UM sentence. note also that, if A is an L-sentence, then AΦ=A
Term
 satisfiable - L-V (predicate calculus)
Definition
 let S be a finite or countable set of (signed or unsigned) L-V sentences. an L-V structure M,Φ is said to satisfy S if vM(AΦ)=T for all A [image] S. S is said to be satisfiable if there exists an L-V structure satisfying S
Term
 satisfiable τ (predicate calculus)
Definition
 let τ be an L-tableau. we say that τ is satisfiable if at least one path of τ is satisfiable
Term
 Lemma 2.3.12
Definition
 let τ and τ' be tableaux such that τ' is an immediate extension of τ, i.e., τ' is obtained from τ by applying a tableau rule to a path of τ. if τ is satisfiable, then τ' is satisfiable   proof on pp. 35-37
Term
 the soundness theorem (predicate calculus)
Definition
 let X1,...,Xk be a finite set of (signed or unsigned) sentences with parameters. if there exists a finite closed tableau starting with X1,...,Xk, then X1,...,Xk is not satisfiable   proof on pg. 37 & notes
Term
 defining A'
Definition
 given a formula A, let A'=A[x1/a1,...,xk/ak], where x1,...,xk are the variables which occur freely in A, and a1,...,ak are parameters not occurring in A. note that A' has no free variables, i.e., it is a sentence   we define A to be satisfiable if and only if A' is satisfiable   we define A to be logically valid if and only if A' is logically valid
Term
 logically equivalent (predicate calculus)
Definition
 let A and B be formulas. A and B are said to be logically equivalent, written A≡B, if A↔B is logically valid
Term
 Remark 2.4.8
Definition
 Look at pp. 38-39 for useful logical equivalences
Term
 variants
Definition
 let A be a formula. a variant of A is any formula A^ obtained from A by replacing all the bound variables of A by distinct new variables. note that A^ has the same free variables as A and is logically equivalent to A
Term
 prenex form
Definition
 a formula is said to be quantifier-free if it contains no quantifiers. a formula is said to be in prenex form if it is of the form Q1x1...Qnxn B, where each Qi is a quanitifier ([image] or [image]), each xi is a variable, and B is quantifier-free
Term
 universal closure
Definition
 let A be a formula. the universal closure of A is the sentence A*=[image]x1...[image]xk A, where x1,...,xk are the variables which occur freely in A. note that A**≡A*
Term
 logical consequence (predicate calculus)
Definition
 let A1,...,Ak,B be formulas. we say that B is a logical consequence of A1,...,Ak if (A1 Λ...Λ Ak)→B is logically valid. this is equivalent to saying that the universal closure of (A1 Λ...Λ Ak)→B is logically valid
Term
 Remark 2.4.20
Definition
 A and B are logically equivalent if and only if each is a logical consequence of the other. A is logically valid if and only if A is a logical consequence of the empty set. [image]xA is a logical consequence of A[x/a], but the converse does not hold in general. A[x/a] is a logical consequence of [image]xA, but the converse does not hold in general
Term
 closed or open L-U sentence(predicate calculus)
Definition
 S is closed if A contains a conjugate pair of L-U sentences. in other words, for some L-U sentence A, A contains TA, FA in the signed case, A, ¬A in the unsigned case   S is open if it is not closed
Term
 U-replete (predicate calculus)
Definition
 S is U-replete if S "obeys the tableau rules" with respect to U   clauses are found on pp. 40-41
Term
 hintikka's lemma (predicate calculus)
Definition
 If S is U-replete and open, then S is satisfiable. in fact, S is satisfiable in the domain U   proof on pp. 41-42 & notes
Term
 Lemma 2.5.4
Definition
 let τ0 be a finite tableau. by applying tableau rules, we can extend τ0 to a (possibly infinite) tableau τ with the following properties: every closed path of τ is finite, and every open path of τ is V-replete   proof on pp. 42-43
Term
 the completeness theorem
Definition
 let X1,...,Xk be a finite set of (signed or unsigned) sentences with parameters. if X1,...,Xk is not satisfiable, then there exists a finite closed tableau starting with X1,...,Xk. if X1,...,Xk is satisfiable, then X1,...,Xk is satisfiable in the domain V   proof on pg. 43 & notes
Term
 the compactness theorem - countable & uncountable (predicate calculus)
Definition
 let S be a set of sentences of the predicate calculus. S is saitisfiable if and only if each finite subset of S is satisfiable   proof on pp. 46-47 & notes
Term
 Theorem 2.7.1
Definition
 let S be a set of L-sentences   1. assume that S is finite or countably infinite. if S is satisfiable, then S is satisfiable in a countably infinite domain   2. assume that S is of cardinality κ≥[image]. if S is satisfiable, then S is satisfiable in a domain of cardinality κ   proof on pg. 48
Term
 Corollary 2.7.4
Definition
 let S be a set of L-sentences. if S is satisfiable in a domain U, then S is satisfiable in any domain of the same or larger cardinality   proof on pg. 48
Term
 quasitautologies
Definition
 1. a tautology is a propositional formula which is logically valid   2. a quasitautology is an L-V sentence of the form F[p1/A1,...,pk/Ak], where F is a tautology, p1,...,pk are the atoms occurring in F, and A1,...,Ak are L-V sentences
Term
 companions
Definition
 a companion of A is any L-V sentence of one fo the forms:   1. ([image]xB)→B[x/a] 2. B[x/a]→([image]xB) 3. ([image]xB)→B[x/a] 4. B[x/a]→([image]xB)   where in 2 and 3, the parameter a may not occur in A or B
Term
 Lemma 3.2.4
Definition
 let C be a companion of A   1. A is satisfiable if and only if C Λ A is satisfiable 2. A is logically valid if and only if C→A is logically valid   proof on pg.52
Term
 companion sequences
Definition
 a companion sequence of A is a finite sequence C1,...,Cn such that, for each i
Term
 Lemma 3.2.6
Definition
 if C1,...,Cn is a companion sequence of A, then A is logically valid if and only if (C1 Λ...Λ Cn)→A is logically valid   proof on pp. 52-53
Term
 the companion theorem
Definition
 A is logically valid if and only if there exists a companion sequence C1,...,Cn of A such that (C1 Λ...Λ Cn)→A is a quasitautology   proof on pp. 53-54
Term
 the system LH
Definition
 our Hilbert-style proof system LH for the predicate calculus is as follows:   1. the objects are L-V sentences 2. for each quasitautology A, is a rule of inference 3. <([image]xB)→B[x/a]> and are rules of inference 4. is a rule of inference 5. and are rules of inference, provided the parameter a does not occur in A or in B
Term
 the system LH (schematically)
Definition
 LH consisits of:   1. A, where A is any quasitautology 2. (a) ([image]xB)→B[x/a] (universal instantiation) (b) B[x/a]→([image]xB) (existential instantiation) 3. if A, A→B then B (modus ponens) 4. (a) if A→B[x/a] then A→([image]xB) (universal generalization) (b) if B[x/a]→A then ([image]xB)→A (existential generalization) where a does not occur in A,B
Term
 soundness of LH
Definition
 LH is sound. in other words, for all L-V sentences A, if A is derivable, then A is logically valid
Term
 Lemma 3.3.5
Definition
 LH is closed under quasitautological consequence. in other words if A1,...,Ak are derivable, and if B is a quasitautological consequence of A1,...,Ak then B is derivable   proof on pg. 57
Term
 Lemma 3.3.6
Definition
 if C is a companion of A, and if C→A is derivable in LH, then A is derivable in LH   proof on pg. 57
Term
 completeness of LH
Definition
 LH is sound and complete. in other words, for all L-V sentences A, A is derivable if and only if A is logically valid   proof on pg. 58
Term
 Notation 3.3.17
Definition
 we write S [image] B to indicate that B is derivable in LH(S)
Term
 language with identity
Definition
 a language with identity consists of a language L with a particular binary predicate, I, designated as the identity predicate
Term
 identity axioms
Definition
 let L be a language with identity. the identity axioms for L are the following sentences   1. [image]x Ixx (reflexivity) 2. [image]x[image]y(Ixy↔Iyx) (symmetry) 3. [image]x[image]y[image]z((Ixy Λ Iyz)→ Ixz) (transitivity) 4. for each n-ary predicate P of L, we have an axiom [image]x1...[image]xn[image]y1...[image]yn((Ix1y1 Λ...Λ Ixnyn)→(Px1...xn↔Py1...yn)) (congruence)
Term
 normal
Definition
 an L-structure M is said to be normal if the identity predicate denotes the identity relation, i.e., IM={ | a [image] UM}
Term
 Theorem 4.1.6
Definition
 If M is an L-structure satisfying the identity axioms for L, then we have a normal L-structure M' satisfying the same sentences as M
Term
 normally satisfiable
Definition
 S is normally satisfiable if there exists a normal L-structure which satisfies S
Term
 Corollary 4.1.8
Definition
 let S be a set of L-sentences. S is normally satisfiable if and only if S U {identity axioms for L} is satisfiable
Term
 the compactness theorem (for normal satisfiability)
Definition
 S is normally satisfiable if and only if each finite subset of S is normally satisfiable
Term
 Löwenheim/Skolem theorem
Definition
 1. if S is normally satisfiable in arbitrarily large finite domains, then S is normally satisfiable in some infinite domain   2. if S is normally satisfiable in some infinte domain, then S is normally satisfiable in all domains of cardinality ≥ the cardinaloty of S   proof on pp. 73-74
Term
 languages (with operations)
Definition
 a language is a set of predicates P,Q,R,...and operations f,g,h,... each predicate and each operation is designated as n-ary for some nonnegative integer n
Term
 terms, formulas, sentences (with operations)
Definition
 let L be a language, and let U be a set. the set of L-U terms is generated as follows:   1. each variable is an L-U term 2. each element of U is an L-U term 3. if f is an n-ary operation of L, and if t1,...,tn are L-U terms, then ft1...tn is an L-U term
Term
 atomic L-U formula
Definition
 an atomic L-U formula is an expression of the form Pt1...tn where P is an n-ary predicate of L, and t1,...,tn are L-U terms
Term
 structures (with operations)
Definition
 an L-structure M consists of a nonempty set UM, an n-ary relation PM [image] (UM)n for each n-ary predicate P of L, and an n-ary function fM: (UM)n → UM for each n-ary operation f of L
Term
 isomorphisms
Definition
 pg. 79
Term
 valuations (with operations)
Definition
 let M be an L-structure   pg. 79
Term
 tableau method (with operations)
Definition
 the signed and unsigned tableau methods carry over to predicate calculus with operations. we modify the tableau rules as follows:   on pg. 80
Supporting users have an ad free experience!