Past exam of the year 1 of the computer science course of the University of Oxford / 2023 / Digital systems, linear algebra and introduction to formal proof / Introduction to formal proof

Use $0$ and $1$ for false and true truth values. The truth table is:

The two satisfying rows with $A=B=1$ combine by eliminating $C$, while the remaining satisfying row has $A=B=0,C=1$. An equivalent disjunctive normal form is thereforeExpanding the logical biconditional into its two implications, and using $\neg B\to C\equiv B\vee C$, gives the conjunctive normal formEach form has exactly the same three satisfying assignments as the original propositional formula.

Apply structural induction to the formation of a propositional formula. Let $L(\theta )$ and $R(\theta )$ count its opening and closing parentheses, and use the usual grammar generated by propositional variables, any allowed truth constants, negation, and parenthesized binary logical connectives.

An atomic variable or truth constant contains neither kind of parenthesis, so $L=R=0$. If $L(\alpha )=R(\alpha )$, prefixing negation leaves both counts unchanged. If the notation writes a negated formula with an extra pair of parentheses, it adds one to each and still preserves equality.

For a binary construction $(\alpha \circ \beta )$, where $\circ$ is an allowed binary logical connective,The two induction hypotheses make these equal. Every grammar construction preserves the property, so every propositional formula contains equally many left and right parentheses. This is balanced parentheses in propositional syntax.

Apply the propositional substitution simultaneously to the atomic variables:By distributivity and the complementary literals $Y,\neg Y$,The other disjunct simplifies using logical implication and absorption:Thus $\phi S\equiv X\vee \neg X\equiv \top$, a tautology.

Interpret $x_1,\dots ,x_n$ as the bits of a binary number, with $x_1$ most significant. Construct a propositional formula saying that this number is strictly less than $k$. This gives a quadratic-size formula with prescribed model count.

For $0<k<2^n$, write $k=(b_1\cdots b_n{)}_2$. For each $i$ with $b_i=1$, define the conjunctionThe empty prefix for $i=1$ is omitted. Let ${\phi }_k={\bigvee }_{i:b_i=1}{T}_i$. A Boolean valuation satisfies $T_i$ exactly when its first difference from the binary representation of $k$ is at position $i$, changing a one of $k$ to a zero. All later bits are unrestricted. Hence these cases are disjoint and cover exactly the numbers $0,\dots ,k-1$.

Alternatively, counting the disjoint cases directly givesEach $T_i$ has length $O(i)$, including its logical connectives and parentheses; the total length is at most a constant multiple of ${\sum }_{i=1}^{n}i=O(n^2)$. The endpoints are ${\phi }_0=\perp$ and ${\phi }_{2^n}=\top$. If constants are unavailable and $n\ge 1$, use $x_1\wedge \neg x_1$ and $x_1\vee \neg x_1$ instead. Assignments are counted over all $n$ specified variables, including any absent from the formula. For $n=0$, the constants describe the two possible counts, zero and one. Thus the construction covers $0\le k\le 2^n$, including the endpoint zero despite the source's word “positive”.

For example, $n=4,k=11=(1011{)}_2$ gives the disjoint cases $0\ast \ast \ast$, $100\ast$ and $1010$, with $8+2+1=11$ satisfying assignments.

Keep the premise $P\to Q$ open. Assume $Q\to \neg P$, then temporarily assume $P$. Two applications of the implication elimination rule produce $Q$ and then $\neg P$, contradicting the temporary $P$. Discharge $P$ using the negation introduction rule, then discharge $Q\to \neg P$ using the implication introduction rule.This natural deduction proof uses only the supplied introduction and elimination rules. Line 6 is an application of the negation elimination rule; no classical contradiction principle is needed.

The nonempty simple graphs having an independent vertex cover of size at most two. The witnesses $x,y$ select the cover. The clause $\neg E(x,y)$ makes the selected vertices nonadjacent; the universal clause forbids every edge whose two endpoints both lie outside the selected set.

