Reading the abstract syntax tree recursively gives the eight distinct subformulas
(1)
A subformula includes the complete propositional formula itself as well as the operands of its connectives. There are nine occurrences in the abstract syntax tree, because the atomic formula occurs twice, but only eight different propositional formulas in the set.
Eliminate the logical implication and apply De Morgan's laws:
(1)
This is disjunctive normal form: a logical disjunction of conjunctions of literals. It has four literal occurrences, namely , meeting the stated bound.
Repeated use of yields
(1)
This logical disjunction is false exactly when are all true and is false. There is precisely one such Boolean valuation out of the assignments to the independent propositional variables. Thus the number of satisfying assignments is . This is the satisfying-assignment count for nested implications; the implication brackets associate to the right here.
Simultaneous propositional substitution gives
(1)
Let . The first disjunct equals . By De Morgan's laws, implies , so absorption reduces that first disjunct to . The second disjunct is and is also absorbed by . Therefore
(2)
The resulting Boolean function is false only when both and are true, providing a four-row truth table check.
Assume the logical conjunction temporarily, then eliminate the premise's logical disjunction by cases. A natural deduction proof, with each indented assumption delimiting its own subproof, is:
1.  not P or not Q                    premise
2.  | P and Q                        temporary assumption
3.  | P                              and-elim-L, 2
4.  | Q                              and-elim-R, 2
5.  | | not P                        first disjunction case
6.  | | false                        not-elim, 3,5
7.  | | not Q                        second disjunction case
8.  | | false                        not-elim, 4,7
9.  | false                          or-elim, 1, cases 5-6 and 7-8
10. not (P and Q)                     not-intro, discharge 2-9
Lines 5–6 and 7–8 are separate sibling subproofs, not one nested inside the other. Both derive the same contradiction under the common assumption on line 2. Logical disjunction elimination discharges the two case assumptions, and negation introduction then discharges the logical conjunction assumption. The sole undischarged premise is the required one. This proof uses only the supplied logical conjunction, logical disjunction and negation rules; no converse form of De Morgan's laws is being assumed as an extra rule.

Ancestors (10)

  1. Digital systems, linear algebra, introduction to formal proof resit
  2. 2022
  3. Past exam of the year 1 of the computer science course of the University of Oxford
  4. Year 1 of the computer science course of the University of Oxford
  5. Computer science course of the University of Oxford
  6. Undergraduate course of the University of Oxford
  7. Course of the University of Oxford
  8. University of Oxford
  9. List of universities
  10. Home

View article source

Discussion (0)

New discussion

There are no discussions about this article yet.

Articles by others on the same topic (0)

There are currently no matching articles.
See all articles in the same topic Create my own version