Pith. sign in

REVIEW 5 major objections 8 minor 19 references

Inferentialist Public Announcement Logic: Base-extension Semantics

T0 review · 5 major / 8 minor · reviewed 2026-08-12 · deepseek-v4-flash

Pith's one-line read This paper presents a base-extension semantics for public announcement logic and proves it sound and complete with respect to the PAL axiomatic system.

desk verdict Genuinely new base-extension semantics for PAL with a real conceptual payoff, but the completeness proof has an unlicensed step and the key update lemma is sketched—worth refereeing, needs repair. read the letter →

arxiv 2411.15775 v3 pith:HNV5PBUL submitted 2024-11-24 math.LO

classification math.LO MSC 03B4503B42
keywords publicannouncementlogicbase-extensionsemanticsproof-theoreticmodalinferentialismS5dynamicepistemicmuddychildrenpuzzle
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

The paper extends base-extension semantics, a proof-theoretic semantics in which validity is defined by induction over bases of atomic rules, to public announcement logic (PAL). Its central goal is to show that announcement operators can be given a fully inferentialist account: an announcement updates the modal relations between bases rather than deleting worlds, and the resulting support relation is sound and complete with respect to the standard PAL axiomatic system (Theorems 3 and 4). A sympathetic reader should care because this establishes that dynamic epistemic reasoning about knowledge and public communication does not require Kripke truth-conditions; it can be grounded in atomic inference. The paper also reads the three-player card game and the muddy children puzzle through this semantics, showing that the inferentialist treatment forces all modelling assumptions to be made explicit as base rules.

What carries the argument

The machinery is the notion of a modal relation on bases (Definition 11), a binary relation $R_a$ between bases satisfying conditions (a)--(d) that control interaction with the subset relation and separate consistent from inconsistent bases; together with update sets (Definition 14), which add reachability and finiteness structure so that updates can always be performed. Announcements act on these relations: Definition 17 defines an effective update $R'_A$ of $R_A$ by $\phi$ at $B$ as an update set on an extended atom language whose reachable base pairs mirror the old relation restricted to bases supporting $\phi$, and Definition 24 constructs such an update explicitly using new atoms $p_\emptyset,p_i$ and the function $\delta_{\pi^+}$. The support relation (Definition 18) then evaluates $[\phi]\psi$ by quantifying over supersets and effective updates. This construction carries the soundness proof because Lemma 6 and Lemma 7 guarantee the updated relations are still modal relations and genuinely effective.

What would settle it

