Term

Definition
a set of propositional atoms p, q, r,....
an atomic Lformula is an atom of L 


Term

Definition
the number of occurences of propositional connective in A 


Term

Definition
a finite sequence A_{1}, A_{2},...,A_{n} such that each term of the sequence is obtained from previous terms by application of one of the rules for the definition of Lformulas.
A formation sequence for A is a formation sequence whose last term is A 


Term

Definition
a finite rooted dyadic tree where each node carries a formula and each nonatomic 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

Definition
a mapping
M: {p  p is an atomic Lformula} → {T,F}
where L is a propositional language and if L has exactly n atoms then there are exactly 2^{n}^{} different Lassignments 


Term
Lvaluation (propositional calculus) 

Definition
Given an Lassignment M, there is a unique Lvaluation
v_{M}: {A  A is an Lformula} → {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., v_{M}(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

Definition
B is a logical consequence of A_{1}, A_{2},...,A_{n} if and only if (A_{1} Λ A_{2} Λ...Λ A_{n}) → 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

Definition
A≡B holds if and only if A↔B is logically valid 


Term

Definition
A formula is said to be in disjunctive normal form if it is of the form A_{1} V A_{2} V...V A_{m}, where each clause A_{i}, i=1,...,m, is of the form B_{1} Λ B_{2} Λ...Λ B_{n}, and each B_{j}. 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

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 A_{1},...,A_{k}, form a signed tableau starting with TA_{1},...,TA_{k}, FB, or equivalently an unsigned tableau starting with A_{1},...,A_{k},¬B. If the tableau closes off, then B is indeed a logical consequence of A_{1},...,A_{k} 


Term
the tableau method: test for satisfiability 

Definition
to test A_{1},...,A_{k} for satisfiability, form a signed tableau starting with TA_{1},...,TA_{k}, or equivalently an unsigned tableau starting with A_{1},...,A_{k}. If the tableasu closes off, then A_{1},...,A_{k} is not satisfiable. If the tableau does not close off, then A_{1},...,A_{k} is satisfiable, and from any open path we can read off an assignment satisfying A_{1},...,A_{k} 


Term
the soundness theorem (propositional calculus) 

Definition
if τ is a finite closed tableau starting with X_{1},...,X_{k}, then X_{1},...,X_{k} is not satisfiable 


Term

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

Definition
any finite tableau can be extended to a finite replete tableau 


Term

Definition
let τ be a replete tableau starting with X_{1},...,X_{k}. if τ is open, then X_{1},...,X_{k} is satisfiable 


Term

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

Definition
If S is a Hintikka set, then S is satisfiable
proof on pg. 19 


Term

Definition
X_{1},...,X_{k} is satisfiable if and only if there is no closed tableau starting with X_{1},...,X_{k} 


Term

Definition
A_{1},...,A_{k} is not satisfiable if and only if there exists a finite closed signed tableau starting with TA_{1},...TA_{k}, or equivalently a finite closed unsigned tableau starting with A_{1},...,A_{k} 


Term

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

Definition
B is a logical consequence of A_{1},...,A_{k} if and only if there exists a finite closed signed tableau starting ith TA_{1},...,TA_{k}, FB, or equivalently a finite closed unsigned tableau starting with A_{1},...,A_{k}, ¬B 


Term

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

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

Definition
an end node of T is a node with no (immediate) successors 


Term

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

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

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 nary 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

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 LU formulas is generated as follows:
1. an atomic LU formula is an expression of the form Pe_{1}e_{2}...e_{n} where P is an nary predicate of L and each e_{1}, e_{2},...,e_{n} is either a variable or an element of U
2. each atomic LU formula is an LU formula
3. If A is an LU formula, then ¬A is an LU formula
4. If A and B are LU formulas, then A Λ B, A V B, A→B, A↔B are LU formulas
5. If x is a variable and A is an LU formula then [image]xA and [image]xA are LU formulas 


Term

Definition
the degree of a formula is the number of occurences of propositional connectives ¬, Λ, V, →, ↔ and quantifiers [image],[image] in it 


Term

Definition
If U is a subset of U', then every LU formula is automatically an LU' formula. In particular, every Lformula is automatically and LU formula, for any set U 


Term

Definition
If A is an LU formula and x is a variable and a [image] U, we define an LU 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

Definition
an occurrence of a variable x in an LU 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 LU 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

Definition
an LU sentence is an LU formula in which no variable occur freely. an Lsentence is an LØ sentence, i.e., an LU sentence where U=Ø, the empty set 


Term
U^{n} is the set of ntuples of elements of U 

Definition
let U be a nonempty set, and let n be a nonnegative integer. U^{n} is the set of all ntuples of elements of U, i.e.,
U^{n}={<a_{1},...,a_{n}>a_{1},...,a_{n} [image] U}
An nary relation on U is a subset of U^{n} 


Term

Definition
Let L be a language. An Lstructure M consists of a nonempty set U_{M}, called the domain or universe of M, together with an nary relation P_{M} on U_{M} for each nary predicate P of L
an Lstructure may be called a structure, in situations where the language L is understood from context 


Term
valuations (predicate calculus) 

Definition
given an Lstructure M, there is a unique valuation or assignment of truth values
v_{M}: {A  A is an LU_{M} sentence} → {T,F}
defined on pg. 26 


Term
truth (predicate calculus) 

Definition
let M be an Lstructure. let A be an LU_{M} sentence. we say that A is true in M if v_{M}(A)=T. we say that A is false in M if v_{M}(A)=F 


Term
satisfaction (predicate calculus) 

Definition
let M be an Lstructure. let S be a set of LU_{M} 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 Lsentences. S is said to be satisfiable if there exists an Lstructure M which satisfies S 


Term

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 Lsentences 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 LU sentences is said to be satisfiable in the domain U if there exists an Lstructure M such that M [image] S and U_{M}=U 


Term

Definition
let S be a set of Lsentences. then S is satisfiable if and only if S is satisfiable in some domain U 


Term

Definition
let S be a set of Lsentences. if S is satisfiable in a domain U, then S is satisfiable in any domain of the same cardinality as U 


Term

Definition
fix a countably infinite set V={a_{1},a_{2},...,a_{n},...}={a,b,c,...}. the elements of V will be called parameters
if L is a language, LV 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) LV 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. 3132 


Term

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

Definition
an LV structure consists of an Lstructure M together with a mapping Φ: V→U_{M}. if A is an LV sentence, we write
A^{Φ}=A[a_{}_{1}/Φ(a),...,a_{}_{k}/Φ(a_{k})]
where a_{1},...,a_{k} are the parameters occurring in A. note that A^{Φ} is an LU_{M} sentence. note also that, if A is an Lsentence, then A^{Φ}=A 


Term
satisfiable  LV (predicate calculus) 

Definition
let S be a finite or countable set of (signed or unsigned) LV sentences. an LV structure M,Φ is said to satisfy S if v_{M}(A^{Φ})=T for all A [image] S. S is said to be satisfiable if there exists an LV structure satisfying S 


Term
satisfiable τ (predicate calculus) 

Definition
let τ be an Ltableau. we say that τ is satisfiable if at least one path of τ is satisfiable 


Term

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. 3537 


Term
the soundness theorem (predicate calculus) 

Definition
let X_{1},...,X_{k} be a finite set of (signed or unsigned) sentences with parameters. if there exists a finite closed tableau starting with X_{1},...,X_{k}, then X_{1},...,X_{k} is not satisfiable
proof on pg. 37 & notes 


Term

Definition
given a formula A, let A'=A[x_{1}/a_{1},...,x_{k}/a_{k}], where x_{1},...,x_{k} are the variables which occur freely in A, and a_{1},...,a_{k} 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

Definition
Look at pp. 3839 for useful logical equivalences 


Term

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

Definition
a formula is said to be quantifierfree if it contains no quantifiers. a formula is said to be in prenex form if it is of the form Q_{1}x_{1}...Q_{n}x_{n} B, where each Q_{i} is a quanitifier ([image] or [image]), each x_{i} is a variable, and B is quantifierfree



Term

Definition
let A be a formula. the universal closure of A is the sentence A*=[image]x_{1}...[image]x_{k} A, where x_{1},...,x_{k} are the variables which occur freely in A. note that A**≡A* 


Term
logical consequence (predicate calculus) 

Definition
let A_{1},...,A_{k},B be formulas. we say that B is a logical consequence of A_{1},...,A_{k} if (A_{1} Λ...Λ A_{k})→B is logically valid. this is equivalent to saying that the universal closure of (A_{1} Λ...Λ A_{k})→B is logically valid 


Term

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 LU sentence(predicate calculus) 

Definition
S is closed if A contains a conjugate pair of LU sentences. in other words, for some LU 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
Ureplete (predicate calculus) 

Definition
S is Ureplete if S "obeys the tableau rules" with respect to U
clauses are found on pp. 4041



Term
hintikka's lemma (predicate calculus) 

Definition
If S is Ureplete and open, then S is satisfiable. in fact, S is satisfiable in the domain U
proof on pp. 4142 & notes 


Term

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 Vreplete
proof on pp. 4243 


Term

Definition
let X_{1},...,X_{k} be a finite set of (signed or unsigned) sentences with parameters. if X_{1},...,X_{k} is not satisfiable, then there exists a finite closed tableau starting with X_{1},...,X_{k}. if X_{1},...,X_{k} is satisfiable, then X_{1},...,X_{k} 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. 4647 & notes 


Term

Definition
let S be a set of Lsentences
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

Definition
let S be a set of Lsentences. 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

Definition
1. a tautology is a propositional formula which is logically valid
2. a quasitautology is an LV sentence of the form F[p_{1}/A_{1},...,p_{k}/A_{k}], where F is a tautology, p_{1},...,p_{k} are the atoms occurring in F, and A_{1},...,A_{k} are LV sentences 


Term

Definition
a companion of A is any LV 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

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

Definition
a companion sequence of A is a finite sequence C_{1},...,C_{n} such that, for each i<n, C_{i+1} is a companion of
(C_{1} Λ...Λ C_{i})→A 


Term

Definition
if C_{1},...,C_{n} is a companion sequence of A, then A is logically valid if and only if (C_{1} Λ...Λ C_{n})→A is logically valid
proof on pp. 5253 


Term

Definition
A is logically valid if and only if there exists a companion sequence C_{1},...,C_{n} of A such that
(C_{1} Λ...Λ C_{n})→A
is a quasitautology
proof on pp. 5354 


Term

Definition
our Hilbertstyle proof system LH for the predicate calculus is as follows:
1. the objects are LV sentences
2. for each quasitautology A, <A> is a rule of inference
3. <([image]xB)→B[x/a]> and <B[x/a]→([image]xB)> are rules of inference
4. <A,A→B,B> is a rule of inference
5. <A→B[x/a], A→([image]xB)> and <B[x/a]→A, ([image]xB)→A> 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

Definition
LH is sound. in other words, for all LV sentences A, if A is derivable, then A is logically valid 


Term

Definition
LH is closed under quasitautological consequence. in other words if A_{1},...,A_{k} are derivable, and if B is a quasitautological consequence of A_{1},...,A_{k} then B is derivable
proof on pg. 57 


Term

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

Definition
LH is sound and complete. in other words, for all LV sentences A, A is derivable if and only if A is logically valid
proof on pg. 58 


Term

Definition
we write S [image] B to indicate that B is derivable in LH(S) 


Term

Definition
a language with identity consists of a language L with a particular binary predicate, I, designated as the identity predicate 


Term

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 nary predicate P of L, we have an axiom
[image]x_{1}...[image]x_{n}[image]y_{1}...[image]y_{n}((Ix_{1}y_{1} Λ...Λ Ix_{n}y_{n})→(Px_{1}...x_{n}↔Py_{1}...y_{n})) (congruence) 


Term

Definition
an Lstructure M is said to be normal if the identity predicate denotes the identity relation, i.e.,
I_{M}={<a,a>  a [image] U_{M}} 


Term

Definition
If M is an Lstructure satisfying the identity axioms for L, then we have a normal Lstructure M' satisfying the same sentences as M 


Term

Definition
S is normally satisfiable if there exists a normal Lstructure which satisfies S 


Term

Definition
let S be a set of Lsentences. 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

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. 7374 


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 nary 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 LU terms is generated as follows:
1. each variable is an LU term
2. each element of U is an LU term
3. if f is an nary operation of L, and if t_{1},...,t_{n} are LU terms, then ft_{1}...t_{n} is an LU term



Term

Definition
an atomic LU formula is an expression of the form
Pt_{1}...t_{n}
where P is an nary predicate of L, and t_{1},...,t_{n} are LU terms 


Term
structures (with operations) 

Definition
an Lstructure M consists of a nonempty set U_{M}, an nary relation P_{M }[image] (U_{M})^{n} for each nary predicate P of L, and an nary function f_{M}: (U_{M})^{n} → U_{M} for each nary operation f of L



Term

Definition


Term
valuations (with operations) 

Definition
let M be an Lstructure
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 