The witnesses need not be distinct, so a one-vertex cover is permitted by choosing $x=y$. A nonempty edgeless graph also satisfies the formula. The empty graph does not, because the existential quantifiers have no witnesses. Here independent vertex cover has its standard vertex cover meaning; 8(b)'s differing parenthetical definition is addressed separately below.

The source's explicit parenthetical condition is domination: every unselected vertex has a neighbour in the selected set. Together with independence this defines an independent dominating set. A first-order sentence expressing that definition with size at most three isThe finite conjunctions and disjunctions abbreviate three explicitly fixed terms, so this is a first-order formula. Repeated witnesses allow one- or two-element choices; the first conjunction enforces independence only between distinct selected vertices. The last clause says that every vertex is selected or adjacent to a selected vertex. With the usual nonempty-domain convention, any such choice has size at least one, so repeated witnesses cover all possibilities of size at most three.

For the standard meaning of independent vertex cover, replace the domination clause byThis instead demands that every edge has a selected endpoint. These interpretations differ: in a triangle in a graph, any singleton is an independent dominating set, but no independent vertex cover exists. Giving both clauses avoids silently treating the source's two definitions as equivalent.

Read the initial universal quantifiers as governing the conjunction of irreflexivity and transitivity. Explicitly, the intended first-order sentence assertsThus $Q$ is an irreflexive relation, a transitive relation, and a serial relation.

Suppose a first-order model had a finite nonempty domain of cardinality $N$. Choose $a_0$. Seriality supplies successive elements $a_1,\dots ,a_N$ with $Q(a_i,a_{i+1})$. By the pigeonhole principle, $a_i=a_j$ for some $i<j$. Repeated transitivity along that part of the chain gives $Q(a_i,a_j)=Q(a_i,a_i)$, contradicting irreflexivity. Hence there is no finite nonempty model. This is the infinite-model property of a serial strict partial order.

An infinite model exists: take domain $\mathbb{N}$ and $Q(x,y)$ to mean $x<y$. It is irreflexive and transitive, and $y=x+1$ witnesses seriality for every $x$.

The quantifier-scope convention matters: giving each printed universal quantifier only the immediately following atomic scope would leave the transitivity implication with free variables and would not express the claimed theorem. The explicit parenthesisation above records the reading under which the source's requested assertion is valid.

Use broad scope up to the enclosing parenthesis, consistent with (c). Thus the first conjunct is read as$f(u,t)$ is not free for substitution for $z$. The free occurrence of $z$ in $Q(z,t)$ lies under $\exists t$; inserting $f(u,t)$ there would capture its $t$. Rename that bound variable to a fresh $s$ first, using alpha equivalence. The capture-avoiding first-order substitution is thenEvery occurrence of $z$ in the original formula is free, so all four are replaced. The variable $t$ introduced by the term remains free, and the final $\exists yQ(y,y)$ is unchanged.

Under the same scope convention, $g(t,z)$ is not free for substitution for $y$. The occurrence of $y$ inside $Q(f(x,y),f(z,z))$ is free but lies under $\exists t$, so its replacement would capture the new $t$. Rename this binder to fresh $s$. Substitute only for the free $y$ occurrences in the first conjunct:The two occurrences of $y$ in the final conjunct are bound variables and remain unchanged. The inserted $t,z$ remain free.

If instead one gives the printed $\exists t$ only the scope $Q(z,t)$, this part's free-for-substitution answer becomes yes, because neither free $y$ occurrence then lies under that binder. Under that alternative parsing, the result is explicitlyThe narrower reading does not change the negative answer in (1): its occurrence of $z$ inside $Q(z,t)$ still requires renaming that binder before substitution. The broad-scope answers above give a single consistent parsing across the paper.

Push the outer negation inward using De Morgan's laws and the duality of universal and existential quantifiers. Negating the outer universal quantifier first gives an existential $x$. Negating its conjunction produces either $\forall y\neg P(x,y)$ or a witness $z$ for failure of the other conjunct. The implication fails precisely when $\neg Q(z)$ holds but its consequent fails. Therefore a negation normal form isAll negations now apply directly to atomic formulas. In particular, the $\neg Q(z)$ remains negative: failure of an implication requires its antecedent to be true.