McDermott and Doyle begin from active processes rather than timeless mathematical proof. A programme diagnoses a fault, predicts a consequence, selects a plan or interprets a message while information is still arriving. Refusing every unforced conclusion produces paralysis. Treating every useful guess as permanent produces brittleness. The desired middle ground permits a conclusion now and records why it may have to disappear later.

The authors distinguish two scales of revision. Routine revision handles familiar exceptions: daylight is expected at noon unless an eclipse, heavy obstruction or some other defeating condition is believed. A much larger reorganisation changes the concepts with which a system describes its world. Their formalism is aimed mainly at the first scale. That modest scope matters. Non-monotonic inference is not presented as a magical theory of scientific revolutions.

Earlier heuristic programmes already used operations such as PLANNER’s THNOT: accept a negative condition when an attempt to prove the positive condition fails. Sandewall proposed rules with Unless; other approaches minimised what could be inferred. These devices captured an important operational intuition but left questions about circular support, incompatible alternatives and what a collection of such rules actually meant.

The 1980 paper proposes a modal-looking language and gives it a fixed-point account. A belief set is not built by applying a one-way recipe once. The set must justify the consistency assumptions that generated it. This recursive demand is the paper’s organising idea: what the reasoner believes determines which assumptions are licensed, while those assumptions help determine what the reasoner believes.

The paper also uses Lq as an abbreviation for M¬q. The notation is historically easy to misread because later autoepistemic logic gives L a knowledge or belief reading. Here the operational test is consistency: an assumption Mq is available when the candidate belief set does not contain ¬q. The absence of a refutation licenses an assumption; it does not manufacture observational support.

Write the noon rule as (noon ∧ M sunshine) → sunshine. With noon explicit and no believed ¬sunshine, the assumption is available and sunshine follows. Add eclipse together with eclipse → ¬sunshine. The candidate set now contains ¬sunshine, so M sunshine is no longer available. The earlier conclusion is withdrawn.

This is not ordinary material implication alone. The modal atom consults the completed belief set that the rule is helping to construct. That self-reference creates the possibility of several coherent completions. It can also create oscillation: assuming C may derive ¬C, which destroys the assumption; dropping the assumption removes ¬C, which restores it.

McDermott and Doyle repeatedly warn against reading M as a standard possible-world modality. Their model theory is deliberately holistic. Whether Mp is true depends on membership in a fixed-point theory S. Indeed, they note an unattractive consequence: Mp may count as true even when p is derivable, if the axiomatisation does not mention the relevant M-expression in the required way. The logic is an early, intentionally weak proposal.

Let A be the explicit axiom set and S a candidate belief set. The paper gathers assumptions Mq whenever ¬q is not in S, excluding M-formulas that already follow classically from A. It then closes A together with those assumptions under ordinary consequence. In the paper’s notation:

As_A(S) = { Mq : q ∈ L and ¬q ∉ S } − Th(A)
NM_A(S) = Th(A ∪ As_A(S))

A fixed point satisfies S = NM_A(S). The equation makes two directions meet. Reading S from left to right determines which q lack a believed negation and therefore which Mq may be assumed. Reading from right to left computes what follows from A and those assumptions. Equality requires the proposal to survive this audit exactly.

The subtraction of Th(A) prevents the apparatus from treating an M-formula already forced by the explicit theory as an extra assumption. That distinction supports later talk about which beliefs are axioms, consequences or assumptions. It also helps the truth-maintenance implementation track what may legitimately be withdrawn.

The operator is non-monotonic in its argument: enlarging S may introduce ¬q, remove Mq from the assumption set and shrink the resulting closure. Familiar least-fixed-point recipes for monotone operators therefore do not automatically apply. McDermott and Doyle initially want a smallest fixed point, but their examples prove that a smallest one may not exist even when several fixed points do.

Consider the theory T1 consisting of propositional calculus plus MC → ¬D and MD → ¬C. One completion assumes C, derives ¬D and thereby defeats MD. Another assumes D, derives ¬C and defeats MC. Both reproduce themselves. Neither contains the other, so neither is a smallest fixed point below the other.

Their intersection omits both ¬C and ¬D. That absence licenses both MC and MD, which regenerates both negations; the intersection is not fixed. Their union contains both negations, blocks both assumptions and also fails to regenerate itself. Sceptical consequence therefore means membership in every fixed point, not closure computed from their intersection as if that intersection were another accepted world.

