a set of propositional atoms p, q, r,....

an atomic L-formula is an atom of L

a finite sequence A₁, A₂,...,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 L-formulas.

A formation sequence for A is a formation sequence whose last term is A

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

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 ¬ →

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 2ⁿ different L-assignments

Given an L-assignment M, there is a unique L-valuation

v_M: {A | A is an L-formula} → {T,F}

given by clauses found on pg. 6

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.

B is a logical consequence of A₁, A₂,...,A_n if and only if (A₁ Λ A₂ Λ...Λ A_n) → B is logically valid.

B is logically valid if and only if ¬B is not satisfiable.

A signed formula is an expression of the form TA or FA, where A is a formula.

An unsigned formula is simply a formula

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

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

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

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

If S is a Hintikka set, then S is satisfiable

proof on pg. 19

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

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"

T is dyadic if each node of T has at most two immediate successors in T

Note that a dyadic tree is finitely branching

let T be an infinite, finitely branching tree. then T has an infinite path

proof on pg. 20 & notes

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

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"

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 Pe₁e₂...e_n where P is an n-ary predicate of L and each e₁, e₂,...,e_n 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

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]

let U be a nonempty set, and let n be a nonnegative integer. Uⁿ is the set of all n-tuples of elements of U, i.e.,

Uⁿ={<a₁,...,a_n>|a₁,...,a_n [image] U}

An n-ary relation on U is a subset of Uⁿ

Let L be a language. An L-structure M consists of a nonempty set U_M, called the domain or universe of M, together with an n-ary relation P_M on U_M 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

given an L-structure M, there is a unique valuation or assignment of truth values

v_M: {A | A is an L-U_M sentence} → {T,F}

defined on pg. 26

fix a countably infinite set V={a₁,a₂,...,a_n,...}={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

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

an L-V structure consists of an L-structure M together with a mapping Φ: V→U_M. if A is an L-V sentence, we write

A^Φ=A[a₁/Φ(a),...,a_k/Φ(a_k)]

where a₁,...,a_k are the parameters occurring in A. note that A^Φ is an L-U_M sentence. note also that, if A is an L-sentence, then A^Φ=A

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

let X₁,...,X_k be a finite set of (signed or unsigned) sentences with parameters. if there exists a finite closed tableau starting with X₁,...,X_k, then X₁,...,X_k is not satisfiable

proof on pg. 37 & notes

given a formula A, let A'=A[x₁/a₁,...,x_k/a_k], where x₁,...,x_k are the variables which occur freely in A, and a₁,...,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

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 Q₁x₁...Q_nx_n B, where each Q_i is a quanitifier ([image] or [image]), each x_i is a variable, and B is quantifier-free

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

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

S is U-replete if S "obeys the tableau rules" with respect to U

clauses are found on pp. 40-41

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

let τ₀ be a finite tableau. by applying tableau rules, we can extend τ₀ 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

let X₁,...,X_k be a finite set of (signed or unsigned) sentences with parameters. if X₁,...,X_k is not satisfiable, then there exists a finite closed tableau starting with X₁,...,X_k. if X₁,...,X_k is satisfiable, then X₁,...,X_k is satisfiable in the domain V

proof on pg. 43 & notes

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

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

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

1. a tautology is a propositional formula which is logically valid

2. a quasitautology is an L-V sentence of the form F[p₁/A₁,...,p_k/A_k], where F is a tautology, p₁,...,p_k are the atoms occurring in F, and A₁,...,A_k are L-V sentences

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

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

a companion sequence of A is a finite sequence C₁,...,C_n such that, for each i<n, C_i+1 is a companion of

(C₁ Λ...Λ C_i)→A

if C₁,...,C_n is a companion sequence of A, then A is logically valid if and only if (C₁ Λ...Λ C_n)→A is logically valid

proof on pp. 52-53

A is logically valid if and only if there exists a companion sequence C₁,...,C_n of A such that

(C₁ Λ...Λ C_n)→A

is a quasitautology

proof on pp. 53-54

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

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

LH is closed under quasitautological consequence. in other words if A₁,...,A_k are derivable, and if B is a quasitautological consequence of A₁,...,A_k then B is derivable

proof on pg. 57

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

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

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]x₁...[image]x_n[image]y₁...[image]y_n((Ix₁y₁ Λ...Λ Ix_ny_n)→(Px₁...x_n↔Py₁...y_n)) (congruence)

an L-structure M is said to be normal if the identity predicate denotes the identity relation, i.e.,

I_M={<a,a> | a [image] U_M}

let S be a set of L-sentences. S is normally satisfiable if and only if

S U {identity axioms for L}

is satisfiable

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

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 t₁,...,t_n are L-U terms, then ft₁...t_n is an L-U term

an atomic L-U formula is an expression of the form

Pt₁...t_n

where P is an n-ary predicate of L, and t₁,...,t_n are L-U terms

an L-structure M consists of a nonempty set U_M, an n-ary relation P_M [image] (U_M)ⁿ for each n-ary predicate P of L, and an n-ary function f_M: (U_M)ⁿ → U_M for each n-ary operation f of L

let M be an L-structure

pg. 79

the signed and unsigned tableau methods carry over to predicate calculus with operations. we modify the tableau rules as follows:

on pg. 80