The Lumenary · Early undergraduate

First-order logic

Name: ______________________

Date: ______________________

You will learn to

Write first-order formulas in a given signature, such as the axioms for groups, linear orders and fields, and recognise statements that are not first-order
Decide whether a sentence is true in a given structure by unwinding the definition of satisfaction
Use natural deduction to derive simple consequences, and prove the soundness theorem $\Gamma \vdash \varphi \Rightarrow \Gamma \models \varphi$
Prove that isomorphic structures satisfy the same sentences, and use sentences and countermodels to show non-isomorphism and non-derivability
State Gödel's completeness theorem and distinguish $\models$ from $\vdash$

1.
In the signature of fields $\{+, \cdot, -, 0, 1\}$ , which sentence says "every non-zero element has a multiplicative inverse"?
- A. $\forall x\, \big(\neg(x = 0) \to \exists y\ (x \cdot y = 1)\big)$
- B. $\exists y\, \forall x\, \big(\neg(x = 0) \to x \cdot y = 1\big)$
- C. $\forall x\, \exists y\, \big(\neg(x = 0) \wedge x \cdot y = 1\big)$
- D. $\forall x\ (x \cdot x^{-1} = 1)$
2.
Let $\mathcal{C} = (\{1, 2, 3\}, E)$ with $E = \{(1,2), (2,3), (3,1)\}$ (a directed triangle). Which sentences are true in $\mathcal{C}$ ? Choose all that apply.
- A. $\forall x\, \exists y\ E(x, y)$
- B. $\exists y\, \forall x\ E(x, y)$
- C. $\forall x\, \forall y\, \big(E(x, y) \to \neg E(y, x)\big)$
- D. $\forall x\, \forall y\, \forall z\, \big(E(x, y) \wedge E(y, z) \to E(x, z)\big)$
- E. $\forall x\, \exists y\, \exists z\, \big(E(x, y) \wedge E(y, z) \wedge E(z, x)\big)$
3.
Which of these properties of a structure $(M, <)$ can be expressed by a single first-order sentence in the signature $\{<\}$ ? Choose all that apply.
- A.There is a least element.
- B.Between any two elements there is a third.
- C.Every non-empty subset has a least element.
- D.There are exactly three elements.
- E.There are only finitely many elements.
4.
Which statement is the soundness theorem?
- A.If $\Gamma \vdash \varphi$ then $\Gamma \models \varphi$ .
- B.If $\Gamma \models \varphi$ then $\Gamma \vdash \varphi$ .
- C.Every consistent theory has a model.
- D.There is an algorithm deciding whether $\Gamma \vdash \varphi$ .
5.
Someone "derives" $P(y) \vdash \forall x\, P(x)$ as follows: (1) $P(y) \vdash P(y)$ by assumption; (2) $P(y) \vdash \forall x\, P(x)$ by $\forall$ I. Which statement is right?
- A.Step 2 is illegal: $\forall$ I requires that $y$ is not free in the assumptions, but $y$ is free in $P(y)$ .
- B.The derivation is correct.
- C.Step 1 is illegal: one cannot assume a formula with a free variable.
- D.It needs $\forall$ E instead of $\forall$ I.
6.
Which sentence proves that $(\mathbb{Z}, <)$ and $(\mathbb{Q}, <)$ are not isomorphic?
- A. $\forall x\, \forall y\, \big(x < y \to \exists z\, (x < z \wedge z < y)\big)$
- B. $\forall x\, \exists y\ (y < x)$
- C. $\forall x\, \exists y\ (x < y)$
- D."There are countably many elements."
7.
In the Lean formalisation, the rule allI : Derivable (Γ.map Formula.shift) φ → Derivable Γ (.all φ) shifts every assumption (variable $i$ becomes $i + 1$ ) before deriving the body φ. What does the shift achieve?
- A.It makes the de Bruijn variable $0$ fresh — it occurs free in no assumption — which is the eigenvariable condition of $\forall$ I.
- B.It renames bound variables to avoid capture during substitution.
- C.It weakens the assumptions, so that fewer formulas are derivable.
- D.Nothing: it is needed only to make the types match.
8.
On a finite domain, quantifiers are loops. Write forall(domain, pred) and exists(domain, pred), and use them to write serial(domain, rel), which decides $\forall x\, \exists y\ R(x, y)$ for a relation rel given as a set of pairs, and has_hub(domain, rel), which decides $\exists y\, \forall x\ R(x, y)$ .
Computational — Practice

Answer key — First-order logic

1.
$\forall x\, (\neg(x = 0) \to \exists y\ x \cdot y = 1)$ . The witness $y$ depends on $x$ , so $\exists y$ comes after $\forall x$ ; and the restriction to non-zero $x$ is expressed with an implication.
2.
True: $\forall x\, \exists y\, E(x,y)$ (witnesses $2, 3, 1$ ), asymmetry, and the 3-cycle statement. False: $\exists y\, \forall x\, E(x,y)$ (fails at $x = y$ ) and transitivity (fails for $1, 2, 3$ ).
3.
Least elements, density and "exactly three elements" are first-order. Well-ordering quantifies over subsets (second-order), and finiteness is not expressible by any set of first-order sentences (compactness; see the lesson on completeness).
4.
Soundness: $\Gamma \vdash \varphi \Rightarrow \Gamma \models \varphi$ . Completeness is the converse $\Gamma \models \varphi \Rightarrow \Gamma \vdash \varphi$ , equivalently "every consistent set of sentences has a model".
5.
$\forall$ I from $\Gamma \vdash \varphi[y/x]$ to $\Gamma \vdash \forall x\, \varphi$ requires $y$ not free in $\Gamma$ . Here $\Gamma = \{P(y)\}$ contains $y$ free, so step 2 is illegal. The sequent is in fact underivable: by soundness it would be a semantic consequence, but $(\{0, 1\}, P = \{0\})$ with $y \mapsto 0$ is a countermodel.
6.
Density, $\forall x\, \forall y\, (x < y \to \exists z\, (x < z \wedge z < y))$ , holds in $(\mathbb{Q}, <)$ and fails in $(\mathbb{Z}, <)$ . Since isomorphic structures satisfy exactly the same sentences, the two orders are not isomorphic — although there is a bijection $\mathbb{Z} \to \mathbb{Q}$ .
7.
Shifting the assumptions renumbers their free variables $i \mapsto i + 1$ , so none of them mentions variable $0$ . Deriving φ from them therefore proves it for an arbitrary value of variable $0$ — the eigenvariable condition. Without it the rule would derive $\forall x\, P(x)$ from $P(x_0)$ , and soundness (Lumenary.FirstOrderLogic.soundness) would fail.
8.
```
def forall(domain, pred):
    return all(pred(a) for a in domain)

def exists(domain, pred):
    return any(pred(a) for a in domain)

def serial(domain, rel):
    return forall(domain, lambda x: exists(domain, lambda y: (x, y) in rel))

def has_hub(domain, rel):
    return exists(domain, lambda y: forall(domain, lambda x: (x, y) in rel))
```
This is Tarski's definition as code: $\forall$ is all over the domain and $\exists$ is any. The tests on the empty domain show why standard first-order logic insists on non-empty structures: there $\forall x\, \varphi$ is always true and $\exists x\, \varphi$ always false, so $\forall x\, \varphi \to \exists x\, \varphi$ would fail. On infinite domains the loops never finish, which is why truth in infinite structures needs proof rather than search.