Tutorials in English

Propositional logic

Classical propositional logic

A formula of propositional logic is in the conjunctive normal form (CNF) if it is a conjunction of (possibly many) disjunctions of (possibly many) propositinal variables and negated propositional variables. Eg., \((p_1\lor\lnot p_2\lor p_3)\land(p_2\lor p_4\lor \lnot p_5)\land(\lnot p_1\land p_2)\) is a CNF formula.

A formula of propositional logic is in \(k\)-CNF if it is in CNF and each disjunction has at most \(k\) disjuncts (variables or their negations). The formula given above is in 3-CNF, byt not in 2-CNF.

A formula of propositional logic is in the disjunctive normal form (DNF) if it is a disjunction of (possibly many) conjunctions of (possibly many) propositinal variables and negated propositional variables.

Exercise 1
Show that for each propositional formula \(\varphi\) there exists a propositional formula \(\psi\) in DNF, equivalent to \(\varphi\), i.e., \(\varphi\leftrightarrow\psi\) is a tautology.

Exercise 2
Show that for each propositional formula \(\varphi\) there exists a propositional formula \(\psi\) in CNF, equivalent to \(\varphi\), i.e., \(\varphi\leftrightarrow\psi\) is a tautology.

Exercise 3
Show that for each propositional formula \(\varphi\) in CNF there exists a propositional formula \(\psi\) in 3-CNF such that \(\psi\) is satisfiable if and only if \(\varphi\) is satisfiable.

Exercise 4
Give a polynomial time algorithm for the following decision problem:

Input: Propositional formula \(\varphi\) in DNF.
Question: Is \(\varphi\) satisfiable?

Exercise 5
Give a polynomial time algorithm for the following decision problem:

Input: Propositional formula \(\varphi\) in 2-CNF.
Question: Is \(\varphi\) satisfiable?

Exercise 6
We consider formulas built using connectives of conjunction and disjunction, only.
For such a formula \(\varphi\) let \(\hat{\varphi}\) denote its dualisation, i.e., the formula obtained from \(\varphi \) by replacing every occurrence of \(\wedge\) by \(\vee\) and every occurrence of \(\vee\) by \(\wedge\).

* Prove that \(\varphi\) is a tautology if and only if \(\lnot\hat{\varphi}\) is a tautology.

* Prove that \(\varphi\leftrightarrow\psi\) is a tautology if and only if \(\hat{\varphi}\leftrightarrow\hat{\psi}\) is a tautology.

* Propose a method to define dualisation for formulas contaning addtionally logical constants \(\bot\) and \(\top\), such that the above equivalences remain valid.

Exercise 7
Prove that for any function \(f:\{0,1\}^k\to\{0,1\}\) there exists a formula \(\varphi\) using only the connectives \(\to\) i \(\bot\) and variables from the set \(\{p_1,\ldots, p_k\}\) with the property that for any valuation \(\varrho\) the following equality holds:
\([[\varphi]]_\varrho = f(\varrho(p_1),\ldots, \varrho(p_k))\).
(In other words, the formula \(\varphi\) defines the function \(f\).)

Exercise 8
Consider an infinite set of lads, each of which has a finite number of fiancees. Moreover, for each \(k\in N\), any \(k\) lads has at least \(k\) fiancees. Demonstrate that it is possible to marry each lad with one of his fiancees, without commiting bigamy.

Exercise 9
Let \(k\) be a fixed natural number. Prove, using the compactness theorem, that if every finite subgraph of an infinite graph \(G=\langle V,E\rangle\) is \(k\)-collorable, then \(G\) itself is \(k\)-collorable, too.

Exercise 10
For the formula \(\gamma =\ r\leftrightarrow (p_1\lor p_2)\) the following equivalence holds: \(\varrho\models\gamma\) if and ony if \(\varrho(r)=\max(\varrho(p_1),\varrho(p_2))\).

Investigate whether there exists a set of formulas \(\Gamma\) such that \(\varrho\models\Gamma\) if and only if \(\varrho(r)=\max_{n\in\mathbb{N}}(\varrho(p_n))\).

Exercise 11
Is the sequent \(\{p,q\to p,\lnot q\}\vdash\{p,q\}\) provable in the Gentzen system for propositional logic?

Exercise 12
Decide if the following sequents are provable in the Gentzen system for propositional logic?

* \( (p\to q) \lor (q\to p)\)
* \((p\to ( q \to p)) \to p\)

Exercise 13
In the Gentzen system, the sequent \(\Gamma,p\vdash\Delta,p\) is an axiom, where \(p\) is a propositional variable. Prove that every sequent of the form \(\Gamma,\varphi\vdash\Delta,\varphi\) is provable in the Gentzen system. What can you assert about the size of this proof?

Three-valued propositional logics

Exercise 14
A logic \(L\) is called monotonic, if the conditions \(\Delta\models\varphi\) and \(\Gamma\supseteq\Delta\) imply \(\Gamma\models\varphi.\)

For a three-valued Sobociński logic we define that \(\Delta\models\varphi\), iff for every valuation of propositional variables into \(\{0,\frac12,1\}\), if the values of all sentences in \(\Delta\) are 1, then the value of \(\varphi\) is 1, too.

Is this logic monotonic?

Exercise 15
Answer the same question as in Exercise 14 for the logics of Heyting-Kleene-Łukasiewicz and Bochvar, as well as for the logic of lazy (short) Pascal evaluation.

Exercise 16
What is the computational complexity of the following decision problem:

Given: A formula \(\varphi\) of propositional logic.
Question: Is there a valuation \(\varrho\) of propositional variables into \(\{0,\frac12,1\}\) such that in the three-valued logic of Bochvar \([[\varphi]]_\varrho=1\)?

Intuitionistic propositional logic

