Notes - Logic and Proof MT24, First-order logic
Flashcards
Syntax
@Define a signature $\sigma$ in first-order logic.
- A set of constant symbols $c _ 1, c _ 2, \ldots$ (can be finite/infinite)
- A set of function symbols $f _ 1, f _ 2, \ldots$ (can be finite/infinite), each with associated arity $k > 0$.
- A set of predicate symbols $P _ 1, P _ 2, \ldots$ (can be finite/infinite)
Suppose:
- $\sigma$ is a signature which defines constant symbols, function symbols and predicate symbols
- $x _ 0, x _ 1, \ldots, \ldots$ are an infinite collection of variables
In this context, @define the set of $\sigma$-terms.
- Each variable is a term.
- Each constant symbol is a term.
- If $t _ 1, \ldots, t _ k$ are terms and $f$ is a $k$-ary function symbol, then $f(t _ 1, \ldots, t _ k)$ is a term.
Suppose:
- $\sigma$ is a signature which defines constant symbols, function symbols and predicate symbols
- $x _ 0, x _ 1, \ldots, \ldots$ are an infinite collection of variables
- $t _ 1, t _ 2, \ldots$ are the inductively-defined $\sigma$-terms
In this context, @define the set of fomulas in first-order logic.
- If $t _ 1, \ldots, t _ k$ are terms and $P$ is a $k$-ary function symbol, then $P(t _ 1, \ldots, t _ k)$ is a formula.
- If $F$ is a formula, $\lnot F$ is a formula
- If $F$ and $G$ are fomulas
- $(F \lor G)$ is a formula
- $(F \land G)$ is a formula
- If $F$ is a formula
- $\exists x F$ is a formula
- $\forall x F$ is a formula
Suppose:
- $\sigma$ is a signature which defines constant symbols, function symbols and predicate symbols
- $x _ 0, x _ 1, \ldots, \ldots$ are an infinite collection of variables
- $t _ 1, t _ 2, \ldots$ are the inductively-defined $\sigma$-terms
@Define an atomic formula in this context.
If $t _ 1, \ldots, t _ k$ are terms and $P$ is a $k$-ary function symbol, then $P(t _ 1, \ldots, t _ k)$ is an atomic formula.
Which is it: $\forall x F \land G$ is
- $\forall x (F \land G)$, or
- $(\forall x F) \land G$
In a formula $\exists x G$, what is the scope of $\exists x$?
What does it mean for a variable $x$ in a propositional formula to be bound/free?
If it is in the scope of some quantifier, it is bound, otherwise it is free.
Semantics
Suppose you have a signature $\sigma$ which defines
- A set of constant symbols $c _ 1, c _ 2, \ldots$ (can be finite/infinite)
- A set of function symbols $f _ 1, f _ 2, \ldots$ (can be finite/infinite), each with associated arity $k > 0$.
- A set of predicate symbols $P _ 1, P _ 2, \ldots$ (can be finite/infinite)
In this context, @define a $\sigma$-structure $\mathcal A$.
- A non-empty set $A$, called the universe of the structure
- For each $k$-ary predicate symbol $P$ in $\sigma$, a $k$-ary relation $P^{\mathcal A} \subset A^k$
- For each $k$-ary function symbol $f$ in $\sigma$, a $k$-ay function $f : A^k \to A$
- For each constant symbol $c$, an element $c^\mathcal A$ of $A$.
Suppose you have a signature $\sigma$ which defines
- A set of constant symbols $c _ 1, c _ 2, \ldots$ (can be finite/infinite)
- A set of function symbols $f _ 1, f _ 2, \ldots$ (can be finite/infinite), each with associated arity $k > 0$.
- A set of predicate symbols $P _ 1, P _ 2, \ldots$ (can be finite/infinite)
and a corresponding $\sigma$-structure $\mathcal A$:
- A non-empty set $A$, called the universe of the structure
- For each $k$-ary predicate symbol $P$ in $\sigma$, a $k$-ary relation $P^{\mathcal A} \subset A^k$
- For each $k$-ary function symbol $f$ in $\sigma$, a $k$-ay function $f : A^k \to A$
- For each constant symbol $c$, an element $c^\mathcal A$ of $A$.
In this context, can you inductively @define for each term $t$ a corresponding function $t^\mathcal A : A^n \to A$?
- If $t$ is a constant symbol$c$, then $t^\mathcal A (\pmb a) = c^\mathcal A$
- If $t$ is the variable $x _ i$, then $t^\mathcal A(\pmb a) = a _ i$
- If $t$ is a term $f(t _ 1, \ldots, t _ k)$, then $t^\mathcal A(\pmb a) = f^\mathcal A(t _ 1^\mathcal A(\pmb a), \ldots, t _ k^\mathcal A(\pmb a))$
Suppose:
- $\sigma$ is a signature
- $\mathcal A$ is a $\sigma$-structure
- $F$ is a first-order formula with free variables among $x _ 1, \ldots, x _ n$
- $\pmb a = (a _ 1, \ldots, a _ n)$
@Define the satisfaction relation
\[\mathcal A \models F(\pmb a)\]
.
It is defined inductively like so:
- $\mathcal A \models P(t _ 1, \ldots, t _ k)(\pmb a)$ if and only if $(t _ 1^\mathcal A(\pmb a), \ldots, t _ k^\mathcal A(\pmb a)) \in P^\mathcal A$
- $\mathcal A \models (F \land G)(\pmb a)$ if and only if $\mathcal A \models F(\pmb a)$ and $\mathcal A \models G(\pmb a)$
- $\mathcal A \models (F \lor G)(\pmb a)$ if and only if $\mathcal A \models F(\pmb a)$ or $\mathcal A \models G(\pmb a)$
- $\mathcal A \models (\lnot F) (\pmb a)$ if and only if $\mathcal A \not\models F(\pmb a)$
- If $F$ is $\exists y G(\pmb x, y)$ then $\mathcal A \models \exists y F(\pmb a)$ if and only if there exists $b \in A$ such that $\mathcal A \models G(\pmb a, b)$
- If $F$ is $\forall y G(\pmb x, y)$ then $A \models \forall x F(\pmb a)$ if and only if $\mathcal A \models F(\pmb a, b)$ for all $b \in A$
If working in first-order logic with equality, then:
- If $F$ is the formula $t _ 1 = t _ 2$, then $\mathcal A \models F(\pmb a)$ if and only if $t^\mathcal A(\pmb a) = t _ 2^\mathcal A(\pmb a)$.
@Define what it means for a first-order formula $F$ over a signature $\sigma$ to be satisfiable.
$\mathcal A \models F(\pmb a)$ for some $\sigma$-structure $\mathcal A$ and valuation $\pmb a$ of free variables in $F$.
@Define what it means for a first-order formula $F$ over a signature $\sigma$ to be valid.
$\mathcal A \models F(\pmb a)$ for every $\sigma$-structure $\mathcal A$ and valuation $\pmb a$ of free variables in $F$.
@Define the notation
\[\pmb S \models F\]
where $\pmb S$ is a set of first-order formulas over a signature $\sigma$.
Every $\sigma$-structure $\mathcal A$ that satisfies $\pmb S$ also satisfies $F$.
@Define what it means for a formula to be in prenex form, and what the matrix of the formula is.
The formula can be written
\[Q_1 y_1 Q_2 y_2 \cdots Q_n y_n F\]where each $Q _ i$ is a quantifier and $F$ contains no quantifiers. and $F$ is the matrix of the formula.
@Define what it means for a formula to be rectified.
No variable occurs both bound and free and all quantifiers in formula refer to different variables.
Suppose:
- $F$ is a first-order formula over a signature $\sigma$
- $x$ is a variable
- $t$ is a term
@Define
\[F[t/x]\]
The formula with $t$ substituted for every free occurences of $x$ in $F$.
@State the translation lemma.
Suppose:
- $t$ is a term built over variables $\pmb x$
- $F(\pmb x, y)$ is a formula such that no variable in $t$ occurs bound in $F$
- $b := t^\mathcal A(\pmb a)$
- $\mathcal A \models Ft/y$ iff $\mathcal A \models F(\pmb a, b)$.
What is meant by $\sigma$ being a “relational signature”?
It has only relation and constant symbols, no function symbols.