Discrete Mathematics: Lecture Notes, Part 2 (Temnikova, 2019)

Olena Leonidivna Temnikova's 2019 KPI lecture course is an admissible secondary source: an authored, reviewed, officially approved teaching volume rather than a student notebook or assignment brief. It gives a valuable view of how Boolean-function theory, formal logic, automata, and concurrent-system models fit into one discrete-mathematics sequence. It is not safe to use as a mathematical authority by itself. Definitions are sometimes ill-typed, several examples contradict their own tables or diagrams, and the metatheory repeatedly merges distinct notions.

Every physical page was read through page-bounded native text and inspected as a full-page render. The 128 source pages, 128 extracted-text pages, 128 renders, and 128 coverage records reconcile exactly. One hundred information-bearing tables, formula layouts, circuits, state diagrams, proof traces, and Petri-net figures were individually audited. The original and archived copies are byte-identical, with SHA-256 58eee2238857eb4bc3bf563fca4425a62b50b69eb18fd0561c74914bf4a9f65f.

What the volume covers #

Physical pages	Durable subject	Evidentiary weight
1-14	Abstract Boolean algebras, the two-element algebra, Boolean functions, essential variables, and formula semantics	Useful curricular structure; foundational labels and examples contain contradictions
14-23	Truth vectors, DNF/CNF, perfect normal forms, algebraic normal form, and Zhegalkin polynomials	Topic map; theorem hypotheses and several printed transformations need repair
23-32	Preservation classes, self-duality, monotonicity, linearity, and Post functional completeness	Strong topic signal; the constructive proof has a material gap
32-41	Implicants, Quine and Quine-McCluskey minimization, covering tables, Veitch/Karnaugh maps, and don't-cares	Useful workflow map; cost arithmetic, one factor, and the claimed greedy optimum are wrong
42-60	Propositional syntax and semantics, validity, entailment, natural-language formalization, and inference patterns	Useful scope; necessary/sufficient conditions and implication are mischaracterized
60-65	Clausal form and resolution refutation	Durable topic; the completeness/search condition is missing and some proof traces are unreliable
65-95	Formal theories, Hilbert calculi, the deduction theorem, proof rules, soundness, completeness, decidability, and independence	Valuable metatheory map; historical schemas and several core distinctions are corrupted
96-109	Sequential machines, Mealy/Moore transducers, equivalence, minimization, finite recognizers, and regular grammars	Already covered more reliably in GTK; source examples contain state/output and grammar errors
109-127	Place/transition Petri nets, conflict and concurrency, behavioral properties, reachability, coverability, incidence algebra, reductions, and extensions	The strongest new territory signal; all formal semantics and algorithms were independently rebuilt
127-128	Review questions and bibliography	Navigation only

GTK does not mirror that chapter order. Boolean-function material remains in the canonical electronics chapter because it connects algebraic forms to physical logic synthesis. Propositional resolution extends the existing logic chapter. Existing automata and transducer chapters already exceed the course and are not rewritten. Petri nets become their own deep discrete-mathematics topic because concurrency, reachability, and invariants form a distinct reusable model.

What remains useful #

The volume's best contribution is its dependency chain. Boolean expressions lead to canonical and minimized forms; propositional semantics leads to proof calculi and automated refutation; machines add stored state; Petri nets then replace a single global state transition with distributed resources and partially ordered events. That progression is pedagogically sound once the formal boundaries are repaired.

Several recurring contrasts are also worth retaining:

an abstract Boolean algebra is not identical to the two-element truth-value algebra;
a formula is syntax, while a Boolean or propositional function is its denotation;
semantic entailment and syntactic derivability are related by soundness and completeness, not interchangeable notation;
a finite-state transducer emits a sequential trace, while a recognizer accepts a language;
Petri-net tokens are resource counts, not individual objects that literally travel through the graph;
ordinary P/T nets provide nondeterministic firing, whereas guards, priorities, values, time, and probabilities require explicit extensions.

Where the source fails #