A concrete way to test the claim would be to take a small update set (for example, bases $B',C',B,C$ with $\phi$ holding at $B',B,C$ but not $C'$, as in the paper's Figure 9), compute the relation $R^+_{a|\phi}$ of Definition 24, and check directly whether it satisfies the Euclidean condition and conditions (c) and (d) of Definition 11 for all subsets and supersets; a single failure would refute Lemma 6 and collapse the soundness theorem. Alternatively, one could search for a PAL formula that is valid in the Kripke semantics but not supported by the base-extension semantics, which would refute Theorem 4.

Watch

Extended reading notes

Core claim

The paper claims that for every formula $\phi$ of PAL, $\vdash\phi$ iff $\Vdash\phi$: the arguments in the paper establish soundness (Theorem 3, every provable formula is supported at every base under every update set) and completeness (Theorem 4, every supported formula is provable in the PAL axiomatization, via the standard translation $t$ from PAL to S5 combined with S5 completeness). The key move is to treat an announcement $[\phi]$ not as deleting bases but as transforming the modal relations $R_a$ into a family of possible 'effective updates' $R_a|_{\phi}^{B}$, depending on the base $B$ at which the announcement is evaluated. Announcements therefore cease to be partial functions in this semantics, yet Lemma 8 shows all effective updates agree on formulae in the original language, so announcement validity is still well defined.

Load-bearing premise

The paper assumes that the explicit update construction of Definition 24, applied to any existing update set at a base where the announced formula holds, always produces relations satisfying the four modal-relation conditions of Definition 11 and the update-set conditions of Definition 14; the proof of this (Lemma 6) is a sketch, with the Euclidean case left as 'analogous'.

Editorial extensions

If this is right

  • The base-extension semantics for PAL is sound and complete, so proof-theoretic validity captures the full dynamic logic of truthful public announcements.
  • Announcements in this semantics are not unique updates: the same announcement at different bases produces different modal relations, but Lemma 8 ensures that any choice of effective update gives the same verdict on formulae in the original language.
  • The card-game and muddy-children analyses provide minimal base set-ups: any extension of those bases preserves the expected conclusions, and the muddy-children case shows that 'not muddy' must be positively supported rather than merely absent.
  • The completeness proof by translation gives a compositional reduction of PAL back to S5, so the dynamic announcement axioms are exactly what is needed to eliminate announcement operators in the base-extension setting.

Reading between the lines

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

  • If soundness and completeness hold for PAL, the same update-relations technology is a plausible starting point for action model logic, where agents' uncertainty about which action occurred could be encoded as uncertainty between candidate modal relations.
  • The dependence of effective updates on the base suggests an intensional notion of informational equivalence: two updates can be semantically equivalent for the original language while differing on atoms added during the update; making this precise could connect to unsuccessful announcements and common knowledge.
  • The authors' explicit positive encoding of negative facts in the muddy children example invites a testable modelling principle: in base-extension models of epistemic puzzles, every frame assumption that a modeller would 'build into' the Kripke valuation must appear as base rules or positive support conditions, otherwise announcements misfire.
  • It would be a natural extension to check whether the muddy-children observation scales: for $n$ children and $m$ muddy children, requiring explicit support of all negated $m_j$ at the appropriate bases should let the $m$-step solution be reproduced in this semantics.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

5 major / 8 minor

Summary. The paper develops a base-extension semantics (B-eS) for public announcement logic (PAL). Extending the authors' earlier B-eS for multi-agent S5, it evaluates formulas at bases (sets of atomic rules) connected by 'modal relations', and it interprets announcements [φ]ψ as updates of those modal relations rather than as deletions of worlds. Because restricting a modal relation to bases that agree on φ need not yield a modal relation, the authors introduce 'effective updates' (Definition 17) and allow the same announcement to produce several possible updated relation sets, so that [φ] is a genuinely box-like operator. The main theorems are Theorem 3 (soundness: ⊢φ implies ⊩φ) and Theorem 4 (completeness: ⊩φ implies ⊢φ), the latter via a translation t: PAL → S5. The paper closes with an analysis of the three-player card game and the muddy children puzzle; a distinctive claim is that the muddy-children reasoning requires bases to support negative information ('Anne is not muddy') rather than merely failing to support 'Anne is muddy'.

Significance. If the technical results can be repaired, this is the first base-extension semantics for a dynamic epistemic logic and a nontrivial extension of proof-theoretic semantics from static modal logics to epistemic actions. The innovation of evaluating announcements against a set of 'effective updates' is well motivated by the concrete failure example in Section 5 and gives announcements a genuinely intensional reading. The two case studies are a strength: Propositions 2 and 3 turn the muddy-children example into testable claims about which base rules must be explicit, and the authors are careful to disclaim strong minimality. There are no machine-checked proofs or executable artifacts; the paper's value is conceptual, and its central claims are currently gated because the completeness proof contains an unlicensed step and the update construction (Lemma 6) is verified only in sketch form.

major comments (5)
  1. [Section 5, proof of Theorem 4] The proof of Theorem 4, the completeness of the base-extension semantics for PAL, is circular as written. After assuming ⊩φ, the proof states 'By Theorem 3 and Lemma 21, we get ⊢φ↔t(φ)'. Theorem 3 is soundness (⊢ψ ⇒ ⊩ψ), and Lemma 21 gives only the semantic equivalence ⊩φ↔t(φ); their conjunction licenses at most ⊩t(φ), never ⊢φ↔t(φ). To conclude ⊢φ from ⊢S5 t(φ), the syntactic translation lemma ⊢PAL φ↔t(φ) is required, and it is neither stated nor proved; it cannot be derived from the semantic lemma without assuming the very completeness that Theorem 4 is meant to establish. The repair is straightforward and the infrastructure is present: the axioms of Definition 8 are biconditionals, and the complexity inequalities of Lemma 20 are exactly those needed for an induction on c(φ) (Definition 26) proving ⊢PAL φ↔t(φ). The proof of Theorem 4 should be rewritten around this syntactic lemma. Note also that citing Theorem 1 for the S5 completeness of t(φ) is imprecise: since PAL-validity of announcement-free formulas is stated relative to update sets (Definition 15), Theorem 2 is the relevant completeness result, and the coincidence of the two validity notions on announcement-free formulas should be stated explicitly.
  2. [Section 5, Lemma 6 and Definitions 20–24] Lemma 6 is the linchpin of the update semantics: it asserts that the relation R+_{A|φ} built in Definition 24 is an S5-modal relation and an update set, and it underpins Corollary 1, Lemma 7, Lemma 17, and hence the soundness of the announcement axioms. As written, its proof is a sketch with several unverifiable steps. (a) The Euclidean case is dismissed with 'follows analogously'; because clause (3) of Definition 24 requires compatibility of two bijections f and g, the Euclidean composition argument needs to be written out as it is (partially) for transitivity. (b) In the proof of modal-relation condition (c) of Definition 11, the text writes δπ+(B+) = {δ | δ ⊂ S*_{A|φ} and B+ ∈ δ}, but Definition 23 defines the elements of δπ+(·) as collections of blocks π+_i of π+; under the definition as written, the displayed identity is not meaningful, and neither is the instruction to obtain C′ 'by simply adding rules'. (c) The verification of the update-set condition claims that (C′′−r), ((C′′−r)−r′), and (C′′−r′) belong to π+_i, but membership in π+_i requires membership in the domain/range of S*_{a|φ}; the proof does not show that removing rules from bases in S*_{a|φ} preserves this membership, which is precisely where condition (d) of Definition 11 must be invoked. (d) The proof uses the symbol δw(C′), which is never defined in the main text. The construction of Definitions 21–24 and the verification of Lemma 6 should be presented in full.
  3. [Definition 18, clause for Kaφ with non-empty Δ] The definition of support for Kaφ after an announcement is type-incoherent as written. The clause reads: 'if Δ is non-empty, then for all C⊇B, R′_A∈RA|ΔC, updates C+ of C and C′ s.t. R′_aC+C′, ⊩^Δ_{C′,RA}φ'. By Definition 17, R′_a is a relation on the extended base set Ω_{P′}, so the target C′ is an updated base in Ω_{P′}; but the support relation in the conclusion is evaluated with the original update set RA, which is defined on Ω_P. The support relation of Definition 18 is only defined for bases in the language of the ambient update set, so the clause as written has no defined meaning. The intended reading is presumably ⊩^Δ_{C′,R′_A}φ, which would be consistent with Lemma 8 (where support after an effective update is evaluated with the updated relations in the subscript); alternatively the paper must explain how RA is extended to Ω_{P′} and why the choice of the particular effective update does not matter. Because the proof of the announcement-and-knowledge axiom in Lemma 18 unpacks this clause directly, the definition and that proof need to be aligned and stated precisely.
  4. [Section 5, Lemma 17] Lemma 17, the equivalence used to prove the announcement-and-knowledge axiom [φ]K_aψ ↔ φ→K_a[φ]ψ in Lemma 18, is not proved as written. The two conditions are stated with different and partially implicit quantifier structures, and neither direction is checked against Definition 17 clause 3. In the direction from 1 to 2, the proof derives from (1) a particular pair C⊇B and D with R_aCD, applies condition (d) to obtain X⊆D with R_aBX, and then concludes the universal statement 'for all X s.t. R_aBX and Y⊇X, if ⊩_{Y,RA}φ then ⊩^φ_{Y,RA}ψ'; the step from the particular D to the universal quantification over all Y⊇X is not justified, and the proof never passes from the given X of (2) to the C,D of (1). In the direction from 2 to 1, the proof starts from X (with R_aBX) and Y⊇X, obtains C⊇B with R_aCY by symmetry and condition (c), and asserts that an effective update R′_A connects C+ and Y+; by Definition 17 clause 3 this requires ⊩_{C,RA}φ in addition to R_aCY and ⊩_{Y,RA}φ, which is not established. A correct proof of 2→1 would instead apply condition (d) to R_aCD with the subset B⊆C, yielding X⊆D with R_aBX, and then invoke (2) with Y=D using ⊩_{D,RA}φ, which is available from Definition 17 clause 3. Please restate Lemma 17 with explicit quantifier prefixes and supply both directions.
  5. [Section 4 (Theorems 1–2) and Appendix A] The soundness and completeness theorems of this paper rest on the S5 base-extension results, but the proof layer below Lemma 6 is not fully available to the reader. Theorem 1 is imported from the authors' companion paper [7]; Theorem 2, the update-set variant that the PAL semantics actually uses, delegates both directions to [7], with the update-set adaptation of one direction relegated to Appendix A. The appendix is itself a sketch: it repeats the hand-wave 'The Euclidean case follows analogously', it invokes an undefined atom q_w ('By Lemma 5, we know there is a maximally-consistent C ⊇ A_w s.t. ⊩C q_w'), and the verification of the final update-set clause for sub- and supersets is compressed into a single paragraph whose key claim (reachable bases must have δ_W of equal length) is asserted rather than proved. Since Theorem 4 applies S5 completeness to the translation t(φ) and since Lemma 6's proof explicitly mimics the appendix construction, the completeness chain is only as solid as this appendix. The authors should either re-prove the S5 update-set results in full or restructure the presentation so that the foundational layer is self-contained and verifiable.
minor comments (8)
  1. [Section 1, third paragraph] Two consecutive sentences refer to 'the first [6]' and 'the second [6]', although they describe two different papers; the second citation should presumably be [7].
  2. [Reference list, item [1]] The Baltag–Moss–Solecki entry is corrupted: 'S/suppress lawomir Solecki' should read 'Sławomir Solecki'.
  3. [Definitions 12, 15, and 18] The clause for implication is written as '⊩_{B,RA} ϕ→ψ iff ϕ ⊩_{B,RA} ψ', which silently invokes the nonempty-Γ clause (with Γ={ϕ}) defined only afterwards; reordering the clauses, or writing '{ϕ} ⊩_{B,RA} ψ', would remove a real source of confusion.
  4. [Definition 18, final validity clause] The last sentence of Definition 18 quantifies over 'sets of S5-modal relations RA', although both the opening of that definition and Definition 15 restrict attention to update sets; this appears to be a slip.
  5. [Section 6.1, Proposition 1] The conclusion of Proposition 1 is written with the turnstile '⊢B012,RA [¬1a]Kc(0a∧1b∧2c)'; since the claim is about support at a base, the symbol should be '⊩B012,RA'.
  6. [Section 5, Lemma 20] The proof of Lemma 20 contains typographical errors: 'c([ϕ]ψ→χ)' should read 'c([ϕ](ψ→χ))', and 'c([ϕ][ψ]χ) = (2+c(ϕ))×((2+c(ψ))×c(χ)' together with the following displayed line are missing closing parentheses.
  7. [Section 2.2 and Section 5] The text contains a number of small language slips, e.g., 'any formula that is false on a Kripke modal' (should be 'Kripke model'), 'so used to proof the same' (should be 'prove'), and Lemma 14 begins 'We proof this by induction' (should be 'prove').
  8. [Definition 22] The definition of C+ (the update of a base) is barely comprehensible as printed; the ranges of the indices in 'p′_0,...,p′_i ⇒ p_∅' and in '{p_1,...,p_n}\{p_k}' and the role of the added rules should be explained in prose, since this construction is the heart of Lemma 6.

Circularity Check

1 steps flagged · score 7.0 of 10

Theorem 4's completeness proof is circular: it converts the semantic equivalence ⊩ϕ↔t(ϕ) into the syntactic equivalence ⊢ϕ↔t(ϕ) using a soundness theorem that only licenses the reverse direction.

  1. other [Section 5, proof of Theorem 4]
    "Assume ⊩ ϕ. By Theorem 3 and Lemma 21, we get ⊢ ϕ↔ t(ϕ). Since t(ϕ) does not contain any announcement formulae andS5 is complete (see Theorem 1), we have⊢S5 t(ϕ). Since PAL is an extension of S5, we also have ⊢t(ϕ) and so⊢ϕ."

    Theorem 3 is the soundness direction only: it licenses passing from ⊢ψ to ⊩ψ. Lemma 21 supplies only the semantic biconditional ⊩ϕ↔t(ϕ). From these two facts one cannot infer the syntactic biconditional ⊢ϕ↔t(ϕ); doing so is exactly to invoke the completeness statement being proved, namely that semantic validity implies provability. The later appeal to S5 completeness for t(ϕ) does not help, because without ⊢PAL ϕ↔t(ϕ) the provability of t(ϕ) does not transfer to ϕ. The paper does not prove ⊢PAL ϕ↔t(ϕ) separately, so the main completeness theorem is not established as written; the argument reduces to its own target. The gap is repairable by an induction using Definition 26 and Lemma 20, but the text as it stands is circular.

full rationale

The paper contains substantial new PAL-specific content—effective updates, support clauses for announcements, and the worked examples—so this is not a bare renaming of a known result, and the standard translation from PAL to S5 is a legitimate strategy. However, the proof of Theorem 4 contains a genuine circular step: after assuming ⊩ϕ, it claims that Theorem 3 and Lemma 21 yield ⊢ϕ↔t(ϕ). Theorem 3 is only soundness (⊢⇒⊩), and Lemma 21 gives only the semantic biconditional; the move to the syntactic biconditional is precisely the completeness direction the theorem is supposed to establish. Without an independent proof of ⊢PAL ϕ↔t(ϕ), the main completeness claim is unproven as written. Other concerns are not circular in the same way: the reliance on the authors' earlier S5 completeness theorem [7] is a load-bearing citation, but it concerns S5 rather than the PAL target, and the appendix adapts that construction rather than assuming the present result. The sketchiness of Lemma 6 is a completeness gap rather than a circularity. Overall, the central derivation has a circular step, but the surrounding framework has independent content, so the score is high but not maximal.

Assumptions & free parameters 0 free parameters · 3 assumptions · 3 invented entities

The paper's semantic framework rests on the authors' prior S5 base-extension semantics [7] (soundness and completeness, update-set machinery) and on the standard S5 axiomatic completeness. The PAL-specific novelty is the effective-update construction, but its correctness is asserted via sketched proofs. No numerical free parameters appear; the 'free choices' are structural (choice of bases, relations, partitions), not fitted parameters.

assumptions (3)
  • standard math The axiomatic system for S5 (Definition 4) is sound and complete with respect to S5 Kripke semantics.
    Treated as a known background result (cited via [9]); used in Theorem 4 to conclude ⊢S5 t(φ).
  • domain assumption The base-extension semantics for S5 (with and without update sets) is sound and complete, as established in [7].
    Theorems 1 and 2 are taken from the authors' own previous paper [7]; the present paper does not re-prove them and the appendix only sketches the adaptation to update sets. This is the main external load-bearing result.
  • domain assumption Every base in an update set has a finite partition πB satisfying the conditions of Definition 14.
    This is part of the definition of update set, but the existence for the constructed relations in the completeness proof is asserted and proved only as a sketch in Appendix A.
invented entities (3)
  • Effective update R_A|φB
    purpose: Semantic value of a public announcement [φ]: a set of updated modal relations, possibly multiple, over an extended atom set P+.
    A definitional device; the paper notes announcements are no longer partial functions in this semantics, and there is no external falsifiable handle.
  • Updated bases C+ (Definition 22)
    purpose: Track which reachable bases survive an announcement, by adding rule-schemata over new atoms.
    Auxiliary construction used to ensure updated relations remain modal relations.
  • δπ+ function (Definition 23)
    purpose: Bookkeeping device to identify which partition cells a base intersects, used to define the updated relations.
    Technical device in the construction; no independent evidence.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Inferentialist Public Announcement Logic: Base-extension Semantics." pith.science (2026). https://pith.science/paper/HNV5PBUL

@misc{pith2026241115775,
  author       = {Pith},
  title        = {Pith review of: Inferentialist Public Announcement Logic: Base-extension Semantics},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/HNV5PBUL}},
  note         = {Machine review of arXiv:2411.15775}
}
abstract