A still smaller theory contains MC → ¬C. If the candidate omits ¬C, MC is permitted and derives ¬C. If the candidate contains ¬C, MC is blocked and ¬C loses its only support. No candidate survives. This is an oscillation with no fixed point, not evidence that one merely failed to search long enough.

The paper defines TH(A) as the intersection of all fixed points, but explicitly intersects the family together with the whole language L. When there are no fixed points, TH(A) is therefore L: every formula counts as a theorem, signalling inconsistency. This convention is classically explosive. It must not be replaced silently by the programming convention that the intersection of an empty list is empty.

Distinct fixed points are inclusion-incomparable. The paper proves that if S1 and S2 are fixed points and S1 ⊆ S2, then they are equal. A classically expressed theory has exactly one fixed point; modal consistency assumptions introduce the branching. Fixed-point multiplicity is thus not an accidental display detail but the formal representation of alternative defensible belief states.

A formula is provable when it occurs in every fixed point: membership in TH(A). It is arguable when it occurs in at least one. The first is a sceptical projection; the second is a possible or brave projection. A claim may be arguable together with its negation when different fixed points support different positions.

Conceivable is dual to provability: roughly, a formula is conceivable when its negation is not provable. Doubtless is dual to arguability: p is doubtless when ¬p is not arguable. A formula is decided if every fixed point contains it or its negation, and ambivalent otherwise. These distinctions show why simple three-valued labels can lose information.

The paper proves a useful consistency link. In a consistent theory, if p is provable, ¬p is not arguable. It also shows that a doubtless and decided proposition is provable. But the lattice contains proper inclusions: the statuses are not decorative synonyms for true, false and unknown.

The authors then ask what happens under theory growth. A formula is assumable if it can be added as an axiom while leaving a consistent theory. Uncontroversial is the dual notion. Safe means provable in every consistent supertheory; foreseeable is its dual. Realizable and undeniable concern appearance as an axiom in consistent supertheories. These categories map vulnerability under revision rather than probability.

Later non-monotonic literature commonly speaks of cautious and brave reasoning. Those terms help modern orientation, but the paper’s own classifications are more extensive and tied to its definitions of fixed point, consistency and theory extension. The companion uses “sceptical” as explanatory shorthand while preserving the primary vocabulary where formal claims are at issue.

Within a pair, ordinary propositional formulas receive their truth through V. Consistency formulas consult S. This gives the authors soundness and completeness theorems: if A proves p non-monotonically, p is true in every non-monotonic model of A; and if p is true in every such model, it is non-monotonically provable.

The completeness result is deliberately unsurprising. The definition of truth refers back to the fixed-point notion used to define proof. This is not a Kripke semantics that independently explains modality through an accessibility relation among worlds. The authors call their semantics holistic because the meaning of M is bound to the whole theory.

That circular-looking arrangement is informative but costly. It clarifies exactly which completed theories count, yet it offers little compositional insight into why M should obey familiar modal principles. The paper acknowledges counterintuitive cases and promises a stronger treatment in “Nonmonotonic Logic II”, which McDermott published in 1982 using extensions of S5.

Later autoepistemic logic and approximation theory should not be collapsed into this semantics. Moore’s stable expansions, possible-world structures, belief pairs and well-founded approximations form a later family with related fixed-point intuitions. Denecker, Marek and Truszczyński’s 2000 synthesis explains how operators revise possible belief states and how partial approximations can capture sceptical information. That is useful hindsight, not the machinery proved in 1980.

A safe historical sentence is therefore narrow: McDermott and Doyle made self-consistent belief sets and their fixed points central to non-monotonic inference. It is unsafe to say they already supplied the later possible-world or approximation frameworks in mature form.

If p is arguable in A, then A ∪ {p} is consistent and shares a fixed point with A. Conversely, under the paper’s conditions, sharing a fixed point supports the link back to arguability. If p is provable, adding it preserves exactly the same fixed points; the new axiom merely makes explicit what every accepted completion already contained.

Adding a formula that is only arguable may select one branch and eliminate others. More surprisingly, adding an axiom can increase the number of fixed points by changing which assumptions can support one another. Information growth is therefore not simply constraint filtering over a fixed solution space: it can reorganise the assumption structure that defines the space.

The theory is non-compact in an arresting sense. A consistent theory may contain an inconsistent subtheory. The paper’s example places C beside MC → ¬C, producing a fixed point for the larger theory; remove the explicit C and the remaining self-defeating rule has none. Classical logic does not behave this way because adding premises cannot repair inconsistency.