Exercise 16
Prove the following formula in the Natural Deduction system for the intuitionistic logic
* \(p \to \neg \neg p\)
* \(\neg (p \lor q) \to\neg p \land\neg q\)
* \(\neg p \land\neg q \to\neg (p \lor q)\)
* \(\neg p \lor\neg q \to\neg (p \land q)\)

Exercise 17
Prove that the following formulas are not tautologies of the intuitionistic logic. Use Kripke models:

* \(((p\to q) \to p) \to p\)
* \(\neg (p \land q) \to (\neg p \lor\neg q)\)

Exercise 18

Prove inexpressibility of connectives in the intuitionistic logic:
* \(\lor\) can not be expressed using only \(\land\), \(\to\) and \(\bot\)
* \(\land\) can not be expressed using only \(\lor\), \(\to\) and \(\bot\)
* \(\to\) can not be expressed using only \(\lor\), \(\land\) and \(\bot\)

First order logic: formulas, models, tautologies

Exercise 1

Let \({\mathfrak A} =\langle{\mathbb N}, p^{\mathfrak A}, q^{\mathfrak A}\rangle\), where:

\(\langle a,b\rangle \in p^{\mathfrak A}\) iff \(a+b\geq 6\);

\(\langle a,b\rangle \in q^{\mathfrak A}\) iff \(b=a+2\).

Check if formulas

  1. \(\forall x p(x,y) \to \exists x q(x,y)\);
  2. \(\forall x p(x,y) \to \forall x q(x,y)\);
  3. \(\forall x p(x,y) \to \exists x q(x,z)\);

are satisfied under the valuation \(v(y) = 7\), \(v(z) = 1\) in structure \({\mathfrak A}\).

Exercise 2

Let \({\mathfrak A} = \langle {\mathbb Z}, f^{\mathfrak A}, r^{\mathfrak A}\rangle \) and \({\mathfrak B} = \langle {\mathbb Z}, f^{\mathfrak B}, r^{\mathfrak B}\rangle \), where \(f^{\mathfrak A}(m,n) = \min(m,n)\) for \(m,n\in{\mathbb Z}\), and \(r^{\mathfrak A}\) is the relation \(\geq\);

\(f^{\mathfrak B}(m,n) = m^2+n^2\) for \(m,n\in{\mathbb Z}\), and \(r^{\mathfrak B}\) is the relation \(\leq\).

Check if formulas

  1. \(\forall y(\forall x(r(z,f(x,y))\to r(z,y)))\);
  2. \(\forall y(\forall x(r(z,f(x,y)))\to r(z,y))\),

are satisfied under the valuation \(v(z) =5\), \(v(y)=7\) in structures \({\mathfrak A}\) and \({\mathfrak B}\).

Exercise 3

Is formula \(\forall x(\lnot r(x,y)\to\exists z(r(f(x,z),g(y))))\) satisfied under the valuation \(v(x) =3\), \(w(x) = 6\) and \(u(x) = 14\)

  1. in the structure \({\mathfrak A} = \langle {\mathbb N}, r^{\mathfrak A}\rangle \), where \(r^{\mathfrak A}\) is the divisibility relation?
  2. in the structure \({\mathfrak B} = \langle {\mathbb N}, r^{\mathfrak B}\rangle \), where \(r^{\mathfrak B}\) is the congruency modulo 7?

Exercise 4

In which structures is the formula \(\exists y (y\neq x)\) satisfied?
And the formula \(\exists y (y\neq y)\) obtained by naive substitution of \(y\) to \(x\)?

Exercise 5

Give examples of models and valuations such that the formula
\(p(x,f(x)) \to \forall x\exists y\, p(f(y),x)\)

is:
a) satisfied;
b) not satisfied.

Exercise 6

Check if the following formulas are tautologies an if they are satisfiable:

  1. \(\exists x\forall y(p(x) \vee q(y)) \to \forall y(p(f(y))\vee q(y))\);
  2. \(\forall y(p(f(y))\vee q(y)) \to \exists x\forall y(p(x) \vee q(y))\);
  3. \(\exists x(\forall y q(y)\to p(x))\to \exists x\forall y(q(y)\to p(x))\);
  4. \(\exists x(\forall y q(y)\to p(x)) \to\exists x(q(x)\to p(x))\).

Exercise 7

Let \(f\) be a function symbol of arity two, that is not used in the formula \(\varphi\).
Show that the formula \(\forall x\exists y \varphi\) is satisfiable if and only if the formula \(\forall x \varphi(f(x)/y)\) is satisfiable.

Exercise 8

Show that the formula \(\forall x\exists y\,p(x,y)\wedge \forall x\neg p(x,x)
\wedge \forall x\forall y\forall z(p(x,y)\wedge p(y,z)\to p(x,z))\) has only infinite models.

Exercise 9

For each \(n\) give a closed formula \(\varphi_n\) such that \({\mathfrak A}\models\varphi_n\) iff \({\mathfrak A}\) has exactly \(n\) elements.

Exercise 10

Show that for each finite structure \({\mathfrak A}\) over a finite signature there exists a set of first order formulas \(\Delta\) such that \({\mathfrak A}\models\Delta\) and for all structures satisfying \({\mathfrak B}\models\Delta\) it holds that \({\mathfrak B}\cong{\mathfrak A}.\)

Exercise 11

Is it true that \({\mathfrak A} \models \exists x\,\varphi\) implies existence of a term \(t\) such that \({\mathfrak A} \models \varphi[t/x]\)?

Exercise 12

Let \(\varphi = \forall x\forall y\,(y=f(g(x))\to(\exists u\,(u=f(x)\land y=g(u))))\) and \(\psi = \forall x\,[f(g(f(x)))=g(f(f(x)))]\). Does it hold that
\(\{\psi\}\models\varphi\)?