Location	Source problem	Corrective treatment
pp. 8, 11	Truth labels are reversed and a named binary Boolean function contradicts its own vector	Reconstruct every truth table from declared `0/1` semantics
pp. 18-20	Canonical-term theorems omit the requirement that every variable occur exactly once; constants and symbols are mishandled	State exact hypotheses and derive DNF/CNF from truth-table rows
pp. 29, 32, 35, 38, 40	Post's constructive argument has a gap; gluing names are swapped; cover costs and a CNF factor are wrong; greedy K-map grouping is called always minimal	Use the exact Post criterion, a verified implicant-combination algorithm, and an explicit cover-cost contract
pp. 46, 49, 59	Necessary and sufficient directions are reversed; a valid axiom is mislabeled “affirming the consequent”; entailment is incorrectly conditioned on satisfiable premises	Separate truth-functional implication, metalinguistic consequence, and natural-language conditionals
pp. 60-65	Resolution is presented without the complete or fair saturation condition, and some line references are defective	Give a checked refutation trace and state soundness, propositional completeness, and search boundaries separately
pp. 65-95	Soundness, semantic completeness, syntactic completeness, consistency, maximal consistency, independence, and decidability are repeatedly conflated; Gödel's theorems are overgeneralized	Define each property with its quantifiers and restrict incompleteness claims to theories satisfying the actual hypotheses
pp. 71-73	Several attributed historical axiom schemata are malformed or falsifiable as printed	Omit the catalogue unless each formula is recovered from its primary historical source
pp. 97-109	A Boolean circuit evaluates incorrectly, a Mealy trace contradicts its output table, an accepting-set type is wrong, and a grammar production disagrees with the automaton	Use independently constructed automata examples and explicit timing/trace conventions
pp. 111-122	The P/T-net tuple is ill-typed; nondeterminism is called randomness; ordinary nets silently acquire guards or values; persistence, safeness, and coverability are misstated	Rebuild semantics from typed pre/post maps, componentwise enabling, and the marking-update equation
pp. 122-126	Pre-incidence direction is reversed, the promised state equation is missing, and six reductions claim blanket property preservation without side conditions	Derive incidence algebra independently; present reductions only with exact hypotheses and preservation direction
pp. 126-127	Simulation and colored-net status claims are categorical or time-sensitive	Replace them with current, scoped descriptions of analysis and high-level-net extensions

Visual audit #

The audit records 22 information-bearing visual groups on pages 1-41, 51 on pages 42-95, and 27 on pages 96-128. They include truth tables, Boolean cubes, implicant charts, Karnaugh maps, proof layouts, automaton tables and graphs, Petri-net markings, coverability trees, matrices, and reduction panels.

No source image is retained in GTK. Several visuals directly encode incorrect values or arc semantics; others depend on damaged surrounding formulas or omit conditions that determine whether the picture is valid. The affected chapters instead use newly authored, theme-aware SVGs whose values, labels, transitions, and invariants are checked against independently verified definitions. This preserves the explanatory role of diagrams without transferring the source's technical defects.

Source claims audit #

Load-bearing source claim	Status	GTK treatment
Boolean functions admit canonical DNF/CNF and a unique algebraic normal form	current with exact hypotheses	Re-derived over the two-element algebra; syntax and denotation remain distinct
Post's five preservation classes characterize functional completeness	current with convention boundary	The historical criterion is limited to the publicly visible Section 26 opening; the modern classes and nullary-constant convention come from the fully read Gonda paper and clone-theory excerpt
Prime implicants and covering tables support two-level minimization	current with cost-model qualification	Rebuilt from verified Quine-McCluskey mechanics; optimum depends on the declared cost
Resolution refutation decides propositional unsatisfiability	current with complete-search qualification	Presented with CNF conversion, negated goal, fair saturation, and the empty clause
First-order structures, satisfaction, and substitution use one typed semantic contract	current within declared scope	Rebuilt from three fully read Open Logic modules; their single-sorted, nonempty, total-function assumptions remain explicit, and a defective printed witness is replaced by direct enumeration
Soundness, completeness, consistency, and decidability are interchangeable	error in source	Replaced by separate semantic and proof-theoretic definitions and implications
Mealy/Moore conversion and minimization follow the printed unconditional counts and trace rules	needs correction	Existing GTK articles keep explicit observation conventions and reachable-state refinement
Ordinary P/T-net firing is random and may manipulate guarded values	error in source	Ordinary nondeterministic token-count semantics is separated from colored, timed, stochastic, and guarded extensions
The state equation and shown reductions decide reachability while preserving all named properties	error/unsupported	State equation is taught as necessary but generally insufficient; unsafe reduction claims are omitted

Editorial role #

The course is cited where its curriculum and explanatory organization materially informed an article. The exact verification chain is narrower: fully read primary papers control McCluskey minimization and Robinson resolution; the bounded Post Section 26 opening plus fully read modern clone sources control functional completeness; three fully read Open Logic modules control the first-order structure, satisfaction, and guarded-substitution contract; Hack's fully read primary report controls core P/T semantics and exact coverability results; the complete van Glabbeek author-version web text controls multiset steps and semantic conflict; Murata's fully read survey controls only the analysis conventions it actually states. Direct reconstruction controls the truth tables, matrices, and worked traces. The source is never cited to support one of its defective examples, historical transcriptions, numerical claims, or diagrams.