Reasoning About Knowledge of Unawareness

Joseph Y. Halpern; Leandro Chaves Rego

REVIEW

Reasoning About Knowledge of Unawareness

Logic in Computer Science · Submitted 5 Mar 2006 · 4 references

Pith's verdict: Syntactic valuations make this the right logic for knowledge of unawareness; the core completeness proof holds up, but the r.e.-completeness theorem needs a countable-Φ hypothesis and some proof details are skipped.

T0 · AI review

How this review was made: An AI referee (deepseek-v4-flash) read the paper on August 28, 2026 and answered a fixed list of questions about it. T0 is the starting level every paper gets. The levels describe how deeply Pith has checked the paper, never the authors.

T0 AI review An AI read the paper and answered a fixed list of questions.
T1 Audit Automatic checks that the references and files the paper relies on exist and match.
T2 Compute The paper's code or calculations re-run with the same results.
T3 Formal statement The claims written out in a formal math language a computer can read.
T4 Proof Those claims proved, and the proof checked by computer.

How Pith checks papers →

· 3 major objections · 5 minor · Ask about this paper · The compiled record · Read the full review →

Challenge this review Comment (0) Read on arXiv ↗

Cite ▾

arXiv IDcs/0603020 (version 1)

Pith IDUTJNP725, Pith's permanent record of this paper and its review

CitationJoseph Y. Halpern, Leandro Chaves Rego. "Reasoning About Knowledge of Unawareness." arXiv:cs/0603020 (2006). https://pith.science/paper/UTJNP725

Cite this reviewBibTeX for Pith's review of this paper

Claim paper

Why Pith says this

Highlight any text to comment on it.

Editor's note

read the letter

The thing to know: this paper is the one that finally lets an agent explicitly know there are facts she is unaware of without naming one. The trick is syntactic valuations: variables are assigned quantifier-free sentences, not truth values, which avoids the circularity that kills semantic valuations in awareness logic. That is a genuinely new mechanism, and the completeness proof for the countably infinite case is real and detailed.

What it does well: the axiomatization is elegant — standard modal and quantifier axioms plus Barcan — and the canonical model argument in the appendix is mostly complete. The reduction for Theorem 5.1 from first-order logic with one binary predicate is a solid undecidability proof. The paper is also honest about the restriction that quantification ranges only over quantifier-free sentences; that is not a hidden flaw, it is stated and it is what makes the semantics well-founded.

The soft spots are in the complexity section, not the semantics. Theorem 5.1 is printed without the 'Φ countably infinite' condition that Theorem 4.1 requires. Section 4 says finite Φ would need extra axioms, and none are given. So as stated, the r.e.-completeness claim is not proved for finite Φ. That is a scope problem in a headline result, but the fix is mechanical: add the hypothesis to the theorem and the abstract. Second, Theorem 5.2 and 5.3 have several 'leave it to the reader' steps, and the C={e} case of Theorem 5.3 relies on a characterization in an unpublished self-cited companion. That makes the decidability results hard to verify from the text. These are real but not fatal; they are the kind of thing a referee would send back for revision.

Who gets value: anyone working in epistemic logic, game theory with unawareness, or bounded rationality. The paper deserves a serious referee; I would not desk-reject it. I'd send it out and ask for those fixes.

Referee report

Significance

If the results hold as stated, the paper is a valuable contribution: it gives a logic that can express knowledge of unawareness in the sense described, provides a complete axiomatization using standard quantifier axioms plus the Barcan formula, and maps out an undecidable/decidable boundary that is surprising in light of Fine's decidability result for S5 with propositional quantifiers. The completeness proof is a genuine and mostly detailed canonical-model construction, and the hardness reduction in Theorem 5.1 is a legitimate embedding of first-order logic into awareness structures. A notable strength is that the paper explicitly discloses the restriction of quantification to quantifier-free sentences and explains why that restriction is needed for well-foundedness; this is a real limitation of the expressiveness claim, but it is not an internal inconsistency. The main weaknesses are in the complexity section, where the statements outrun the proofs: the r.e. upper bound is tied to a completeness theorem that is proved only for countably infinite Φ, and the proofs of Theorems 5.2 and 5.3 contain substantial omitted cases.

