TU Wien:Logic and Computability VU (Ciabattoni)/Oral Exam Questions 2022SS

Logic and Computability

Ciabattoni

Classical Logic

Compactness Theorem

Soundness and Completeness of the Propositional Sequent Salculus

• Soundness:
  • We want to check that Axiom ${\textstyle A\vdash A}$ is valid in classical logic and the inference rules of ${\textstyle LK'}$ preserve validity.
  • Axiom is valid since ${\textstyle A\vDash A}$ is trivially valid. Structural rules (Weakening, Contraction; Permutation) also trivial.
  • For logical rules investigate interpretation ${\textstyle v}$ s.t. all ${\textstyle A\in \Gamma }$ take value ${\textstyle 1}$ and all in ${\textstyle \Delta }$ value ${\textstyle 0}$, other cases are trivial.
• Completeness:
  • We can show that the calculus rules preserve validity when applied bottom up (similarly to soundness proof). Additionally, when applying rules bottom up the number of connectives will decrease and thus in a finite amount of steps we will reach sequents only containing atomic rules. If a formula ${\textstyle A\in \Gamma '\cap \Delta '}$, then ${\textstyle \Gamma '\vdash \Delta '}$ can be derived from ${\textstyle A\vdash A}$ using weakening rules.

Completeness of the Sequent Calculus for first-order Classical Logic

• We use the proposed proof search algorithm which ensures that all variables introduced in ${\textstyle (\forall r)}$ and ${\textstyle (\exists l)}$ do not appear free in the conclusion and for ${\textstyle (\forall l)}$ and ${\textstyle (\exists r)}$ all terms are potentially considered. If our algorithm finds a proof we are done, if not either:
  • one of the leafs is not an axiom
    • then we can define an interpretation based on the contained atomic formulas.
  • there is an infinite branch
    • this means the left and right side of the sequent have to be disjoint.
    • we can then construct an interpretation from the infinite branch
    • ?????

Löwenheim-Skolem Theorem

Overspill Lemma

- where ${\textstyle \exists ^{\geq n}}$ represents the formula ${\textstyle \exists x_{1},\dots x_{n}\bigwedge \limits _{i\neq j}\neg (x_{i}=x_{j})}$

Reachability Problem (non-expressibility in first-order logic)

Computability Theory

Non Existence of an Algorithm for each (decision) Problem

• Each decision problem can be seen as a function ${\textstyle f:{\mathcal {N}}\rightarrow \{0,1\}}$
  • Each algorithm computes a function
  • algorithms operate on various objects but we can encode them into ${\textstyle {\mathcal {N}}}$
• ${\textstyle \{f\ |\ f:{\mathcal {N}}\rightarrow \{0,1\}\}}$ is uncountable
• There are only countably many algorithms
  • There are ${\textstyle {\mathcal {N}}}$ algorithms
    • Let ${\textstyle S}$ be a formal system which describes algorithms
    • Let ${\textstyle A_{S}}$ be the set containing all algorithms in ${\textstyle S}$
    • Each algorithm in ${\textstyle A_{S}}$ computes a function ${\textstyle f:{\mathcal {N}}\rightarrow {\mathcal {N}}}$
    • Alphabet of ${\textstyle S}$ has a finite number of symbols
    • A bijection can now be built between ${\textstyle A_{S}}$ and ${\textstyle {\mathcal {N}}}$ by ordering the algorithms first according to the number of symbols and then lexicographically

Undecidability of the Halting Problem

Enumeration and s-m-n Theorem (intuitive proofs)

Fixed Point Theorem for computable Functions

Each Recursive Set is R.E.

Post Theorem

Equivalence between R.E. Sets and semi-decidable sets

• I r.e. ${\textstyle \implies }$ ${\textstyle \exists g}$ s.t. ${\textstyle R(g)=I}$ and ${\textstyle h}$ s.t. ${\textstyle D(h)=I}$ is
  • h(x) := …
    • is g(0) = x?
    • is g(1) = x?
    • …
• I semi-decidable ${\textstyle \implies }$ ${\textstyle \exists }$ total computable ${\textstyle g}$ s.t. ${\textstyle A=R(g)}$, where ${\textstyle R(g)=\{z\ |\ \exists xg(x)=z\}}$.
• Let ${\textstyle D(h)=I}$ and ${\textstyle g}$ s.t. ${\textstyle R(g)=I}$
  • if ${\textstyle I=\emptyset }$ then ${\textstyle I}$ is r.e. by definition
  • otherwise there ${\textstyle \exists k\in I}$. Using dovetailing ${\textstyle g(y)=\pi (x,n)=}$
    • x if ${\textstyle h(x)\downarrow }$ in n steps
    • k otherwise

Rice Theorem

Fermüller

Automated Deduction

Why is Herbrand’s Theorem important for automated deduction?

• A universal prenex formula ${\textstyle \forall x_{1}\dots \forall x_{n}\ F}$ is unsatisfiable iff there exists a finite unsatisfiable set ${\textstyle {\mathcal {F}}}$ of instances of the quantifier-free ${\textstyle F}$.
• Allows for instantiation of FOL formulas, these can then be treated like propositional formulas.
  • thus it provides a complexity reduction which is the base of automated deduction procedures

On what principles are state-of-the-art provers for first-order logic based?

• unification: compute most general unifiers
• atomic cut: propositional resolution rule (cut atom and its negation)

Can there be a computable function that bounds the size of the search space of a first-order prover in terms of the size of the input (formulas of set of clauses)? (Explain!)

• No:
  • then we would have a decision procedure (finite search space) and we know that validity of first order formulas is only semi-decidable.
  • if yes, we could limit the search space to a finite space which would make it decidable (i.e. FOL would no longer be undecidable)

What is the idea of structural clause forms? What can be gained (relative to traditional clause form translation) in terms of size of clause forms, minimal refutations, and search space, respectively?

• Introduce new predicate for each subformula, validity preserving
• Gain: only constant number of clauses for each subformula (usually worst case exponential), sometimes smaller refutations, larger search space since more variables (but smaller formulas at the same time)

What does ‘most general unification’ mean? Why is it so important for automated deduction? How does it occur there? Can it be implemented efficiently?

• Generality:
  • We say ${\textstyle E_{1}}$ is more general than ${\textstyle E_{2}}$ if ${\textstyle \exists \sigma }$ s.t. ${\textstyle E_{1}\sigma =E_{2}}$ holds.
  • A substitution ${\textstyle \sigma _{1}}$ is more general than ${\textstyle \sigma _{2}}$ if ${\textstyle \forall }$ expressions ${\textstyle E}$, ${\textstyle E\sigma _{1}}$ is more general than ${\textstyle E\sigma _{2}}$.
  • ${\textstyle \sigma }$ is a mgu of ${\textstyle E}$ if ${\textstyle \sigma }$ is a unifier of ${\textstyle E}$ and ${\textstyle \sigma }$ is more or equally general than any other unifier ${\textstyle \sigma '}$ of ${\textstyle E}$.
• Importance:
  • Yes, as we do not spoil future resolutions when applying them.
• Efiiciency
  • Yes, shown by Robinson and Martelli.

In what sense is Robinson resolution complete and sound?

• It is refutationally sound and complete, i.e.
  • if a formula is unsat, then we will be able to resolve to the empty clause

Why does one have to speak of refutational completeness? What exactly does this mean?

• Since binary/robinson resolution is not complete for satisfiable formulas
• if a formula is unsat, then we will be able to resolve to the empty clause

Why is binary resolution not complete in general? Can you give an example?

Why is binary resolution not complete in general?

Because we cannot apply factoring/renaming.

Can you give an example?

Yes, take two clauses $C$ and $D$ such that $C=\{P(x)\}$ and $D=\{\lnot P(y),\lnot P(z)\}$. We can use binary resolution to unify the first two literals of $C$ and $D$, but we need something more to get rid of the literal $\lnot P(z)$.

What is factorisation? Why is it needed?

• A p-reduction on a G-instance of a clause.
  • This means a smaller formula resulting in leaving out redundant literals after a renaming of a clause.

What is a semantic tree? How can we use it to prove completeness of resolution refinements and of redundancy elimination mechanisms (e.g., tautology elimination and subsumption)?

• Represents all Herbrand interpretations of a clause set ${\textstyle {\mathcal {S}}}$, where each branch induces an assignment of truth values to the herbrand base of ${\textstyle {\mathcal {S}}}$.
• ???
• Things that wont fail at any node of the tree can be removed from the set.

Why does one have to consider refinements (like A-orderings) in practice?

• This speeds up search.
• Since the number of resolvents grows exponentially, pruning possibilities is helpful.

Why is quantifier scope minimisation significant (in theory and) in practice?

• ???

Intuitionistic Logic/Constructivism

What is the basic difference between constructive and classical reasoning?

• constructive:
  • focus on verification, we can only assert truth after
  • epistemic (valid = invariantly known)proving/verifying it
• classical:
  • every statement is assumed to be either true or false
  • ontological (valid = invariantly true)

What is the (effective) disjunction principle? How does it relate to constructive existence?

• We can only assert ${\textstyle A\lor B}$ once we have proved either ${\textstyle A}$ or ${\textstyle B}$
• A proof of existence of an object has to inform us on how to construct the object.
• We can translate it to constructive existence.

Brouwer claimed that mathematics is more fundamental than logic. Which consequences/analogues can we formulate computer science? (Explain!)

• When investigating underlying logic one should derive logic from underlying principles and not other way around.
• Analysing programs:
  • first investigate what should be accepted asa good analysis of a model and then look at what that means for a good underlying logic

Why are intuitionistic proofs useful for programming? What is the Curry-Howard correspondence? Which types of programming languages are based on this relation?

• Because an intuitionistic proof delivers a process for constructing an object (i.e. using a program).
  • States that there mathematical proofs and computer programs are equivalent. (They represent the same kind of mathematics objects.)
  • A proof is a program and the formula it proves is the type for the program.
  • Functional languages

What does the Collatz (3n +1 problem) example illustrate?

• It is a conjecture which is widely accepted to be true, while no one has found a proof for its truth as of yet.
  • Halve even numbers, for odd: triple and then plus one and you will always end up at one for arbitrarily large integers.
• Very easily specifiable program which could not yet be verified, also interesting in terms of incompleteness.

What is the idea of BHK semantics? Explain the meaning of logical connectives and quantifiers according to that interpretation.

• An interpretation in BHK semantics defines how to prove a given formula.
• A connective is defined according to how you prove it.
• Provides semantics for IL.

Explain why tertium non datur is constructively unsound.

• Because the absence of a proof of a formula does not necessitate the existence of a proof for its negation.

Is ex falso quodlibet constructively sound? Why?

• Yes. If we can prove an inconsistency i.e. prove a formula as well as its negation, we can derive anything from this.

Can you name a few other classically valid formulas that are not intuitionistically valid?

• ${\textstyle \neg \neg A\supset A}$
• ${\textstyle (A\supset B)\lor (B\supset A)}$
• ${\textstyle \neg \forall x\neg A(x)\supset \exists xA(x)}$

Modal Logic

What is the basic idea of modal logic? What does ‘modal’ mean here?

• Developed in order to represent necessity and possiblity.
• The mode of assertion.

Why are there so many different modal logics?

• They allow modal logics to be applied in various different concepts, i.e. deontic, epistemic or temporal.

Can you name a few different possible interpretations of the Box-operator? Can you name different application scenarios in computer science where there interpretations are useful?

• temporal: always holds, talking about consistency of a system
• deontic: obligation, when trying to define AI for use in law
• epistemic: knows, when reasoning about knowledge of agents?

Can you derive the informal meaning of Diamond, given the informal meaning of Box? Why and how? (Illustrate with concrete examples)

• Yes, it is ${\textstyle \neg \square \neg F}$.

What is a Kripke frame? What is a Kripke interpretation?

• They are a version of possible world semantics.
  • Frame: ${\textstyle {\mathcal {F}}=\langle W,R\rangle }$
  • Interpretation: ${\textstyle {\mathcal {M}}=\langle W,R,V\rangle }$

What four levels of truth can be distinguished in modal logic?

• Truth in a world: ${\textstyle ({\mathcal {M}},w)\vDash A}$
• Truth in a model: ${\textstyle {\mathcal {M}}\vDash A}$
• Truth in a frame: ${\textstyle {\mathcal {F}}\vDash A}$
  • ${\textstyle A}$ is valid in ${\textstyle {\mathcal {F}}}$ if ${\textstyle A}$ is true in all interpretations of ${\textstyle {\mathcal {F}}}$
• Truth in a class of frames: ${\textstyle A}$ is true in ${\textstyle \phi }$ if ${\textstyle \forall {\mathcal {F}}\in \phi :{\mathcal {F}}\vDash A}$ - where ${\textstyle \phi }$ is a class (set) of frames

How does one specify a specific normal modal logic semantically?

• Using classes of frames determined by properties of the accessibility relation

Explain the purely syntactic notion of a ‘logic’. Why is it useful?

• A set of formulas which is:
  • closed under substitutions
  • closed under modus ponens
• I can compare different axiom schemes, different derivation rules, different Hilbert-type systems arising from either adding or removing certain axioms. So we can compare those logics then in the most basic way, namely in the ways of set inclusion. Is the one contained in the other or are they incomparable sets? That’s what we often want to know about logics.

What is the necessitation rule? Why is it sound?

• we can derive ${\textstyle \square F}$ from ${\textstyle F}$
• can be read like MP, if ${\textstyle F}$ can be derived so can ${\textstyle \square F}$
• since we are in Hilbert system there are no assumptions, thus you can only derive tautologies

Why is the deduction theorem (in it’s usual form) not valid for usual modal logics?

• We can always derive ${\textstyle \square F}$ from ${\textstyle F}$, but
• ${\textstyle F\supset \square F}$ does not hold in general
  • Counterexample: interpretation ${\textstyle {\mathcal {M}}=\langle \{u,v\},\{(u,v)\},V\rangle }$ and ${\textstyle V(F)=\{u\}}$

Incompleteness

How does Smullyan’s Gödelian puzzle relate to the incompleteness theorem(s)?

• Because the statement “I am not a knight” can neither be shown to be true or false in the given “system”.

Why do we need to use two different signs for natural numbers? What is the difference?

• To differentiate between the domain of the natural numbers and the structure of the natural numbers
  • ${\textstyle {\mathcal {N}}}$ … set of natural numbers
  • ${\textstyle \mathbb {N} }$ … structure of natural numbers

What is the difference between incompleteness in the sense of Theorem GT and Gödel-incompleteness?

• GT: If ${\textstyle \Sigma }$ is sound and ${\textstyle {\overline {P}}^{*}}$ expressible in it, then ${\textstyle \Sigma }$ is incomplete.
• Gödel-incompleteness: If ${\textstyle \Sigma }$ is sound and ${\textstyle {\overline {P}}^{*}}$ is expressible then ${\textstyle \Sigma }$ is Gödel incomplete.
• Difference: Gödel incomplete refers to a system containing formally undecidable sentences. (i.e. a sentence is contained neither in the provable nor refutable sentences of the system).

What is more difficult in general: deciding whether a given formula is true in all possible interpretations of whether it is true in a given concrete interpretation?

• In all possible interpretations, since things get more complicated when they are more concrete.
• Gödel showed:
  • Completeness of FOL holds on general level.
  • Incompleteness of FOL in arithmetic.

What is the difference between formal undecidability in Gödel’s sense and undecidability in the sense of computability theory? Can a theory with formally undecidable sentences be decidable? Can a theory ${\textstyle \mathbf {T} }$, where for each ${\textstyle F}$, either ${\textstyle F\in \mathbf {T} }$ or ${\textstyle \neg F\in \mathbf {T} }$ be undecidable?

• Gödel: sentences which are neither provable nor refutable.
• CT: sentences which we cannot decide

What is ‘true arithmetic’(${\textstyle \mathbf {TA} }$)? Why is it well defined? How does it compare with Peano Arithmetic (${\textstyle \mathbf {PA} }$)?

• The set of sentences that are satisfied in model ${\textstyle \mathbb {N} }$.
• ${\textstyle \mathbf {PA} }$ is ordinary FO-Logic plus peano axioms.
• The set is well defined, since we have a well defined notion of the true sentences.
• Peano: Induction axiom can only be described in second order logic or in FOL by using one axiom per predicate but
  • no. of predicates is countable
  • no. of sets of natural numbers is uncountable
  • this means we cannot describe some sets when using FOL representation

In what specific sense is arithmetical truth undefinable? Do you see a relation here with the liar paradox? In which sense is undefinability of truth different from (Gödel-)incompleteness?

In what specific sense is arithmetical truth undefinable?

In the sense of Tarski's Undefinability Theorem, which asserts that the set $T=\{\ulcorner S\urcorner ~|~\mathbb {N} \vDash S\}$ is not definable in Formal Arithmetic.

Do you see a relation here with the liar paradox?

No.

In which sense is undefinability of truth different from (Gödel-)incompleteness?

If we refer to arithmetic definability specifically, then we have that a number set $X$ is arithmetically definable/expressible if $n\in X\iff \mathbb {N} \vDash F({\hat {n}})$ for a given formula $F$. Therefore, (arithmetic) undefinability of a number set $X$ refers to the impossibility of finding a formula $F$ that expresses $X$, while (Gödel)-incompleteness refers to the impossibility of establishing the membership of every formula $S$ to either ${\mathcal {P}}$ or ${\mathcal {R}}$.

What is the ADRF Theorem? What is the proof idea?

• It states that all recursive functions are arithmetically definable.
• Church-Turing thesis: all computable functions are arithmetically definable
• We apply induction on the possible ways of function can be built.
  • Base: projection, constant-0 and successor
  • Inductive cases: composition, primitive recursion, minimisation. Show witness formula for definability.
  • Predicates can be coded as characteristic functions

How does one arithmetically define a function / a predicate / a number set?

• function: n+1-ary predicate with output as last parameter
• predicate: characteristic function
• number set: formula takes free variable and is true iff corresponding number is in set

What is Gödel’s second incompleteness theorem? Why was it considered to be even more important than his first incompleteness theorem in 1931?

• If the provability predicate for a proof system ${\textstyle \Pi }$ is representable in ${\textstyle \Pi }$ and satisfies the provability conditions then ${\textstyle \neg B(\ulcorner 0<0\urcorner )}$ is only provable if ${\textstyle \Pi }$ is inconsistent.
  • provability conditions: (using provability predicate ${\textstyle B(v)}$ describing provability)
    • ${\textstyle \vdash _{\Pi }S}$ then ${\textstyle \vdash _{\Pi }B(\ulcorner S\urcorner )}$
    • ${\textstyle \vdash _{\Pi }B(\ulcorner S\subset T\urcorner )\supset (B(\ulcorner S\urcorner )\supset B(\ulcorner T\urcorner ))}$
    • ${\textstyle \vdash _{\Pi }B(\ulcorner S\urcorner )\supset B(\ulcorner B(\ulcorner S\urcorner )\urcorner )}$
• Because it showed that the Hilbert problem of finding a proof of consistency using an elementary system (not stronger than arithmetic) could not be positively solved.

How are incompleteness and undecidability related? What phenomenon was shown first? By whom? Can one derive one from the other?

• We know every sound proof system for formal arithmetic is incomplete.
• From the incompleteness theorem we get undecidability of ${\textstyle \mathbf {TA} }$ as a corollary, it is complete and can thus not be decidable.
• Undecidability came later.
• If we can encode undecidable problem in a system and it is sound, then our system must be incomplete.
• The other way is less immediate but can also be derived.

What is the significance of incompleteness for software verification?

• From incompleteness we know that there cannot be a proof system that allows verification of all programs in a reasonably rich language.
• If you fix a proof system for establishing program correctness then there are cases which cannot be verified by the system.