Hint
In exercises of the form "Show that the set of formulas \(\Delta\) is independent", one has to prove that for each \(\varphi\in\Delta,\) \(\Delta\setminus\{\varphi\}\not\models\varphi,\) by showing a model of \(\Delta\setminus\{\varphi\},\) which is not a model of \(\varphi.\)

Exercise 13

Show that the set of axioms of equivalence relation

\(\left\{\begin{array}[]{c}\forall x\forall y(Exy\to Eyx)\\ \forall x\ Exx\\ \forall x\forall y\forall z((Exy\land Eyz)\to Exz)\end{array}\right\}\)

is independent.

Exercise14

Show that the set of axioms of linear orders

\(\left\{\begin{array}[]{c}\forall x\forall y((x\leq y)\lor(y\leq x))\\ \forall x\forall y((x\leq y\land y\leq x)\to x=y)\\ \forall x\forall y\forall z((x\leq y\land y\leq z)\to x\leq z)\end{array}\right\}\)

is independent.

Exercise 15

Show that the set of axioms of of group theory (in multiplicative notation, over signature
\(\Sigma^{F}_{{2}}=\{*\},\Sigma^{F}_{0}=\{ 1\}\))

\(\left\{\begin{array}[]{c}\forall x((1*x=x)\land(x*1=x))\\ \forall x\forall y\forall z((x*y)*z=x*(y*z))\\ \forall x\exists y((x*y=1)\land(y*x=1))\end{array}\right\}\)

is independent.

Exercise 16

Show that the formula \((\forall x\exists y\ Exy)\to(\exists x\forall y\ Exy)\) is not a tautology.

Exercise 17

Show that the formula

\((\forall x\forall y((f(x)=f(y))\to(x=y)))\to(\forall x\exists y(f(y)=x))\)

is not a tautology. Does its negation have a finite model?

Exercise18

Show that the formula \(\exists x\exists y\exists u\exists v((\lnot u=x)\lor(\lnot v=y))\land(f(x,y)=f(u,v))\) is not a tautology. How many non-isomorphic finite models does this formula have?

Exercise 19

Show that the following formulas are tautologies:

  • \((\exists y p(y) \to \forall z q(z)) \to
    \forall y\forall z(p(y)\to q(z))\);
  • \((\forall x\exists y r(x,y) \to \exists x\forall y r(y,x))\to
    \exists x\forall y(r(x,y) \to r(y,x))\);
  • \(\forall x\exists y((p(x)\to q(y))\to r(y))
    \to ((\forall x p(x)\to \forall y q(y))\to \exists y r(y))\);
  • \(\forall x(p(x)\to \exists y q(y))\to
    \exists y(\exists x p(x)\to q(y))\).

Exercise 20

Does it hold that
\(
\{\forall x\underbrace{f\ldots f}_n(x)= x~|~n=2,3,5,7\}\models\forall x
\underbrace{f\ldots f}_{11}(x)= x
\)?

First order logic: formalizing properties

Exercise 1

For each pair of structures below give a closed formula that holds in one structure but not in the other:

  • \(\langle {\mathbb N},\leq\rangle\) and \(\langle \{m-{1\over n}\ |\ m,n\in{\mathbb N}-\{0\}\}, \leq\rangle\);
  • \(\langle {\mathbb N}, +\rangle\) and \(\langle {\mathbb Z}, +\rangle\);
  • \(\langle {\mathbb N}, \leq\rangle\) and \(\langle {\mathbb Z}, \leq\rangle\).

Exercise 2

Give examples of closed formulas \(\varphi\) and \(\psi\) such that

  • \(\varphi\) holds in \({\mathfrak A} = \langle {\mathbb Z}, +, 0 \rangle\), but not in \({\mathfrak B} = \langle {\mathbb N}, +, 0 \rangle\);
  • \(\psi\) holds in \({\mathfrak B} = \langle {\mathbb Z}, +, 0 \rangle\), but not in \({\mathfrak C} = \langle {\mathbb Q}, +, 0 \rangle\).

Exercise 3

Give an example of a first order formula

  • satisfiable in the field of real numbers, but not in the field of rational numbers;
  • satisfiable in the algebra \({\mathbb N}\) with multiplication, but not in the algebra \({\mathbb N}\) with addition;
  • satisfiable in \(\langle \{a,b\}^*,\cdot,\varepsilon\rangle\), but not in \(\langle \{a,b,c\}^*,\cdot,\varepsilon\rangle\).

Auxiliary definitions
Spectrum \(Spec(\varphi)\) of a closed formula \(\varphi\) is the set of natural numbers \(n\) such that \(\varphi\) has a model of cardinality \(n.\)

The standard model of arithmetics is the structure \(\mathfrak{N}=\langle\mathbb{N},*^{\mathfrak{N}},+^{\mathfrak{N}},0^{\mathfrak{N}},1^{\mathfrak{N}},\leq^{\mathfrak{N}}\rangle.\)

Exercise 4

Give an example of a closed formula \(\varphi\) (over a signature of your choice) such that \(Spec(\varphi)=Spec(\lnot\varphi).\)

Exercise 5

Give an example of a closed formula \(\varphi\) (over a signature of your choice) such that \(Spec(\varphi)=\{ n^{2}~/~n\in\mathbb{N}\}.\)

Exercise 6

Give an example of a closed formula \(\varphi\) (over a signature of your choice) such that \(Spec(\varphi)=\{ 2*n~/~n\in\mathbb{N}\}.\)

Exercise 7

Give an example of a closed formula \(\varphi\) (over a signature of your choice) such that \(Spec(\varphi)=\{ n~/~n\in\mathbb{N}\) and \(n\) is not a prime number\(\}\).

