NNIL-formulas revisited: universal models and finite model property

Dick de Jongh; Fan Yang; Julia Ilin

NNIL-formulas revisited: universal models and finite model property

T0 review · 0 major / 6 minor · reviewed 2026-08-14 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read NNIL formulas are exactly the intuitionistic formulas preserved by arbitrary substructures, with a finite universal tree model as the witness.

desk verdict The n-universal model for NNIL-formulas is a genuinely new tool; the paper is sound, with one manageable external dependency in the headline subframe-logic generalization. read the letter →

arxiv 1908.01635 v2 pith:YI6WEJOJ submitted 2019-08-05 math.LO

Julia Ilin , Dick de Jongh , Fan Yang This is my paper · ORCID

classification math.LO MSC 03B2003B5503F55

keywords NNIL-formulasintuitionisticlogicuniversalmodelssubframelogicsfinitemodelpropertymonotonicmapsMR-formulasrelationalsemantics

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 establishes a sharp semantic boundary for NNIL, the intuitionistic propositional formulas that forbid nesting of implication on the left. It proves that being an NNIL formula is the same as being reflected by color-preserving monotonic maps between relational models, and the same as being preserved under arbitrary substructures, not only the topo-subframes usually required. The argument runs through a finite rooted n-universal model built out of finite trees, in which every upset is definable by a NNIL-subframe formula. From this the paper derives that every logic axiomatized by NNIL formulas, equivalently every intermediate subframe logic, has the finite model property and is canonical.

What carries the argument

The engine is the color-preserving monotonic map: an order-preserving function between relational models that leaves the truth values of the $n$ proposition letters unchanged. Against it, the paper sets NNIL-subframe formulas $\beta(N)$, inductively built from a finite rooted model $N$, with the refutation criterion that a frame $F$ falsifies $\beta(N)$ exactly when a color-consistent monotonic map from the unraveled tree $N^t$ into $F$ exists. The universal model $T(n)$ is then assembled from finite trees as nodes, ordered by existence of these maps; its key property is that every finite $n$-tree maps back and forth into a unique representative in $T(n)$, which makes the model exact for NNIL and MR.

What would settle it

Try to find any intermediate subframe logic whose frame class is not closed under arbitrary substructures; the paper's Corollary 4.13 predicts none exists. More locally, the refutation criterion would be overturned by a finite rooted $n$-model $N$ and a descriptive frame $F$ that refutes $\beta(N)$ while admitting no color-consistent monotonic map from the unraveled tree $N^t$ into $F$.

Watch

Extended reading notes

Core claim

On the paper's own terms, the central discovery is that a finite tree-like model $T(n)$ is an exact $n$-universal model simultaneously for NNIL-formulas and for MR-formulas, the formulas reflected by color-preserving monotonic maps. For every finite $n$-tree there is exactly one node $T_w$ of $T(n)$ equivalent to it under two-way color-preserving monotonic maps, and every upset of $T(n)$ is definable by a conjunction $\beta^+(U)$ of NNIL-subframe formulas. The paper then derives that NNIL and MR coincide: every MR-formula is equivalent to a finite conjunction of NNIL-subframe formulas, and NNIL-formulas are exactly the formulas reflected by color-preserving monotonic maps. It also derives that logics axiomatized by NNIL formulas are precisely the intermediate subframe logics, that their frame classes are closed under arbitrary substructures, and that these logics are canonical and have the finite model property.

Load-bearing premise

The paper's broadest conclusion, that every intermediate subframe logic has a frame class closed under arbitrary substructures, rests on an imported theorem that every intermediate subframe logic is axiomatized by NNIL-subframe formulas; the paper does not prove that theorem.

Editorial extensions

If this is right

Every MR-formula is equivalent to a finite conjunction of NNIL-subframe formulas, so the two classes coincide up to equivalence; in particular, formulas reflected by color-preserving monotonic maps are exactly NNIL formulas.
The frame class of any intermediate subframe logic is closed under arbitrary substructures, not only topo-subframes, and every such logic is canonical.
Every logic axiomatized by NNIL or MR formulas has the finite model property, obtained here by a direct finite color-preserving submodel reduction.
The $n$-universal model $T(n)$ is finite and rooted, isomorphic to the $n$-canonical model, and exact: every upset is NNIL-definable.

