Practice: First-order logic

First-order logic

Warm-upHuman

In the signature of fields $\{+, \cdot, -, 0, 1\}$ , which sentence says "every non-zero element has a multiplicative inverse"?

Choose one

\forall x\, \big(\neg(x = 0) \to \exists y\ (x \cdot y = 1)\big)

\exists y\, \forall x\, \big(\neg(x = 0) \to x \cdot y = 1\big)

\forall x\, \exists y\, \big(\neg(x = 0) \wedge x \cdot y = 1\big)

\forall x\ (x \cdot x^{-1} = 1)

First-order logic

Warm-upHuman

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.

Choose all that apply

\forall x\, \exists y\ E(x, y)

\exists y\, \forall x\ E(x, y)

\forall x\, \forall y\, \big(E(x, y) \to \neg E(y, x)\big)

\forall x\, \forall y\, \forall z\, \big(E(x, y) \wedge E(y, z) \to E(x, z)\big)

\forall x\, \exists y\, \exists z\, \big(E(x, y) \wedge E(y, z) \wedge E(z, x)\big)

First-order logic

CoreHuman

Which of these properties of a structure $(M, <)$ can be expressed by a single first-order sentence in the signature $\{<\}$ ? Choose all that apply.

Choose all that apply

There is a least element.Between any two elements there is a third.Every non-empty subset has a least element.There are exactly three elements.There are only finitely many elements.

First-order logic

CoreHuman

Which statement is the soundness theorem?

Choose one

If

\Gamma \vdash \varphi

then

\Gamma \models \varphi

.If

\Gamma \models \varphi

then

\Gamma \vdash \varphi

.Every consistent theory has a model.There is an algorithm deciding whether

\Gamma \vdash \varphi

.

First-order logic

CoreHuman

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?

Choose one

Step 2 is illegal:

\forall

I requires that

y

is not free in the assumptions, but

y

is free in

P(y)

.The derivation is correct.Step 1 is illegal: one cannot assume a formula with a free variable.It needs

\forall

E instead of

\forall

I.

First-order logic

CoreHuman

Which sentence proves that $(\mathbb{Z}, <)$ and $(\mathbb{Q}, <)$ are not isomorphic?

Choose one

\forall x\, \forall y\, \big(x < y \to \exists z\, (x < z \wedge z < y)\big)

\forall x\, \exists y\ (y < x)

\forall x\, \exists y\ (x < y)

"There are countably many elements."

First-order logic

StretchFormal

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?

Choose one

It makes the de Bruijn variable

0

fresh — it occurs free in no assumption — which is the eigenvariable condition of

\forall

I.It renames bound variables to avoid capture during substitution.It weakens the assumptions, so that fewer formulas are derivable.Nothing: it is needed only to make the types match.

First-order logic

CoreComputational

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)$ .

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.