TU Wien:Logic and Computability VU (Ciabattoni)/Written Exam 2025-01

Task 1: Is the following sequent calculus rule sound for classical logic?

If $\Gamma \vdash \neg A,\Delta$ and $\Gamma \vdash B,\Delta$ then $\Gamma \vdash A\lor B,\Delta$

Is it invertible? Provide either a proof or a counterexample.

Task 2: What can you say about the size of the models of the following formula?

$\neg \exists P(x,x)\land \forall uvw((P(u,v)\land P(v,w))\rightarrow P(u,w))\land \forall x\exists yP(x,y)$

Task 3: Is the set $\{x|\phi _{x}{\text{is not 1-1}}\}$ recursive, r.e. or none of them?

Task 4: Let $\phi _{a}$ be a computable function whose domain is not the empty set. Is the following function computable?

$g(i)=1{\text{ if }}D(\phi _{i})\cap D(\phi _{a})=\emptyset ,\uparrow {\text{ otherwise}}$

Task 5: Show via Robinson-resolution that the below clauses together are unsatisfiable. Specify all used factors, MGUs, and unified literals.

$C=q(a,x)\lor q(x,a)$

$D=\neg q(x,y)\lor q(g(x),g(x))$

$E=\neg q(g(g(x)),g(y))\lor \neg q(g(y),g(g(x)))$

Task 6: Prove or refute:

(a) $\Box \Box A\supset \Box A$ is valid in all transitive frames.

(b) The validity of $\neg A\lor \Diamond B\lor (B\supset \Box \Box A)$ in a frame ${\mathcal {F}}$ entails the transitivity of ${\mathcal {F}}$.

Task 7: Use the proof of the ADRF theorem to show that the following function is arithmetically definable (assuming $g$, $h$ are arithmetically definable):

$f(x,y,z)=g(h(x+3),2y*h(z))+1$