McDermott and Doyle define safety through all consistent supertheories. Safe(A) is the least set containing A, closed under classical consequence, and closed under a characteristic consistency condition: if ¬p is safe, then Mp is safe. This captures beliefs protected against every consistent elaboration, a far stronger property than being in today’s fixed points.

These results matter for systems that retain conclusions. Marking a claim merely “derived” omits whether it is provable across fixed points, supported by one branch, preserved by a specific extension, or safe through all consistent extensions. Revision policies need these different dependency contracts.

An ordinary tableau for A → p seeks a falsifying branch. If every branch closes, p follows classically. Non-monotonic tableaux must additionally decide whether each Mq is available. When an occurrence of Mq is labelled false on an open branch, the construction opens a tableau for A → ¬q to test whether ¬q is derivable under the same global labelling.

The tableaux therefore form a mutually referring structure. A labelling is admissible when it satisfies the consistency constraints across that structure. A branch closes if it assigns both truth values to a formula. The initial goal is non-monotonically provable only when its tableau closes under every admissible labelling.

For the chain theory MC → ¬D, MD → ¬E, ME → ¬F, one admissible labelling remains. It supports ¬F but not ¬C. For the symmetric fork MC → ¬D, MD → ¬C, two admissible labellings correspond to the two fixed points. Neither ¬C nor ¬D is universal, though a disjunction about the alternatives can be.

The paper proves that the procedure halts and finds all admissible labellings for finite proper axiom sets. Lemmas connect labellings to fixed points, and Theorem 16 concludes that non-monotonic provability is decidable for finite extensions of sentential calculus.

The boundary is sharp. Non-monotonic predicate calculus is not even semidecidable in general. The authors sketch why an imagined theorem procedure would decide number-theoretic questions by running searches involving p and a modalised alternative in parallel. Their finite decision result must not be advertised as a solver for the first-order language.

A database item is “in” when it has a valid justification whose supporting items are in and whose defeating conditions are out. Only in-items are visible to the problem solver. The maintenance process keeps support non-circular and avoids simultaneously endorsing a claim and the consistency assumption for its negation.

When a new justification invalidates an assumption, labels propagate through dependent items. The system seeks another non-circular support structure. When both p and ¬p become in, it traces the contradiction backwards to the assumptions on which each side depends. It then adds a justification or axiom that denies one of those assumptions: dependency-directed backtracking.

The paper’s compact example begins with MC → E. The system accepts MC and derives E. A new rule MD → ¬E permits MD and derives ¬E, exposing a conflict. Tracing the two sides finds MC and MD. Adding E → ¬D uses the already supported E to derive ¬D, defeat MD and withdraw ¬E while preserving the larger existing structure.

This is a policy of minimal disruption, not a theorem that one fixed point is uniquely correct. The TMS normally finds one admissible labelling: or a fragment corresponding to one fixed point: so its visible conclusions may be arguable rather than provable. The paper defends this commitment: an active programme must choose a working model and stay with it until trouble supplies a reason to move.

There are two kinds of trouble. Local conflicts can be repaired by relabelling and backtracking. A subtheory with no fixed point can make the TMS loop indefinitely; checking globally for that condition would be expensive and is omitted. The implementation therefore approximates the logic rather than deciding its full sceptical consequence on every update.

The authors also note that the TMS handles combinations such as Mp, M¬p, Lp and L¬p in a way that may connect to Belnap’s four-valued logic. This is presented as a possible relationship, not as a completed reduction. The central engineering lesson remains support provenance plus directed revision.

The deduction theorem fails in general. Whether p follows can depend on the completeness of the axiom set and the absence of other formulas; moving a premise into an implication may alter which consistency assumptions are available. Classical proof transformations cannot be imported without checking their interaction with the non-monotonic operator.

A theory may express an intuitive default and still have no fixed point. The paper’s exceptional example includes MC → D and ¬D. The rule’s consequent is refuted, but the weak system may derive ¬MC without deriving ¬C, producing incoherence that the TMS resolves by an additional arbitrary commitment. Likewise, M does not distribute through conjunction in the expected way: M(C ∧ D) need not supply MC.

First-order reach is a severe boundary. The authors hope for “asymptotic decidability”: an indefinitely running system might revise answers overall but change its answer to each particular question only finitely often. They observe that even finite first-order theories can frustrate this hope. The proposal is a research direction, not a delivered convergence theorem.

“Nonmonotonic Logic II” later strengthens the modal basis with S5-style machinery and requires new semantics, completeness arguments and procedures. Moore’s autoepistemic logic, Reiter’s default logic, logic programming semantics and later belief-pair approximations further diversify the fixed-point landscape. Shared vocabulary: expansion, fixed point, default, stable belief: does not make their operators equivalent.

