Flashcards in Chapter 3: Definitions Deck (12)
Given a set of predicate symbols Π and a set of functional symbols Ω, with assigned arities, an L(Π, Ω)-structure consists of the following:
1) A non-empty set U.
2) For each predicate symbol P of arity n in Π, an n-ary predicate, or relation, PU on U.
3) For each functional symbol F of arity n in Ω, an n-ary functional, or function, FU on U, i.e. a functional FU : U n → U (if n = 0, FU corresponds to a specific, constant, element of U)
An occurrence of a variable symbol, x say, in a formula α, is said to be free if...
it is not within the scope of a ‘∀x’, i.e. if x is not present in a formula to which a ‘∀x’ applies
Otherwise, an occurrence of x within the scope of a ‘∀x’ is said to be bound (the x present within a ‘∀x’ string is also said to be bound).
A sentence is ....
a formula containing no free (occurrences of) variables.
The set of terms in a first order predicate language is defined, inductively, via:
(i) Each variable symbol is a term.
(ii) Each 0-ary functional symbol is a term.
(iii) If F is an n-ary functional symbol, and t1, · · · , tn are terms, then F t1 · · ·tn is a term.
A closed term is....
a term containing no variables
If, for a structure U, the sentence α satisfies αU = 1, then we say that
If there is a set T of sentences such that U |= s for each s ∈ T, then we write
α is true in U, or that α holds in/for U. Equivalently, we say that U models α, or that U is a model of α, and we write U |= α.
U |= T, and say that U models T, or that U is a model of T.
A theory in some (specified) language L(Π, Ω) is
a set of sentences in L(Π, Ω).
(∀x) (x = x)
(∀x)(∀y) ((x = y) ⇒ (y = x))
(∀x)(∀y)(∀z) (((x = y) ∧ (y = z)) ⇒ (x = z))
Let S be a subset of formulae in a first order predicate language L(Π, Ω) and α a formula in L(Π, Ω). Then, a proof of α from S is a finite, ordered sequence of formulae (or lines), t1, t2, · · · , tn say, such that tn is the formula α, and, such that, for each formula ti, 1 ≤ i ≤ n:
a) ti is an (occurrence of an) axiom, or
b) ti is a formula in S (we call such a formula a hypothesis), or
c) ti can be deduced by one of the two rules of deduction (modus ponens or generalisation) from
earlier lines, so that either:
(i) ti is a formula that can be deduced by modus ponens from two preceding formulae: ti is some formula β, and, for some j, k < i, tj is some formula α and tk is the formula α ⇒ β, or
(ii) ti is a formula that can be deduced by generalisation: ti is some formula (∀x)α, and, for some j < i, tj is the formula α, such that, for k < j, no free occurrence of x appears in any formula tk used to obtain the formula tj
Consider a subset S of the set of formulae in a first order predicate language L(Π, Ω), and a formula α in L(Π, Ω). Then, we say that S syntactically implies or proves α, and
S |- α
if there exists a proof of α from S (S being a set of hypotheses in this case)
If, within a first order predicate language, L(Π, Ω) say, there exists a proof of a formula α that uses only occurrences of the five given axioms, modus ponens and generalisation, then we say that α is
a theorem, i.e. α ∈ L(Π, Ω) is a theorem if ∅ |- α. In such a case, we may
also write |- α.