Major objections (3)

[§5, Theorem 5.1] Theorem 5.1 is stated for all Φ and all C, but the proof of the r.e. upper bound cites Theorem 2.1, which axiomatizes only the quantifier-free language LK,X,A_n(Φ). For the quantified language the relevant completeness result is Theorem 4.1, and that theorem is proved only under the hypothesis that Φ is countably infinite. Section 4 explicitly says that for finite Φ 'we would need extra axioms' because universal quantification can collapse to a finite conjunction, and no such axioms are supplied. Consequently, as stated, the r.e. upper bound, and therefore the abstract's claim that validity is 'recursively enumerable, but not decidable' for the logic, is not established when Φ is finite. The theorem and abstract should either carry the countably infinite Φ hypothesis or be accompanied by a finite-Φ axiomatization and completeness argument.
[Appendix A, proof of Theorem 5.2] The proof of Theorem 5.2 is carried out under the assumption that Φ is countably infinite, and the reduction from infinite Φ to arbitrary Φ, including |Φ|=1, is only a sketch that delegates to [Halpern 1995] and leaves the construction of the formulas r_j and the verification of the analogues of Lemmas A.9 and A.10 to the reader. This is load-bearing because the theorem is stated for every Φ with no cardinality restriction. The r.e. upper bound for Theorem 5.2 also cites Theorem 2.1, which does not axiomatize the quantified language, so the same scope problem from Theorem 5.1 applies. Please supply the missing proof or explicitly restrict the theorem to countably infinite Φ.
[Appendix A, proof of Theorem 5.3] The decidability proof is given in detail only for the case C={r,e,t}. For C={e,t} the paper lists modifications but does not prove the modified Lemma A.11, and for C={e} it states that the same ideas prove an analogous result, omits details, and relies on a semantic characterization from [Halpern and Rêgo 2006a]. Since Theorem 5.3 is one of the four main results, the omitted cases are load-bearing: the counting argument changes substantially through the introduction of KK-counts and the formulas indist and indistKK. A complete proof, or a precise pointer to a published proof of the characterization and the quantifier-elimination argument, is needed before the decidability classification can be considered established.

Minor objections (5)

[§3, semantics of ∀] The restriction of syntactic valuations to quantifier-free sentences in LK,X,A_n(Φ) is stated clearly, but its consequence for the intended reading of ∃x should be highlighted in the abstract or introduction: the 'facts' over which x ranges are quantifier-free facts, not all facts expressible in the full quantified language.
[§5, proof of Theorem 5.1] The sentence 'The fact that deciding validity is r.e. follows immediately from Theorem 2.1' appears to be a typo for Theorem 4.1, and the same proof text later says 'valid in M^∅_n(Φ,X)' where the reduction was carried out for one agent; it should read M^∅_1(Φ,X).
[§5, statement of Theorem 5.2] The theorem statement says L∀,K_n(Φ), but the definition in Section 3 and the proof use L∀,K_n(Φ,X); the notation should be made consistent.
[Appendix A, Lemma A.2] In the statement of the consistency extension step, the text says '∆ ∪ ¬ϕ[x/q]' but the surrounding argument and the witness construction require '∆ ∪ {¬ψ[x/q]}' where ¬∀xψ is the formula in ∆; the mismatch between ψ and ϕ should be corrected.
[Appendix A, Theorem 4.1 header] The appendix restates Theorem 4.1 without the 'Φ is countably infinite' hypothesis that appears in the main text and is used in the proof; the two statements should be identical.

How Pith checks papers → · Full audit of this paper →

The paper

The paper claims

Propositional quantification lets a logic of awareness express that an agent knows there are unknown facts without naming one, and the paper proves the logic has a complete axiom system.

The reading