Exercise 8

Give an example of a closed formula \(\varphi\) (over a signature of your choice) such that \(Spec(\varphi)=\{ 2^{n}~/~n\in\mathbb{N}\}.\)

Exercise 9

Give an example of a closed formula \(\varphi\) (over a signature of your choice) such that for each natural number \(n,\) \(\varphi\) has exactly \(n\) non-isomorphic models of cardinality \(n.\)

Exercise 10

Give an example of a closed formula \(\varphi\) (over a signature of your choice) such that for each natural number \(n,\) \(\varphi\) has exactly \(2^{n}\) non-isomorphic models of cardinality \(n.\)

Exercise 11

Give an example of a closed formula \(\varphi\) (over a signature of your choice) such that for each natural number \(n,\) \(\varphi\) has exactly \(n!\) non-isomorphic models of cardinality \(n.\)

Exercise 12

For a given \(k\in\mathbb{N},\) give an example of a closed formula \(\varphi\) (over a signature of your choice) such that for each natural number \(n,\) \(\varphi\) has exactly \({n \choose k}\) non-isomorphic models of cardinality \(n.\)

Exercise 13

For a given \(k\in\mathbb{N},\) give an example of a closed formula \(\varphi\) (over a signature of your choice) such that for each natural number \(n,\) \(\varphi\) has exactly \(n^{k}\) non-isomorphic models of cardinality \(n.\)

Exercise 14

Give a formula \(\varphi(x,y)\) that holds in the standard model of arithmetics iff \(x\) and \(y\) are co-prime.

Exercise 15

Give a formula \(\varphi(x,y,z)\) that holds in the standard model of arithmetics iff \(z\) is the greatest common divisor of \(x\) and \(y.\)

Exercise 16

Give a formula \(\varphi(x,y,z)\) that holds in the standard model of arithmetics iff \(y\) is the greater number that is a power of a prime, which does not divide \(x.\)

Exercise 17

Consider finite directed cycles \(\mathfrak{C}\) over the signature containing a single binary relational symbol \(E\).

Show that for each natural number \(n\) there is a first order formula \(\varphi_n(x,y,z)\) using only three variables (which can be requantified as often as needed) such that for each finite cycle \(\mathfrak{C}\) the following equivalence holds: \(\mathfrak{C},x:a,y:b,z:c\models\varphi_n(x,y,z)\) iff \(\mathfrak{C}\) has \(3n\) edges, and the directed distances from \(a\) to \(b\), form \(b\) to \(c\), and from \(c\) to \(a\) are all equal to \(n\).

Exercise 18

Consider finite binary trees \(\mathfrak{T}\) over the signature consisting of two binary relational symbols \(L\) i \(P\), where \(L(x,y)\) means that \(y\) is the left son of \(x\), and similarly \(P\) denotes the right son. Each node can have 0, 1 or 2 sons, always at most one left and at most one right.

Show that for each natural \(n\) there is a closed first order formula \(\varphi _{n}\) using only two variables (which can be requantified as often as needed) such that for each finite binary tree \(\mathfrak{T}\) the following equivalence holds: \(\mathfrak{T}\models\varphi _{n}\) iff \(\mathfrak{T}\) is the full binary tree of depth \(n\).

First order logic and natural lanuguage

  1. Jak rozumiesz następujące zdania? Jak je sformułować, żeby nie budziły wątpliwości?
    • Nie wolno pić i grać w karty.
    • Nie wolno pluć i łapać.
    • Zabrania się zaśmiecania i zanieczyszczania drogi.[Kodeks Drogowy przed nowelizacją w roku 1997.]
    • Zabrania się zaśmiecania lub zanieczyszczania drogi. [Kodeks Drogowy po nowelizacji w roku 1997.]
    • Wpisać, gdy osoba ubezpieczona nie posiada numerów identyfikacyjnych NIP lub PESEL. [Instrukcja wypełniania formularza ZUS ZCZA (Zgłoszenie danych o członkach rodziny...)]
    • Podaj przykład liczby, która jest pierwiastkiem pewnego równania kwadratowego o współczynnikach całkowitych i takiej, która nie jest.
    • Warunek zachodzi dla każdego \(x\) i dla pewnego \(y\).
  2. Czy następujące definicje można lepiej sformułować?
    • Zbiór \(A\) jest dobry, jeśli ma co najmniej 2 elementy.
    • Zbiór \(A\) jest dobry, jeśli dla każdego \(x\in A\), jeśli \(x\) jest parzyste, to \(x\) jest podzielne przez \(3\).
    • Zbiór \(A\) jest dobry, jeśli dla pewnego \(x\in A\), jeśli \(x\) jest parzyste, to \(x\) jest podzielne przez \(3\).
  3. Wskazać błąd w rozumowaniu:
    • Aby wykazać prawdziwość tezy ,,Dla dowolnego \(n\), jeśli zachodzi warunek \(W(n)\) to zachodzi warunek \(U(n)\)'' załóżmy, że dla dowolnego \(n\) zachodzi \(W(n)\)...
    • Aby wykazać prawdziwość tezy ,,Dla pewnego \(n\), jeśli zachodzi warunek \(W(n)\) to zachodzi warunek \(U(n)\)'' załóżmy, że dla pewnego \(n\) zachodzi \(W(n)\)...
  4. Sformułować poprawnie zaprzeczenia stwierdzeń:
    • Liczby \(m\) i \(n\) są pierwsze.
    • Liczby \(m\) i \(n\) są względnie pierwsze.
  5. Czy zdanie ,,Liczba \(a\) nie jest kwadratem pewnej liczby całkowitej'' jest poprawnym zaprzeczeniem zdania ,,Liczba \(a\) jest kwadratem pewnej liczby całkowitej''?
  6. Zapisać następujące zdanie Lincolna o wyborcach i politykach:

    "You can fool some of the people all of the time, and all of the people some of the time, but you cannot fool all of the people all of the time"

    w terminach relacji \(fool(p,t)\) oznaczającej "you can fool person p at time t".