Later scholarship supplies a valuable conceptual gloss. Denecker, Marek and Truszczyński describe a fixed point of a revision operator as a belief state that cannot be revised away and use belief pairs to approximate sceptical reasoning. They also report high complexity for extension and expansion tasks. Those claims concern later formal systems; they help explain why incomplete approximations matter without changing the 1980 theorem set.

Lehmann’s later account of preferred-model and choice-function semantics shows another route: replace full Tarskian monotonicity with weaker properties and select preferred models. That framework clarifies how broad the field became. McDermott and Doyle’s contribution is not that they settled every approach, but that they made the feedback between belief, consistency and revision mathematically explicit at a foundational moment.

Separate strict observations from consistency assumptions. A sensor reading, policy axiom or signed record should not share the same provenance class as “not currently contradicted”. This lets an update defeat the assumption without rewriting the observation history.

Compute or approximate multiplicity deliberately. If several fixed points exist, decide whether the query needs what all share, what any permits, or one branch selected for action. Label the selection rule. A sceptical dashboard, diagnostic explorer and autonomous controller can legitimately expose different projections of the same landscape.

Detect self-defeat. Before presenting a belief set, recompute the assumptions it licenses and verify that their closure returns the set. Iteration that alternates between two candidates is evidence of a semantic problem, not a licence to return whichever appeared last.

Track dependency edges. When a contradiction arrives, follow both sides to their revisable assumptions and choose a repair under an explicit priority or minimal-change policy. The TMS makes this operational. Modern implementations may use assumption-based truth maintenance, SAT, answer-set solving or provenance graphs, but the responsibility remains.

Do not confuse logical status with decision value. A provable formula is shared by accepted completions; an arguable formula has a supporting completion. Neither label contains cost, risk or probability. High-stakes action needs a separate decision layer, and safety may demand refusing a default even when it is logically licensed.

Finally, publish computational boundaries. State the language fragment, whether every completion was enumerated, how non-existence was certified, which timeouts apply and whether the output is all-fixed-point or one-maintained-world. McDermott and Doyle’s candid statement that the logic is weak is a model of responsible technical writing.

Review one: primary fidelity and pedagogy. The reconstruction was checked across the complete 37-page MIT AI Memo 486a scan: August 1978, revised January 1979: and against the 1980 journal record. The reading covered motivations, THNOT and Unless, the M/L syntax, classical closure, As_A and NM_A, examples with two and no fixed points, the definition of TH(A), holistic models, soundness and completeness, fixed-point structure, epistemic classifications, theory evolution, safety, linked tableaux, decidability, the TMS, first-order limits and the proposed stronger sequel.

The sharpest risks were notation and empty cases. Lq is kept as the paper’s abbreviation rather than assigned its later autoepistemic meaning. The no-fixed-point theory reports TH(A)=L under the authors’ convention, not an empty intersection. Fixed-point intersection is presented as a sceptical projection and not itself assumed fixed.

Review two: fairness, later context and executable delivery. The paper’s self-criticism is retained: the modality is holistic, the logic is weak, some theories behave exceptionally, the TMS approximates rather than fully implements the logic, and predicate-calculus provability is not semidecidable. Later work on stable expansions, preferred models and belief pairs is dated and labelled as context.

All ten bespoke SVG figures have titles, descriptions, captions and source notes; animation is redundant and disabled under reduced-motion preference. The laboratory checks three scenarios under three report modes. It enumerates every finite candidate, independently verifies S=Γ(S), compares the reported list with exhaustive enumeration and checks the all/some projection including the paper’s empty-family convention.

Circumscription prefers models by a set-inclusion order. McDermott and Doyle instead define an operator over candidate theories. Both allow conclusions to disappear when facts grow, and both can leave multiple admissible alternatives. Their mathematical explanations differ: one asks which worlds contain no unnecessary instances; the other asks which belief sets regenerate their licensed assumptions.

The neighbouring 1980 Artificial Intelligence papers: McCarthy on circumscription, McDermott and Doyle on non-monotonic logic, and Reiter on default logic: give three foundational answers to incomplete information. Keeping them adjacent makes the contrasts visible rather than blending “default reasoning” into one mechanism.

Canon 0096 turns from a particular non-monotonic formalism to Allen Newell’s “The Knowledge Level”. Newell asks how an intelligent system may be described by what it knows and what goals it has, abstracting from the symbol-level mechanisms that implement those commitments.