Reading between the lines

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

The finite reduction theorem is constructive in the number of colors; a natural next step, not taken in the paper, is to extract explicit bounds on countermodel size and see whether NNIL fragments have tractable finite-model-finding.
The same 'closed under arbitrary substructures' test could be applied to modal subframe logics: the paper leaves open whether a syntactic characterization exists, and the color-consistent map criterion is a candidate discriminating principle.
Because every upset of $T(n)$ is definable by a $\beta^+$ formula, the $\mathrm{NNIL}_n$ Lindenbaum-Tarski algebra has a transparent representation; this may make interpolation or correspondence questions for the fragment easier to settle.

Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

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

Desk Editor's Note

read the letter

You should know two things about this paper. First, the construction of T(n), the exact n-universal model for NNIL- and MR-formulas, is real and self-contained. I checked the main inductions—Proposition 4.4's fixed-point argument, Theorem 4.9's back-and-forth map, Proposition 4.10's beta-plus exactness—and they hold together. Second, the advertised closure of all intermediate subframe logics under arbitrary substructures (Corollary 4.13) is not self-contained; it rests on Bezhanishvili's Theorem 3.4, imported without proof from his thesis. That is the load-bearing dependency, and it is the only place I worried about a hidden hypothesis.

What is actually new: the T(n) construction itself, its exactness, and the consequence that every MR-formula is a finite conjunction of B-subframe formulas (Corollary 4.11). The paper also uses a neat filtration-like method—color-preserving submodels—to give a new proof of FMP for NNIL-axiomatized logics. It openly says FMP and canonicity were already known; the FMP proof in [18] is disclosed. That is honest scholarship.

The soft spots are minor. Lemma 5.3's existence argument skips the case where a successor of the root has the same color as the root; the fix is simple (take the root itself) but the proof should say so. Proposition 4.4 relies on an implicit invariant that colors strictly increase away from every tree root; it is true and easy to state, but currently backgrounded. The more substantive caveat is the external Theorem 3.4. If its statement is exactly what the paper needs—every intermediate subframe logic is NNIL-axiomatized with NNIL-subframe formulas in the class B—then Corollary 4.12 and 4.13 go through. I did not find a mismatch, but the paper should make the precise usage explicit. Reassuringly, the FMP result in Theorem 5.8 does not need that external theorem: by Corollary 4.11, an NNIL-axiomatized logic is also B-axiomatized, and then Corollary 3.8 alone gives the needed substructure closure.

Who should read this: people working on intuitionistic logic, universal models, or subframe logics. It is a competent, useful contribution, not a radical one. It deserves a serious referee who knows the [3] theorem.

Recommendation: send it to peer review. The revisions are small: fix the root case in Lemma 5.3, make the Prop 4.4 invariant explicit, and flag the external dependency clearly.

Referee Report

0 major / 6 minor

Summary. The paper studies NNIL-formulas of intuitionistic propositional logic and their model-theoretic behaviour. It first proves a refutation criterion (Theorem 3.3): a formula beta(N) associated with a finite rooted n-model N fails on an n-model M exactly when the unraveling N^t maps monotonically and color-preservingly into M. This is generalized to color-consistent maps into arbitrary Kripke or descriptive frames (Theorem 3.7), yielding preservation of the class B of NNIL-subframe formulas under arbitrary substructures, without the topo-subframe condition (Corollary 3.8). The authors then construct a finite exact n-universal model T(n) for NNIL- and MR-formulas (Proposition 4.10), prove that every finite n-tree is MR-equivalent to a unique node of T(n) (Theorem 4.9), and derive that NNIL-formulas are exactly the formulas reflected by color-preserving monotonic maps and that every MR-formula is equivalent to a finite conjunction of B-formulas (Corollary 4.11). They connect these results to subframe logics (Corollary 4.12) and canonicity (Corollary 4.13), and prove finite model property for logics axiomatized by NNIL- or MR-formulas (Theorem 5.8) using finite color-preserving submodels. The universal-model and B/NNIL/MR portions are self-contained; the statements about all subframe logics rely on Theorem 3.4, imported from Bezhanishvili's thesis.

