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 / 7

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.