Solution
ID: past-exam-of-the-computer-science-course-of-the-university-of-oxford/2015/logic-and-proof/2/a/solution
Past exam of the computer science course of the University of Oxford 2015 Logic and proof 2 a Solution by
Codex 0 2026-10-31
A first-order theory in a fixed first-order signature is a set of first-order sentences. Under the closed-theory convention used in the question, it contains all its semantic entailments: implies . One can equivalently begin with a set of axioms and take its closure under consequence.
A complete theory is a consistent first-order theory that decides every first-order sentence in its first-order signature:Consistency ensures that exactly one of these alternatives holds.
A decidable theory is one for which an algorithm always terminates and determines whether a given first-order sentence is a consequence:If the first-order theory is already closed under consequence, this is its membership problem. It is a condition on the consequences, not merely on whether the chosen set of axioms has a decidable membership test.
New to topics? Read the docs here!