Proof-theoretic semantics, and base-extension semantics in particular, can be seen as a logical realization of inferentialism, in which the meaning of expressions is understood through their use. We present a base-extension semantics for public announcement logic, building on earlier work giving a base-extension semantics for the modal logic $S5$, which in turn builds on earlier such work for $K$, $KT$, $K4$, and $S4$. These analyses rely on a notion of `modal relation' on bases. The main difficulty in extending the existing B-eS for $S5$ to public announcement logic is to account announcements of the form $[\psi]\phi$, which, in this setting, update the modal relations on bases. We provide a detailed analysis of two classical examples, namely the three-player card game and the muddy children puzzle. These examples illustrate how the inferentialist perspective requires fully explicit information about the state of the participating agents.

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

19 extracted references · 19 canonical work pages

  1. [7]

    Timo Eckhardt and David J. Pym. Base-extension semantics for S5 modal logic. Logic Journal of the IGPL , 2025

  2. [1]

    Moss, and S/suppress lawomir Solecki

    Alexandru Baltag, Lawrence S. Moss, and S/suppress lawomir Solecki. The Logic of Public Announcements, Common Knowledge, and Private Suspicions. In I. Gilboa, edi- tor, Proceedings of the 7th Conference on Theoretical Aspects of Rationality and Knowledge, pages 43–56, 1998

  3. [2]

    Making It Explicit: Reasoning, Representing, and Discursive Commitment

    Robert Brandom. Making It Explicit: Reasoning, Representing, and Discursive Commitment. Harvard University Press, Cambridge, Mass., 1994

  4. [3]

    Articulating reasons: An introduction to inferentialism

    Robert Brandom. Articulating reasons: An introduction to inferentialism . Harvard University Press, 2009

  5. [4]

    Dynamic Epistemic Logic

    Hans van Ditmarsch, Wiebe van der Hoek, and Barteld Kooi. Dynamic Epistemic Logic. Springer Publishing Company, Incorporated, 1st edition, 2007

  6. [5]

    The logical basis of metaphysics

    Michael Dummett. The logical basis of metaphysics . Duckworth, London, 1991

  7. [6]

    Timo Eckhardt and David J. Pym. Base-extension semantics for modal logic. Logic Journal of the IGPL , 2024

  8. [8]

    On an inferential semantics for classical logic

    David Makinson. On an inferential semantics for classical logic. Logic Journal of the IGPL, 22(1):147–154, 2014

Show all 19 references
  1. [9]

    Meyer, J.-J. Ch. and Hoek, W. van der.Epistemic Logic for AI and Computer Sci- ence. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1995

  2. [10]

    Completeness in Proof-Theoretic Semantics , pages 231–251

    Thomas Piecha. Completeness in Proof-Theoretic Semantics , pages 231–251. Springer International Publishing, Cham, 2016

  3. [11]

    The definitional view of atomic systems in proof-theoretic semantics

    Thomas Piecha and Peter Schroeder-Heister. The definitional view of atomic systems in proof-theoretic semantics. In The Logica Yearbook 2016. Universit¨ at T¨ ubingen, 2017

  4. [12]

    Incompleteness of intuitionistic propositional logic with respect to proof-theoretic semantics

    Thomas Piecha and Peter Schroeder-Heister. Incompleteness of intuitionistic propositional logic with respect to proof-theoretic semantics. Studia Logica, 107(1):233–246, 2019

  5. [13]

    Ideas and results in proof theory

    Dag Prawitz. Ideas and results in proof theory. In J.E. Fenstad, editor, Proceed- ings of the Second Scandinavian Logic Symposium, volume 63 of Studies in Logic and the Foundations of Mathematics , pages 235–307. Elsevier, 1971

  6. [14]

    Meaning approached via proofs

    Dag Prawitz. Meaning approached via proofs. Synthese, 148:507–524, 2006

  7. [15]

    An Inferentialist Interpretation of Classical Logic

    Tor Sandqvist. An Inferentialist Interpretation of Classical Logic. Uppsala prints and preprints in philosophy. Univ., Department of Philosophy, 2005

  8. [16]

    Classical logic without bivalence

    Tor Sandqvist. Classical logic without bivalence. Analysis, 69(2):211–218, 2009

  9. [17]

    Base-extension semantics for intuitionistic sentential logic

    Tor Sandqvist. Base-extension semantics for intuitionistic sentential logic. Logic Journal of the IGPL , 23(5):719–731, 2015

  10. [18]

    Validity concepts in proof-theoretic semantics

    Peter Schroeder-Heister. Validity concepts in proof-theoretic semantics. Synthese, 148(3):525–571, 2006

  11. [19]

    Proof-Theoretic versus Model-Theoretic Consequence

    Peter Schroeder-Heister. Proof-Theoretic versus Model-Theoretic Consequence. In Michal Pelis, editor, The Logica Yearbook 2007. Filosofia, 2008. 40 A Proof Details Elided in Main Text This construction is an adaptation of the proof of Soundness for S5 base-extension semantics ...

Pith tools

Reviewed August 12, 2026 · model on record in the stance chip above.