Knowledge of unawareness—knowing that there are facts you have not even considered—appears in everyday settings such as a doctor referring a patient to a specialist or an investor choosing a fund manager. Earlier awareness logics could not express this: an agent could know he is unaware of a specific formula, but could not know that some fact escapes him without knowing which. This paper closes that gap by adding propositional quantification to the logic of general awareness. The paper proves that the resulting logic is soundly and completely axiomatizable, and that deciding validity is recursively enumerable but undecidable. If the results are right, higher-order ignorance becomes formally tractable in a language with a complete proof system.

What carries the argument

The load-bearing device is a syntactic valuation: a function that assigns to each propositional variable a quantifier-free sentence of the base awareness language, instead of a truth value. Universal quantification $\forall x\phi$ is then evaluated by replacing $x$ with every such quantifier-free sentence; because substitution removes variables, the truth definition is well-founded. The axiomatization adds the standard quantification axioms—$\forall x\phi \Rightarrow \phi[x/\psi]$ for substitutable quantifier-free $\psi$, $K\forall$, $N\forall$, the Barcan axiom $\forall x K_i\phi \Rightarrow K_i\forall x\phi$, and the rule $Gen\forall$—on top of the usual knowledge and awareness axioms. In the completeness proof, a canonical model is built from 'acceptable' maximal consistent sets of sentences, which ensure that every false universal sentence $\neg\forall x\psi$ has a witness $\neg\psi[x/q]$ for some primitive proposition $q$; this is why the set $\Phi$ of primitive propositions must be countably infinite.

Extended reading notes

Core claim

On the paper's own terms, the central discovery is that propositional quantification can be added to the logic of general awareness, with the quantifier ranging only over quantifier-free sentences, so that the formula $X_i(\exists x \neg A_i x)$ can be true even when no particular formula $\psi$ satisfies $X_i(\neg A_i \psi)$. The semantics uses syntactic valuations rather than truth-value valuations, and this restriction is what keeps the truth definition non-circular. With that semantics, the paper proves a sound and complete axiomatization (Theorem 4.1) and shows that validity in the language is r.e.-complete (Theorem 5.1).

Load-bearing premise

The truth of a universal formula is checked by substituting only quantifier-free sentences, not every sentence of the richer language; if the range were the full language, the definition of truth would chase its own tail and the paper's completeness result would no longer apply.

Editorial extensions

If this is right

An agent can know that he is unaware of something without being able to name a single thing he is unaware of, so higher-order ignorance is representable.
Multi-agent scenarios like referral and delegation can be modeled: one agent can explicitly know that another agent is aware of facts he is not, without knowing those facts.
The usual knowledge and awareness axioms, plus standard quantifier axioms, are enough; no nonstandard quantifier rules are needed beyond the restricted substitution axiom.
Validity cannot be decided by any algorithm, so reasoning about knowledge of unawareness is inherently open-ended: all validities can be enumerated, but no procedure can answer every formula.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

The paper leaves implicit that the same trick—restricting quantification to a syntactic fragment that shrinks under substitution—would work for other intensional operators such as probability or belief, potentially producing complete logics for higher-order uncertainty.
A natural extension is a hierarchy of quantifiers ranging over sentences of bounded quantifier depth; the paper's well-foundedness argument suggests this remains consistent, though the r.e.-completeness result may change at each level.
In games, the undecidability result implies that strategic reasoning about opponents' unawareness cannot be fully automated; any practical solver must restrict the language or accept incompleteness.

Original abstract

Awareness has been shown to be a useful addition to standard epistemic logic for many applications. However, standard propositional logics for knowledge and awareness cannot express the fact that an agent knows that there are facts of which he is unaware without there being an explicit fact that the agent knows he is unaware of. We propose a logic for reasoning about knowledge of unawareness, by extending Fagin and Halpern's \emph{Logic of General Awareness}. The logic allows quantification over variables, so that there is a formula in the language that can express the fact that ``an agent explicitly knows that there exists a fact of which he is unaware''. Moreover, that formula can be true without the agent explicitly knowing that he is unaware of any particular formula. We provide a sound and complete axiomatization of the logic, using standard axioms from the literature to capture the quantification operator. Finally, we show that the validity problem for the logic is recursively enumerable, but not decidable.