Significance. If the results hold, the paper is a substantial contribution to the model theory of intuitionistic logic. The construction of T(n) as a finite exact n-universal model for NNIL- and MR-formulas is elegant and gives a new structural proof that NNIL equals both MR and the class of finite conjunctions of B-formulas. The refutation criterion via color-consistent monotonic maps is clean, and the finite-model-property proof via color-preserving submodels is a genuinely different route from earlier canonical-formula arguments. The paper is for the most part carefully written and contains detailed proofs of the universal-model facts, including exact definability of every upset by beta_+(U) and the isomorphism with the n-canonical model. The main caveat is that the extension from B-axiomatized logics to 'all subframe logics' in Corollaries 4.12 and 4.13 is not self-contained: it passes through Theorem 3.4, cited from [3] without proof. This does not appear to be a flaw in the paper's own derivations, but it is a dependency that should be made explicit and verified against the exact form of Definition 3.1.

minor comments (6)

[§3, Theorem 3.4; §4, Corollaries 4.12–4.13] Please add a sentence stating explicitly that the equivalence with subframe logics and the canonicity corollary are conditional on Bezhanishvili's Theorem 3.4, cited from [3], and verify that the NNIL formulas axiomatizing subframe logics in [3] are indeed of the form given in Definition 3.1. The self-contained part of the paper establishes the B/NNIL/MR equivalences and the substructure preservation for B-formulas; the step to 'all subframe logics' is the one place where the paper relies on an external result.
[§5, Lemma 5.3] The proof of Lemma 5.3 does not explicitly treat the root case in the verification that N is color-preserving. If w is the root and a successor u has the same color as the root, the required witness is v = w; if the color is strictly larger, take the first node on the path where the color jumps. Please spell this out, because as written the phrase 'since col(w0) < col(w)' only applies after the root case is separated.
[§4, Proposition 4.4(1)] The proof of Proposition 4.4(1) uses the fact that no element of X contains a node of the color of the fresh root w. This follows from persistence and from the construction because every node in a tree Tw_i has color at least the color of its root, which is strictly larger than col(w); please state this invariant explicitly, since it is otherwise easy to miss.
[§4, Proposition 4.10(2)] In the proof of Proposition 4.10(2), the last displayed sentence says 'Tu does not satisfy beta_+(w)' but the formula is beta_+(U); please correct the variable.
[Abstract and §1] There are several typos: 'formulas that does not allow' should be 'formulas that do not allow'; 'subsitutions' should be 'substitutions'; and the abstract contains an awkward 'i.e.i' fragment. These should be cleaned up.
[§4, Definition 4.1] Definition 4.1(ii) contains a double period after 'V(phi) = U'; also, since T(n) is finite, it may be worth noting explicitly that the model satisfies the stronger 'exact' condition for all upsets, not only point-generated ones, as is done later in Proposition 4.10.

Circularity Check

0 steps flagged · score 0.0 of 10

No derivation reduces to its own inputs: the universal-model construction, the NNIL/MR characterization, and the FMP proof are self-contained, and the one imported axiomatization theorem is external to the author set, not a self-citation.

full rationale

I walked the paper's derivation chain and found no step in which a claimed prediction or conclusion is equivalent to its inputs by construction. The NNIL-subframe formulas beta(N) are defined independently from arbitrary finite rooted n-models, and Lemma 3.2 and Theorem 3.3 establish the refutation criterion by induction; the use of Lemma 2.2 is backed by a proof included in the text. Corollary 3.8, the preservation of B-formulas under arbitrary substructures, follows from Theorem 3.7, whose color-consistent map argument is self-contained. The universal model T(n) is constructed from finite color-decreasing trees, and Proposition 4.10(2) defines beta+(U) as a finite conjunction of the previously defined beta(v)-formulas; the proof of exactness uses Lemma 3.2 and Theorem 3.3 rather than assuming the NNIL-definability it establishes. Corollary 4.11, that every MR-formula is equivalent to a finite conjunction of B-formulas, is derived from the universal-model exactness, and the equivalence NNIL = MR is therefore a proven consequence, not a renamed input. The only substantive imported result is Theorem 3.4, taken from N. Bezhanishvili's 2006 thesis, which states that every intermediate subframe logic is axiomatized by NNIL-formulas. That theorem is external, is not by any of the current authors, and is invoked as a premise rather than justified by the present derivation; if it were unsupported, the all-subframe-logics corollary would be weakened, but that would be a question of external support, not circularity. The FMP proof in Theorem 5.8 uses the proven color-preserving submodel theorem and the substructure closure, and no fitted parameter is renamed as a prediction. I therefore find no circular step and assign score 0.

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