First order logic: Ehrenfeucht-Fraisse games

Ex. 1

Prove that there is no first-order sentence \(\varphi\) such that for every undirected (finite or not) graph \(\mathfrak{G}\) there is
\(\mathfrak{G}\models\varphi\) iff every vertex \(\mathfrak{G}\) belongs to a (finite) cycle in the graph.

Ex. 2

Prove that for any fixed finite graph \(\mathfrak{G}\) (this glyph is the gothic G) and any fixed \(m\in\mathbb{N}\), the following decision problem can be decided by a deterministic Turing machine that, in addition to a read-only input tape, has a working tape of length \(O(\log n)\), where \(n\) is the input size:

Given: an encoding of a finite graph \(\mathfrak{H}\) (gothic H) as an incidende matrix listed by rows.
Question: Does Player II have a winning strategy in the game \(G_m(\mathfrak{G},\mathfrak{H})\)?

Ex. 3

Prove that the class of all structures \(\mathbb{A}=\langle A,r^{\mathbb{A}}\rangle,\) where \(r\in\Sigma^{R}_{1}\) such that \(|r^{\mathbb{A}}|=|A\setminus r^{\mathbb{A}}|\) is not axiomatizable.

Ex. 4

Prove that the class of all structures \(\mathbb{A}=\langle A,E^{\mathbb{A}}\rangle\) over a signature that contains a single binary relation symbol \(E\), such that \(|\{(a,b)\in A\times A~/~(a,b)\in E^{\mathbb{A}}\}|< |\{(a,b)\in A\times A~/~(a,b)\notin E^{\mathbb{A}}\}|,\), is not axiomatizable.

Ex. 5

Prove that the class of all structures \(\mathbb{A}=\langle A,E^{\mathbb{A}}\rangle\) over a signature that contains a single binary relation symbol \(E\), such that \(E^{\mathbb{A}}\) is finite, is not definable.

Ex. 6

Prove that the class of all equivalence relations with finitely many equivalence classes is not axiomatizable.

Ex. 7

Let \(\mathfrak{H}^n\) be a structure whose carrier is the hypercube \(\{0,1\}^n\), where the only binary relation \(E^{\mathfrak{H}^n}\) is defined by:
\(E^{\mathfrak{H}^n}(x,y)\) iff \(x\) and \(y\) differ on exactly one position.

What is the largest \(m\) such that Player II has a winning strategy in the Ehrenfeucht-Fraisse game
\(G_m(\mathfrak{H}^4,\mathfrak{H}^3)\)?

Ex. 8

Prove that ther is no first-order sentence \(\varphi\) such that the every finite graph \(\mathfrak{G}\) there is \(\mathfrak{G}\models\varphi\) iff \(\mathfrak{G}\) has an Euler cycle.

Model theory for first order logic: compactness theorem, Skolem-Loewenheim theorem

Ex. 1

Show a set \(\Delta\) of first-order sentences such that every two countable models of \(\Delta\) are isomorphic, but there exist two uncountable, nonisomorphic models of \(\Delta.\)

Ex. 2

Let \(\Sigma\) be a finite signature. Prove that for every set \(\Delta\) of sentences over \(\Sigma,\) the following conditions are equivalent:

  1. \(\Delta\) has only finite models.
  2. \(\Delta\) has, up to isomorphims, only finitely many models.

Ex. 3

Prove that if a class \(\mathcal{A}\) of structures over a signature \(\Sigma\) is axiomatizable by a set of first-order sentences, and if its complement
\(Mod(\Sigma)\setminus\mathcal{A}\) is also axiomatizable by a set of first-order sentences, then both classes are definable by single first-order sentences.

Ex. 4

