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$

\[(\forall x F) \land G\]

In a formula $\exists x G$, what is the scope of $\exists x$?


\[G\]

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.

Suppose $H$ is a formula with free variables $x _ 1, x _ 2, \ldots, x _ n$. @Define the universal closure $\forall^\ast H$.


\[\forall^\ast H = \forall x_1 \forall x_2 \cdots \forall x_n H\]



Related posts