The central results carry no fitted constants. The universal model depends only on the number n of variables as an index. The substantive imported premises are the finite model property of IPC and Bezhanishvili's theorem that all intermediate subframe logics have NNIL-subframe axiomatizations. No new entities with external empirical content are introduced.

assumptions (2)

standard math IPC has the finite model property with respect to finite rooted Kripke trees; a non-derivable rule phi nobdash psi has a finite tree countermodel.
Used in Proposition 4.10(1) to produce the finite tree that is then matched to a node of T(n); standard completeness result not proved in the paper.
domain assumption Theorem 3.4: every intermediate subframe logic is axiomatizable by NNIL-subframe formulas, due to Bezhanishvili 2006, Cor. 3.4.16.
Imported without proof and used in Corollaries 4.12 and 4.13 to extend B-axiomatizability and substructure closure to all subframe logics.

how reviews work

0 comments

Cite this review

Pith. "Pith review of NNIL-formulas revisited: universal models and finite model property." pith.science (2026). https://pith.science/paper/YI6WEJOJ

@misc{pith2026190801635,
  author       = {Pith},
  title        = {Pith review of: NNIL-formulas revisited: universal models and finite model property},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/YI6WEJOJ}},
  note         = {Machine review of arXiv:1908.01635}
}

abstract

NNIL-formulas, introduced by Visser in 1983-1984 in a study of $\Sigma_1$-subsitutions in Heyting Arithmetic, are intuitionistic propositional formulas that does not allow nesting of implication to the left. The first results about these formulas were obtained in a paper of 1995 by Visser et al. In particular, it was shown that NNIL-formulas are exactly the formulas preserved under taking submodels of Kripke models. Recently Bezhanishvili and de Jongh observed that NNIL-formulas are also reflected by color-preserving monotonic maps of Kripke models. In the present paper, we first show how this observation leads to the conclusion that NNIL-formulas are preserved by arbitrary substructures not necessarily satisfying the topo-subframe condition. Then we apply it to construct universal models for NNIL. It follows from the properties of these universal models that NNIL-formulas are also exactly the formulas that are reflected by color-preserving monotonic maps. By using the method developed in constructing the universal models, we give a new direct proof that the logics axiomatized by NNIL-axioms have the finite model property.

Figures

Figures reproduced from arXiv: 1908.01635 by the authors.

**Figure 1.** A fragment of U(2) – For each element w in the mth layer, and each color c < col(w), add a new node u to layer m+ 1 with color c and with w the only immediate successor of u. – For each set X = {w1, . . . , wk} (k ≥ 2) of pairwise R-incomparable elements in layers ≤ m containing at least one member from layer m, and each color c less than or equal to the color of all nodes in X, add a new node w to layer m + 1 with … view at source ↗

**Figure 2.** T (2) 17 [PITH_FULL_IMAGE:figures/full_fig_p017_2.png] view at source ↗

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

30 extracted references · 30 canonical work pages

[18]

J. Ilin, D. de Jongh, and F. Yang. NNIL axioms have the ﬁni te model property. In J. van Eijck, R. Iemhoﬀ, and J. Joosten, editors, Liber Amicorum Alberti, volume 30 of Tributes, pages 177–185. College pub- lications, 2016

work page 2016
[3]

Bezhanishvili

N. Bezhanishvili. Lattices of Intermediate and Cylindric Modal Logics. PhD thesis, University of Amsterdam, 2006. Available at http://www.illc.uva.nl/Research/Publications/Dissertations/DS-2006-02.text.pdf

work page 2006
[1]

Bellissima

F. Bellissima. Finitely generated free Heyting algebra s. Journal of Symbolic Logic, 51:152–165, 1986

work page 1986
[2]

Bezhanishvili and S