The compiled record

The paper's own sentences, arranged, kept beside the review and separate from it. Each label is drawn from a closed vocabulary; the number beside it is the probability the classifier gave that label. Numbers in the tables are the authors', checked by code. No sentence in this record was written by a model.

Compiled by classifier-1.13-20260917 via OpenRouter, question bank abstract-p1-20260923, 2026-09-23: 1 request, 5,575 input tokens, $0.0002 reported.

What the abstract itself states, as probabilities: claims first 0.07 · states limitation 0.78 · human participants 0.02 · controlled comparison 0.02 · randomized assignment 0.01 · states quantitative result 0.07 · compares with prior results 0.75 · mentions code or data availability 0.02.

The abstract, sentence by sentence

arXiv listing abstract v1. Results and the main claim are underlined; show every role.

Awareness has been shown to be a useful addition to standard epistemic logic for many applications. However, standard propositional logics for knowledge and awareness cannot express the fact that an agent knows that there are facts of which he is unaware without there being an explicit fact that the agent knows he is unaware of. We propose a logic for reasoning about knowledge of unawareness, by extending Fagin and Halpern's \emph{Logic of General Awareness}. The logic allows quantification over variables, so that there is a formula in the language that can express the fact that ``an agent explicitly knows that there exists a fact of which he is unaware''. Moreover, that formula can be true without the agent explicitly knowing that he is unaware of any particular formula. We provide a sound and complete axiomatization of the logic, using standard axioms from the literature to capture the quantification operator. Finally, we show that the validity problem for the logic is recursively enumerable, but not decidable.

background contribution method result interpretation main claim

What the classifier reports for each sentence. The number is the probability it gave the label.
#	sentence	role	the authors' own work	states the main conclusion	strength
s0	Awareness has been shown to be a useful addition to standard epistemic logic for many applications.	background 1.00	0.05	0.02	asserted 1.00
s1	However, standard propositional logics for knowledge and awareness cannot express the fact that an agent knows that there are facts of which he is unaware without there being an explicit fact that the agent knows he is unaware of.	gap 0.85	0.09	0.07	asserted 1.00
s2	We propose a logic for reasoning about knowledge of unawareness, by extending Fagin and Halpern's \emph{Logic of General Awareness}.	contribution 0.98	0.93	0.23	asserted 0.98
s3	The logic allows quantification over variables, so that there is a formula in the language that can express the fact that ``an agent explicitly knows that there exists a fact of which he is unaware''.	contribution 0.73	0.90	0.37	asserted 0.99
s4	Moreover, that formula can be true without the agent explicitly knowing that he is unaware of any particular formula.	result 0.73	0.86	0.20	asserted 0.97
s5	We provide a sound and complete axiomatization of the logic, using standard axioms from the literature to capture the quantification operator.	contribution 0.64	0.94	0.11	asserted 1.00
s6	Finally, we show that the validity problem for the logic is recursively enumerable, but not decidable.	result 0.97	0.94	0.18	asserted 1.00

What kind of paper the classifier reports this is: theoretical result 0.71 · evidence from proof or derivation 1.00.

What was examined, and what was not

sources read

arXiv listing abstract v1

not examined

full text
figures and tables
references and citing sentences
relations to other papers

levels run

P abstract

not run

S sections
T body sentences
C citations
R cross-paper relations

Every quoted sentence on this record is the authors'. Every label is from Pith's closed vocabulary, with the probability shown beside it. Every number in the measurements table is the authors', checked by code. Record as JSON

Figures

**Figure 1.** States. In the figure, the K1 relation consists of the pairs joined by dotted lines; the K2 consists of the pairs liked by the continuous edges. (In both cases we omit self-loops.) Let atomic(x ) be an abbreviation for the formula ¬K1K2K1¬(p ∧ q ∧ x) ∧ ¬∃y(¬K1K2K1¬(x ∧ y) ∧ ¬K1K2K1¬(x ∧ ¬y)). Intuitively, atomic(x ) is true if all K1K2K1-reachable worlds that satisfy x agree on all sentences. We use worlds where p∧q∧x holds for some atomic formula x to represent elements in d. If two worlds satisfy the same atomic formula, then they represent the same domain element. Let σ1 be the…