Prove the following Robinson theorem:
If \(\Delta,\Delta'\) are satisfiable sets of sentences over some signature \(\Sigma,\) but \(\Delta\cup\Delta'\) is not satisfiable, then there exists a sentence
\(\varphi\) such that \(\Delta\models\varphi\) and \(\Delta'\models\lnot\varphi.\)

Ex. 5

Let \(Spec(\varphi)\) denote the set of cardinalities of all finite models of a formula \(\varphi.\)
Prove that if \(\Delta\) is a set of sentences such that for each \(\varphi\in\Delta\) the set \(Spec(\lnot\varphi)\) is finite,
and if \(\Delta\models\psi,\) then \(Spec(\lnot\psi)\) is also finite.

Ex. 6

Prove that the class of all equivalence relations that have finitely many equivalence classes, is not axiomatizable.

Ex. 7

Prove that the class of al structures \(\mathbb{A}=\langle A,E^{\mathbb{A}}\rangle\) over a signature with a single binary relation symbol \(E\) such that \(E^{\mathbb{A}}\) is finite, is not axiomatizable.

Ex. 8

Prove that the class of all algebras \(\mathbb{A}=\langle A,f^{\mathbb{A}}\rangle,\) where \(f\) is a unary function symbol, such that \(|\vec{f}(A)|< |A|\), is not axiomatizable.

Ex. 9

Prove that the class of all structures \(\mathbb{A}=\langle A,E^{\mathbb{A}}\rangle\) over a signature with a single binary relation symbol \(E\) such that \(|\{(a,b)\in A\times A~/~(a,b)\in E^{\mathbb{A}}\}|< |\{(a,b)\in A\times A~/~(a,b)\notin E^{\mathbb{A}}\}|,\) is not axiomatizable.

Ex. 10

Prove that the class of all structures \(\mathbb{A}=\langle A,r^{\mathbb{A}}\rangle,\) where \(r\in\Sigma^{R}_{1}\) such that \(|r^{\mathbb{A}}|=|A\setminus r^{\mathbb{A}}|\) is not axiomatizable.

Zad. 11

Prove the following Hessenberg Theorem:
For each infinite cardinality \(\mathfrak{m}\), there is \(\mathfrak{m}^2=\mathfrak{m}.\)

Ex. 12

Prove that the class of all structures \(\mathbb{A}=\langle A,r^{\mathbb{A}}\rangle,\) where \(r\in\Sigma^{R}_{1}\) such that \(|r^{\mathbb{A}}|=2^{{|A\setminus r^{\mathbb{A}}|}}\) is not axiomatizable.

Ex. 13

Prove that the class of all structures isomorphic to a structure of the form \(\mathbb{A}=\langle\mathcal{P}(A),\cup^{\mathbb{A}},\cap^{\mathbb{A}},\subseteq^{\mathbb{A}}\rangle,\) where \(\cup^{\mathbb{A}},\cap^{\mathbb{A}}\) and \(\subseteq^{\mathbb{A}}\) are, respectively, the union, intersection and containment relations on sets, is not axiomatizable.

Zad. 14

Consider a signature with a binary function symbol \(\circ\), unary function symbol \(inv\) and a constant symbol \(id\). A model \(\mathfrak{F}\) (this is the gothic F, you may write ordinary F in the solution) over this signature is called a bijection group if its carrier is the set of all bijections \(f:A\to A\) on some set \(A,\) and the operations are interpreted as follows: \(\circ^{\mathfrak{F}}\) is function composition, \(inv^{\mathfrak{F}}\) is function inversion and \(id^{\mathfrak{F}}\) is the identity function on \(A\).

Prove that ther is no set \(\Gamma\) of first order sentences such that \(\mathfrak{B}\models\Gamma\) iff \(\mathfrak{B}\) is isomorphic to a bijection group.

Ex. 15

Prove that there is no first order sentence \(\varphi\) with the property that for each undirected (finite of not) graph \(\mathfrak{G}\) there is
\(\mathfrak{G}\models\varphi\) iff evert vertex of \(\mathfrak{G}\) belongs to a (finite) cycle in the graph.

Ex. 16

Does every set of sentences \(\Delta\) contain a minimal, wrt. inclusion, subset \(\Delta'\subseteq\Delta\) such that \(\Delta'\models\Delta\)?

Ex. 17

Prove that every finite set of sentences \(\Delta\) contains a subset \(\Delta'\subseteq\Delta\) such that \(\Delta'\models\Delta\) and that is independent, i.e., such that for each \(\varphi\in\Delta'\) there is \(\Delta'\setminus\{\varphi\}\not\models\varphi\).

Ex. 18

Let \(f\) be a unary function symbol, and let \(\mathcal{A}=\bigcup_{n\in\mathbb{N}}Mod(\forall x\underbrace{f\ldots
f}_n(x)=x).\)

Prove that \(\mathcal{A}\) cannot be axiomatized with any set of first order sentences, and the complement of \(\mathcal{A}\) cannot be defined with a single first-order sentence.

Logic and databases, relational algebra

Ex. 1

Let \(R,S\) be respectively \(n+m\)- i \(m\)-ary relational signature symbols.
Consider a new operation \(\div\) in relational algebra:

\([\![R\div S]\!]=\{\langle a_1,\dots,a_n\rangle|\) for each \(\langle b_1,\dots,b_m\rangle\in[\![S]\!]\ (\langle a_1,\dots,a_n,b_1,\dots,b_m\rangle\in[\![R]\!])\}\).

Show that the operator \(\div\) is expressible in terms of the other operators of relational algebra. Give an expression of relational algebra that defines \(R\div S\).


Definitions

Non-uniform class \(AC^0\) contains functions \(f:\{0,1\}^*\to\{0,1\}^*\) such that there is a polynomial \(p(n)\) and a constant \(c\) such that for every \(n\) there is a logical circuit \(C\) that computes \(f(x)\) for all \(x\in\{0,1\}^n\), which:

  1. has \(n\) input gates and \(m\) output gates
  2. is built from logical gates AND, OR and NOT
  3. input and logical gates can have arbitrarily many outputs
  4. gates AND and OR can have arbitrarily many inputs, NOT gates - only one input
  5. the number of gates in the circuit does not exceed \(p(n)\)
  6. the depth of the circuit does not exceed \(c\)

Non-uniform class \(NC^1\) contains functions \(f:\{0,1\}^*\to\{0,1\}\) such that there is a polynomial \(p(n)\) and a constant \(c\) such that for every \(n\) there is a logical circuit \(C\) that computes \(f(x)\) for all \(x\in\{0,1\}^n\), which:

  1. has \(n\) input gates and one output gate
  2. is built from logical gates AND, OR and NOT
  3. input and logical gates can have arbitrarily many outputs
  4. gates AND and OR must have exactly 2 inputs, NOT gates - only one input
  5. the number of gates in the circuit does not exceed \(p(n)\)
  6. the depth of the circuit does not exceed \(c\)

Ex. 2

Prove that with a suitable (natural) encoding of finite structures \(\mathfrak{A}\) as binary strings \(code(\mathfrak{A})\), for every sentence \(\varphi\) of first order logic, the function
\(f_\varphi:code(\mathfrak{A})\mapsto\) if \(\mathfrak{A}\models\varphi\) then \(1\) else \(0\)
belongs to non-uniform \(AC^0\).

Ex. 3

Prove that \(f_\varphi\) of the previous exercise, belongs to \(NC^1\).

Information In databases, an important optimization rule for relational algebra expressions tries to minimize the size of intermediate results obtained during query evaluation.

Ex. 4

Prove that the following problem is undecidable:

Data: a relational algebra expression \(E\) over a signature with a single binary symbol \(R\) and perhaps some other symbols.
Question: is \(|[\![E]\!]|<|[\![R]\!]|^2\) for every model?

Ex. 5

Relational algebra with total order can be constructed in two ways. Assume that \(\leq\) is a total order on all elements that appear in tuples, and there are no constants in the signature.

The first way is to introduce, to every database, an additional table (formally, a view) \(LEQ\) with two columns, containing all tuples
\(\langle a,b\rangle\) for \(a,b\) in the active domain, such that \(a\leq b\). Then ordinary expressions of relational algebra can use \(LEQ\)
as any other table. Then we treat \(LEQ\) as part of the query syntax, and not as an ordinary table.

Another way is to keep the tables as they are, but extend the syntax and in the condition \(\theta\) of selection \(\sigma_\theta(E)\) allow inequalities of the form \(i\leq j\) for \(i,j\) not larger than the number of columns in \(E\). Semantics is obvious, e.g. \([\![\sigma_{i\leq j}(E)]\!]=\{\vec{a}\in [\![E]\!]:a_i\leq a_j\}.\)

Prove that the queries expressible in both formalisms are the same.


Definition

The semijoin operator \(\gg\) of relational algebra has the following semantics (caution: I use a nonstandard symbol, as I could not produce the standard one with the available markers here):

\([\![R\gg_\theta S]\!]=\{\vec{a}\in [\![R]\!]~:~\exists \vec{b}\in[\![S]\!] \theta(\vec{a},\vec{b})\}\),
where \(\theta\) is a set of equalities between the columns of \(R\) and \(S\), numbered jointly.

For example, for binary \(R\) and \(S\)
\([\![R\gg_{1=3, 2=4} S]\!]=\{\langle a_1,a_2\rangle\in [\![R]\!]~:~\exists \langle b_1,b_2\rangle\in[\![S]\!]a_1=b_1\land a_2=b_2\}.\)

Ex. 6

Prove that semijoin is expressible in relational algebra, and define it using the other operators.

Ex. 7

Prove that expressions built of selection, projection, sum, difference and semijoin do not express all queries definable in relational algebra.

Ex. 8

Prove that every expression built of selection, projection, sum, difference and semijoin in a database where elements are natural numbers, can be computed in time \(O(n\log n),\) where \(n\) is the maximal number of tuples in relations.

Ex. 9

Prove that expressions built of projection, product, sum, difference and semijoin express all queries definable in relational algebra, provided there there are no constants in the signature.

Ex. 10

Prove that there is an expression built of selection, projection, sum, difference and semijoin, than defines the interestion of two relations.

Ex. 11

Prove that the following relational algebra operators are not expressible in terms of the others:

  • Sum is not expressible by selection, projection, product and difference.
  • Difference is not expressible by selection, projection, product and sum.
  • The other cases are very easy.

Ex. 12

Consider two tables \(A\) i \(B\) with two columns each. The first one has \(n_A\) rows.

Design an algorithm to calculate the relational algebra expression

\(A-\pi_{1,2}(\sigma_{1=3}(A\times B)).\)

You should assume that the active domain consist of integers, and table rows are indexed by nonnegative integers.

The algorithm should use exactly one table of two columns and \(n_A\) wierszy, and a few additional variables. Do not use pointers, recursion and other methods of implicit memory allocation.

Tables \(A\) and \(B\) are read-only, and you may assume that they are sorted.

Ex. 13

Let \(k\in\mathbb{N}\) be a constant. Prove that if \(E\) is a relational algebra expression and the maximal number of columns in subexpressions of
\(E\) is \(k\), then there is an agorithm to calculate the value of \([\![E]\!]\) in every structure \(\mathfrak{A}\) running in time \(O(n^{k}\log n),\) where \(n\) the size of the active domain of \(\mathfrak{A}\).

Decidability of logical theories

Zad. 1

Sygnatura składa się z jednego jednoragumentowego symbolu funkcyjnego \(f\). Niech \(\psi\) będzie zdaniem \(\forall x(f(f(x))=x\land \lnot f(x)=x)\).

  1. Udowodnić, że teoria \(\{\varphi\in FO~|~\psi\models\varphi\}\) jest rozstrzygalna.
  2. Udowodnić, że teoria \(\{\varphi\in FO~|~\psi\models\varphi\}\) należy do PSPACE.

Zad. 2

Sygnatura jest pusta. Niech \(\Gamma\) będzie zbiorem zdań \(\{\forall x_1\dots x_n\exists x_{n+1}(\bigwedge_{i=1}^n\lnot x_{n+1}=x_i)~|~n\in\mathbb{N}\}\).

  1. Udowodnić, że teoria \(\{\varphi\in FO~|~\Gamma\models\varphi\}\) jest rozstrzygalna.
  2. Udowodnić, że teoria \(\{\varphi\in FO~|~\Gamma\models\varphi\}\) należy do PSPACE.

Zad. 3

Udowodnić, że następujący problem decyzyjny jest nierozstrzygalny:
Dane:Formuła \(\varphi\) logiki pierwszego rzędu
Pytanie:Czy \(\varphi\) ma wyłącznie skończone modele?

Zad. 4

Wyjaśnić, jak można pogodzić ze sobą Zadania 2 i 3.

Zad. 5

Czy teoria pierwszego rzędu ciała liczb zespolonych \(\mathfrak{C}=\langle\mathbb{C},+,\cdot,0,1\rangle\) jest rozstrzygalna?

Linear Temporal Logic (LTL)

Zad. 1

Sformalizować w LTL własność "\(\varphi\) jest prawdziwe we
wszystkich parzystych stanach, a fałszywe we wszystkich nieparzystych"

Zad. 2
Pokazać, że nie da się w LTL sformalizować własności \(\varphi\)
jest prawdziwe we wszystkich parzystych stanach".

Zad. 3
Dokonać separacji kilku dodatkowych przypadków w dowodzie tw. Gabbaya.

Zad. 4
Jak można by sformułować twierdzenie o separacji dla logiki pierwszego rzędu, tak aby było ono prawdziwe?


Zad. 5
Proszę sformułować i udowodnić analogiczne twierdzenie o separacji dla monadycznej logiki drugiego rzędu.


Zad. 6

"Słaby until", oznaczany \(\mathtt{U}_w\), to temporalny operator dwuargumentowy taki, że \(\alpha\mathtt{U}_w\beta\) jest równoważna formule \((\alpha\mathtt{U}\beta)\lor\mathtt{G}\alpha\). ``Słaby until'' jest więc skrótem notacyjnym.

Wykazać, że dysponując operatorami \(\mathtt{X}\) i \(\mathtt{U}_w\) może zdefiniować standardowy unitl \(\mathtt{U}\).
Wynika stąd, że definicję logiki LTL można by równie dobrze oprzeć o słaby until.

Second order logic (SO) and monadic second order logic (MSO)

SO

Zad. 1

Pokazać, że dla każdego zdania \(\varphi\) logiki drugiego rzędu SO istnieje inne zdanie \(\varphi'\) tejże samej logiki takie, że
\(Spec(\varphi')=\mathbb{N}_+\setminus Spec(\varphi).\)

Zad. 2

Pokazać, że odpowiednik twierdzenia o zwartości nie zachodzi dla logiki drugiego rzędu.

Zad. 3

Napisać zdanie \(\Pi^1_1\), czyli uniwersalnego fragmentu logiki drugiego rzędu, którego wszystkimi modelami są dokładnie struktury skończone.

Zad. 4

Spróbować naszkicowac dowód tw. Fagina, że \(\Sigma^1_1=NP\) nad słowami (było sformułowane na wykładzie).

Zad. 5

Rozważamy skończone grafy \(\mathfrak{G}\) (ta litera to gotyckie G, w rozwiązaniu można pisać zwykłe G) nad sygnaturą składającą się z jednego dwuargumentowego symbolu relacyjnego \(E\).

Napisać zdanie \(\varphi\) logiki drugiego rzędu postaci \(\exists R_{1}\ldots\exists R_{k}\psi(R_{1},\ldots,R_{k}),\) w którym \(\psi\) jest zdaniem pierwszego rzędu takie, że dla każdego skończonego grafu \(\mathfrak{G}\) zachodzi równoważność: \(\mathfrak{G}\models\varphi\) wtw \(\mathfrak{G}\) ma cykl Eulera.

MSO

Zad. 1

Na wykładzie podany został dowód, że dla każdego zdania \(\varphi\) logiki MSO istnieje automat, który akceptuje dokładnie te słowa, w których \(\varphi\) jest prawdziwe.

Oszacować, jaki jest stosunek rozmiaru minimalnego deterministycznego automatu do długości formuły.


Zad. 2

Udowodnić, że każde zdanie MSO nad słowami jest równoważne zdaniu z tylko jednym kwantyfikatorem egzystencjalnym po relacji unarnej, w dodatku umieszczonym na początku.

Zad. 3

Skonstruować zdanie logiki MSO, które ma wyłącznie modele mocy co najmniej \(\mathfrak{c}\).

Zad. 4

Skonstruować zdanie logiki MSO, które ma wyłącznie modele mocy co najmniej \(2^{\mathfrak{c}}\).

Zad. 5

Skonstruować zdanie logiki MSO, którego spektrum to zbiór wszystkich liczb pierwszych.

Zad. 6

Rozważamy skończone grafy nieskierowane \(\mathfrak{G}\) (ta litera to gotyckie G, w rozwiązaniu można pisać zwykłe G) nad sygnaturą składającą się z jednego dwuargumentowego symbolu relacyjnego \(E\).

Napisać zdanie \(\varphi\) logiki MSO postaci \(\forall R_1\ldots\forall R_k\psi(R_1,\ldots,R_k),\) w którym \(\psi\) jest zdaniem pierwszego rzędu takie, że dla każdego skończonego grafu \(\mathfrak{G}\) zachodzi równoważność: \(\mathfrak{G}\models\varphi\) wtw \(\mathfrak{G}\) jest grafem acyklicznym.

Zad. 7

Napisać zdanie MSO, którego wszystkie skończone modele to dokładnie te grafy, które są 3-kolorowalne.

Zad. 8

Rozważamy modele dla PDL postaci skończonego łańcucha złożonego z dwóch programów atomowych: \(u\) i \(v\). Między każdymi dwoma kolejnymi stanami przechodzi jeden i tylko jeden z tych programów. Zmienne zdaniowe są dwie: \(p\) prawdziwa tylko w pierwszym stanie łańcucha i \(k\) prawdziwa tylko w ostatnim stanie. Innych zmiennych zdaniowych nie ma.

Każdą taką strukturę można naturalnie uważać również za strukturę pierwszego rzędu, wówczas \(u\) i \(v\) są relacjami dwuargumentowymi a \(p\) i \(k\) relacjami jednoargumentowymi.

Udowodnić, że dla każdego zdania \(\varphi\) logiki MSO istnieje zdanie \(\phi\) logiki PDL takie, że dla każdej struktury \(\mathfrak{A}\) jak powyżej, \(\phi\) jest prawdziwe w stanie początkowym struktury \(\mathfrak{A}\) wtedy i tylko wtedy, gdy \(\mathfrak{A}\models\varphi\).