G. Bezhanishvili and S. Ghilardi. An algebraic approach to subframe logics. Intuitionistic case. Ann. Pure Appl. Logic, 147(1-2):84–100, 2007

work page 2007
[4]

Bezhanishvili

N. Bezhanishvili. Frame based formulas for intermediat e logics. Studia Logica, 90:139–159, 2008

work page 2008
[5]

Bezhanishvili, D

N. Bezhanishvili, D. Coumans, S. van Gool, and D. de Jongh . Dual- ity and universal models for the meet-implication fragment of IPC. In M. Aher, D. Hole, E. Jeˇ r´ abek, and C. Kupke, editors,Logic, Language, and Computation: 10th International Tbilisi Symposium on Logi c, Lan- guage, and Computation, TbiLLC 2013, Gudauri, Georgia, Septemb er 23-27, 2013...

work page 2013
[6]

Bezhanishvili and D

N. Bezhanishvili and D. de Jongh. Stable logics in intuit ionistic logic. Notre Dame Journal of Formal Logic , 59(3):307–324, 2018

work page 2018
[7]

Bezhanishvili, D

N. Bezhanishvili, D. de Jongh, A. Tzimoulis, and Z. Zhao. Univer- sal models for the positive fragment of intuitionistic logi c. In Logic, Language, and Computation - 11th International Tbilisi Sympos ium, TbiLLC 2015, Tbilisi, Georgia, September 21-26, 2015, Revised S e- lected Papers, pages 229–250, 2015

work page 2015

Show all 30 references

[8]

Chagrov and M

A. Chagrov and M. Zakharyaschev. Modal logic, volume 35 of Oxford Logic Guides. The Clarendon Press, New York, 1997

1997
[9]

Contrini and Y

C. Contrini and Y. Gurevich. Transitive infon logics. Rev. Symb. Log. , 6(2):281–304, 2013

2013
[10]

van Dalen

D. van Dalen. Intuitionistic Logic. In D. Gabbay and F. G uenth- ner, editors, Handbook of Philosophical Logic, volume 3, pages 225–339. Kluwer, Reidel, Dordrecht, 1986. 31

1986
[11]

de Jongh

D. de Jongh. Investigations on the Intuitionistic Propositional Calculus. PhD thesis, University of Wisconsin, 1968. Available at http://www.illc.uva.nl/Research/Publications/Dissertations/HDS-05-Dick-de-Jongh.text.pdf

1968
[12]

de Jongh and A

D. de Jongh and A. Visser. Embeddings of Heyting Algebra s. In Wil- frid Hodges, Martin Hyland, Charles Steinhorn, and John Tru ss, edi- tors, Logic: from foundations to applications, European logic col l. 1993, Oxford Science Publications, pages 187–213. Clarendon Pre ss, Oxf...

1993
[13]

K. Fine. Logics containing K4. II. J. Symbolic Logic , 50(3):619–651, 1985

1985
[14]

Ghilardi

S. Ghilardi. Free heyting algebras as bi-heyting algeb ras. Math. Rep. Acad. Sci. Canada XVI. , 6:240–244, 1992

1992
[15]

Metsniereba

R. Grigolia. Free Algebras of Non-Classical Logics . “Metsniereba”, Tbilisi, 1987. (Russian)

1987
[16]

Hendriks

A. Hendriks. Computations in Propositional Logic . PhD thesis, University of Amsterdam, 1996. Available at http://www.illc.uva.nl/Research/Publications/Dissertations/DS-1996-01.text.ps.gz

1996
[17]

J. Ilin. Filtration revisited: lattices of stable non-classical lo gics. PhD thesis, University of Amsterdam, 2018

2018
[19]

E. Jerabek. A note on the substructural hierarchy. Mathematical Logic Quarterly, 62(1-2):102–110, 2016

2016
[20]

de Jongh and F

D. de Jongh and F. Yang. Jankov’s theorems for intermedi ate logics in the setting of universal models. In N. Bezhanishvili et al., editor, Pro- ceedings of TbiLLC’09: International Conference on Logic, Langua ge and Computation, volume 6618 of LNAI, pages 53–76. Springer-Verlag, 2011

2011
[21]

Nishimura