Figures reproduced from arXiv:cs/0603020 by the authors.

References

Works cited (4)

[1]

Bull, R. (1969). On modal logic with propositional quantiﬁe rs. Journal of Symbolic Logic 34, 257–263. Dekel, E., B. Lipman, and A. Rustichini (1998). Standard sta te-space models preclude un- awareness. Econometrica 66, 159–173. Enderton, H. B. (1972). A Mathematical Introduction to Logic. New York: Academic Press. Engelhardt, K., R. van der Meyden, and ...

View on Pith 1969
[158]

An extended version with the title “Interactive unawar eness” will appear in the Journal of Economic Theory. Hintikka, J. (1962). Knowledge and Belief. Ithaca, N.Y .: Cornell University Press. Hughes, G. and M. Cresswell (1996). A New Introduction to Modal Logic. London: Rout- ledge. Kaplan, D. (1970). S5 with quantiﬁable propositional varia bles. Journal...

View on Pith 1962
[355]

Kripke, S. (1959). A completeness theorem in modal logic. Journal of Symbolic Logic 24, 1–14. Lewis, H. R. (1979).Unsolvable Classes of Quantiﬁcational Formulas. New York: Addison- Wesley. 31 Modica, S. and A. Rustichini (1994). Awareness and partitional information structures. The- ory and Decision 37, 107–124. Modica, S. and A. Rustichini (1999). Unawar...

View on Pith 1959
[2003]

30 Fagin, R., J. Y . Halpern, and M. Y . Vardi (1992). What can machines know? On the proper- ties of knowledge in distributed systems. Journal of the ACM 39(2), 328–376. Feinberg, Y . (2004). Subjective reasoning—games with unawareness. Technical Report Re- sarch Paper Series #1875, Stanford Graduate School of Business. Fine, K. (1969). For Some Proposit...

View on Pith arXiv 1992

Discussion

Disagree with the review, or know something it missed? Leave a comment, highlight any passage above to comment on it, or challenge this review formally.

[1] [1]

Bull, R. (1969). On modal logic with propositional quantiﬁe rs. Journal of Symbolic Logic 34, 257–263. Dekel, E., B. Lipman, and A. Rustichini (1998). Standard sta te-space models preclude un- awareness. Econometrica 66, 159–173. Enderton, H. B. (1972). A Mathematical Introduction to Logic. New York: Academic Press. Engelhardt, K., R. van der Meyden, and ...

View on Pith 1969

[2] [158]

An extended version with the title “Interactive unawar eness” will appear in the Journal of Economic Theory. Hintikka, J. (1962). Knowledge and Belief. Ithaca, N.Y .: Cornell University Press. Hughes, G. and M. Cresswell (1996). A New Introduction to Modal Logic. London: Rout- ledge. Kaplan, D. (1970). S5 with quantiﬁable propositional varia bles. Journal...

View on Pith 1962

[3] [355]

Kripke, S. (1959). A completeness theorem in modal logic. Journal of Symbolic Logic 24, 1–14. Lewis, H. R. (1979).Unsolvable Classes of Quantiﬁcational Formulas. New York: Addison- Wesley. 31 Modica, S. and A. Rustichini (1994). Awareness and partitional information structures. The- ory and Decision 37, 107–124. Modica, S. and A. Rustichini (1999). Unawar...

View on Pith 1959

[4] [2003]

30 Fagin, R., J. Y . Halpern, and M. Y . Vardi (1992). What can machines know? On the proper- ties of knowledge in distributed systems. Journal of the ACM 39(2), 328–376. Feinberg, Y . (2004). Subjective reasoning—games with unawareness. Technical Report Re- sarch Paper Series #1875, Stanford Graduate School of Business. Fine, K. (1969). For Some Proposit...

View on Pith arXiv 1992