I. Nishimura. On formulas of one variable in intuitioni stic propositional calculus. Journal of Symbolic Logic , 25:327–331, 1960. 32

1960
[22]

Renardel de Lavalette, A

G.R. Renardel de Lavalette, A. Hendriks, and D. de Jongh . Intuition- istic Implication without Disjunction. J. Log. Comp. , 22(3):375–404, 2012

2012
[23]

L. Rieger. On the lattice theory of Brouwerian proposit ional logic. Acta fac. rerum nat. Univ. Car. , 189:1–40, 1949

1949
[24]

V. V. Rybakov. Admissibility of Logical Inference Rules. Elsevier, 1997

1997
[25]

Shehtman

V.B. Shehtman. Rieger-Nishimura lattices. Soviet Mathematics Dok- lady, 19:1014–1018, 1978

1978
[26]

R. Statman. Intuitionistic propositional logic is pol ynomial-space com- plete. Theor. Comp. Sc. , 9:67–72, 1979

1979
[27]

A. Visser. Evaluation, provably deductive equivalenc e in Heyting’s Arithmetic. Technical Report 4, Dept. of Philosophy, Utrecht Univer- sity, 1985

1985
[28]

Visser, D

A. Visser, D. de Jongh, J. van Benthem, and G. Renardel de Lavalette. NNIL a study in intuitionistic logic. In A. Ponse, M. de Rijke , and Y. Venema, editors, Modal logics and Process Algebra: a bisimulation perspective, pages 289–326, 1995

1995
[29]

F. Yang. Intuitionistic subframe formulas, NNIL-form ulas and n- universal models. Master’s Thesis, MoL-2008-12, ILLC, Uni versity of Amsterdam, 2008

2008
[30]

Zakharyaschev

M. Zakharyaschev. Syntax and semantics of superintuit ionistic logics. Algebra and Logic , 28(4):262–282, 1989. 33

1989

Pith tools

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

[1] [18]

J. Ilin, D. de Jongh, and F. Yang. NNIL axioms have the ﬁni te model property. In J. van Eijck, R. Iemhoﬀ, and J. Joosten, editors, Liber Amicorum Alberti, volume 30 of Tributes, pages 177–185. College pub- lications, 2016

work page 2016

[2] [3]

Bezhanishvili

N. Bezhanishvili. Lattices of Intermediate and Cylindric Modal Logics. PhD thesis, University of Amsterdam, 2006. Available at http://www.illc.uva.nl/Research/Publications/Dissertations/DS-2006-02.text.pdf

work page 2006

[3] [1]

Bellissima

F. Bellissima. Finitely generated free Heyting algebra s. Journal of Symbolic Logic, 51:152–165, 1986

work page 1986

[4] [2]

Bezhanishvili and S

G. Bezhanishvili and S. Ghilardi. An algebraic approach to subframe logics. Intuitionistic case. Ann. Pure Appl. Logic, 147(1-2):84–100, 2007

work page 2007

[5] [4]

Bezhanishvili

N. Bezhanishvili. Frame based formulas for intermediat e logics. Studia Logica, 90:139–159, 2008

work page 2008

[6] [5]

Bezhanishvili, D

N. Bezhanishvili, D. Coumans, S. van Gool, and D. de Jongh . Dual- ity and universal models for the meet-implication fragment of IPC. In M. Aher, D. Hole, E. Jeˇ r´ abek, and C. Kupke, editors,Logic, Language, and Computation: 10th International Tbilisi Symposium on Logi c, Lan- guage, and Computation, TbiLLC 2013, Gudauri, Georgia, Septemb er 23-27, 2013...

work page 2013

[7] [6]

Bezhanishvili and D

N. Bezhanishvili and D. de Jongh. Stable logics in intuit ionistic logic. Notre Dame Journal of Formal Logic , 59(3):307–324, 2018

work page 2018

[8] [7]

Bezhanishvili, D

N. Bezhanishvili, D. de Jongh, A. Tzimoulis, and Z. Zhao. Univer- sal models for the positive fragment of intuitionistic logi c. In Logic, Language, and Computation - 11th International Tbilisi Sympos ium, TbiLLC 2015, Tbilisi, Georgia, September 21-26, 2015, Revised S e- lected Papers, pages 229–250, 2015

work page 2015