Pith. sign in

REVIEW 3 major objections 4 minor 42 references

Modelling socio-political competition

T0 review · 3 major / 4 minor · reviewed 2026-08-14 · deepseek-v4-flash

Pith's one-line read The paper proves that a two-sorted modal logic of promises and demands is sound and complete for many-valued graph-based frames.

desk verdict The paper's new many-valued multi-type logic is a real extension, but the completeness theorem in the appendix is proved for a different frame convention than the body, with no transfer argument, so the main claim is not yet established. read the letter →

arxiv 1908.04817 v1 pith:ONZYUZZS submitted 2019-08-13 math.LO

classification math.LO MSC 03B4503B5003G10
keywords many-valuedmodallogicnon-distributivegraph-basedsemanticsmulti-typesocio-politicalcompetitionconceptlatticeformalanalysisreflexivegraphs
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

This paper tries to put socio-political competition on a logical footing. It introduces a multi-type modal language with two kinds of formulas—social demands, evaluated at political parties, and political promises, evaluated at social groups—connected by heterogeneous modal operators. The intended models are many-valued graph-based frames: reflexive graphs whose graded edges record similarity between groups and between parties, plus affinity relations between the two sides. The main technical claim is that the basic logic $\mathsf{LMT}$ is sound and complete with respect to these frames. A worked example uses an eleven-valued Łukasiewicz chain to calculate how the Duke's demand and the Conservative fox-hunting promise fare across target and non-target groups.

What carries the argument

The central object is the graph-based $A$-frame: a pair of reflexive $A$-graphs (one for social groups, one for political parties) equipped with $A$-valued affinity relations linking the two sides. Each $A$-graph induces a formal $A$-context and hence a concept lattice, and the affinity relations induce completely join-preserving modal operators on the product of the two concept lattices. The completeness proof further relies on many-valued filters, ideals, and complements of ideals to build the canonical frame and to prove the truth lemma.

What would settle it

A reader could settle the convention question by computing, for a finite reflexive $A$-graph with $A$ the two-element Boolean algebra and $Z=\{0,1\}$, the concept lattices produced by the polarity in Definition 3.1 and by the swapped polarity in Appendix A; if the two complex algebras are not isomorphic for some graph, then Theorem A.8 does not cover the frames defined in the body. If they are isomorphic in all finite cases, the missing equivalence would still need an explicit proof.

Watch

Extended reading notes

Core claim

The central discovery is a completeness theorem: the basic multi-type normal $\mathsf{LMT}$-logic—the common core of non-distributive lattice logic with two sorts and two normal modal operators—captures exactly the inferences valid on all many-valued graph-based $A$-frames. In the intended reading, $A$ is the algebra of truth degrees, the two sorts are social demands $\mathsf{SD}$ and political promises $\mathsf{PP}$, and the two arenas are social groups and political parties. Each frame is built from two reflexive $A$-graphs, and the modal operators are interpreted through graded affinity relations satisfying stability conditions. The proof constructs a canonical model from many-valued filters and ideals on the Lindenbaum–Tarski algebra and shows every non-derivable type-uniform sequent fails there. The case study then shows how promises such as "tax money used to enforce fox hunting ban" receive support degrees on each social group and how the modal operators convert group support into party response.

Load-bearing premise

The completeness theorem rests on an unproved interchangeability between the frame convention used in the appendix's canonical model (which swaps the two sides of the formal context) and the convention used to define graph-based frames in Definition 3.1; the appendix itself notes that the complex algebras are different.

Editorial extensions

If this is right

  • Validity checking reduces to graph data: every sequent derivable in $\mathsf{LMT}$ is true in every graph-based $A$-model, so claims about promises, demands, groups, and parties can be checked solely from the graded relations.
  • The framework gives a formal meaning to 'winning on away ground': a party outperforms a rival when its promises score better than the rival's on social groups with low affinity, and symmetrically for demands of groups tested on parties.
  • The logic is parameterized by the truth-value algebra $A$, so the completeness theorem covers Łukasiewicz, Gödel, and Boolean gradings alike; the case study uses an eleven-element Łukasiewicz chain.
  • With fixed-point operators added, expressions such as $\mu X.\blacklozenge\bigstar(X\wedge\pi)$ would describe convergence of the ongoing interaction between social groups and political parties, as the paper notes in its conclusions.
  • The graded similarity relations are reflexive but need not be symmetric or transitive, matching empirical observations of asymmetric similarity from psychology and business, and they are built directly into the semantics.

Reading between the lines

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

  • If the appendix convention is aligned with Definition 3.1, the same canonical-model strategy would likely prove completeness for a range of richer frames with additional compatible relations, because the construction uses only the lattice of many-valued filters and ideals.
  • Beyond the paper, the formal notion of 'winning on away ground' suggests an empirical test: compute the logic's support degrees from party manifestos and group issue sets, then compare which promises score highest on non-core groups against polling data.
  • The permitted asymmetry between the two affinity relations makes 'recognition' measurable: a party may recognize a group's issues more than the group recognizes the party's issues, and the logic tracks the consequences of that asymmetry for which demands get heard.
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.

Referee Report

3 major / 4 minor

Summary. The paper introduces a many-valued, multi-type modal language LMT with two formula types, social demands (SD) and political promises (PP), connected by heterogeneous modal operators diamond and box. The semantics are based on enriched reflexive A-graphs, where A is a complete residuated lattice of truth values, and frame validity is defined via graph-based A-frames and models. The central technical claim is Theorem A.8: the basic multi-type normal LMT-logic is sound and complete with respect to the class of graph-based A-frames. The paper also presents a case study, loosely inspired by British politics, in which the framework is used to model competition among political parties and social groups through promises and demands.

Significance. If Theorem A.8 is correct, the paper extends the single-type many-valued graph-based semantics of [4] to a genuinely multi-type setting for non-distributive modal logic, providing a complete axiomatization for a two-sorted lattice-based modal language. This is a useful contribution to the program of graph-based semantics for non-distributive logics and gives a formal vocabulary for two-sided socio-political competition. The paper is careful in defining the semantic structures and the case study illustrates the intended readings. However, the completeness proof is carried out in an appendix that changes the frame convention relative to the body of the paper, and the auxiliary canonical-model construction contains partially specified or inadmissible states. These issues are load-bearing for the central claim, so the completeness theorem as stated is not yet established, although the gaps appear repairable.

major comments (3)
  1. [Appendix A, opening paragraph; Definitions 2.4 and 3.1] The appendix changes the definition of the associated formal context: Definition 2.4 sets ZA := A × Z and ZX := Z with IE((α,z), z') = E(z,z') → α, while the appendix sets ZA := Z and ZX := A × Z with IE(z,(α,z')) = E(z,z') → α, and explicitly says the complex algebras are different from those of Definition 3.1. Lemma A.4 verifies the compatibility conditions only for this altered convention, and no equivalence or transfer theorem is supplied. Since E is not assumed symmetric and appears asymmetrically in the liftings [0] and [1], the two conventions are not trivially interchangeable. Consequently, Theorem A.8, as stated, does not cover the graph-based A-frames defined in Section 3.
  2. [Lemma A.6] In the proof of inequality (4), the proof introduces a state z' := (f^p, u) where u is the constant map 1 on PP. But states in ZS (Definition A.3) require the second coordinate to lie in CA(PP), the complements of proper A-ideals, which forces u(⊥) = 0. The constant-1 map has u(⊥) = 1 and therefore is not a state of the canonical frame. No replacement witness is given, so this step of the proof is invalid as written.
  3. [Lemma A.4 and Lemma A.6] Several auxiliary states are only partially specified. For example, in Lemma A.4 the state z' in ZA_P is required only to satisfy g_{z'} = f^{-✸}_z; its second coordinate in CA(SD) is not defined, and the compatibility condition ⋀_{σ ∈ SD}(g_{z'}(σ) → v_{z'}(σ)) = 1 is not verified. Similarly, in Lemma A.6 the states (f_⊤, u_⊥), (f_{π∧χ}, u_⊥), and (f_π, u_⊥) are used without proving that the first coordinate is a proper A-filter or that the pair belongs to ZS. These omissions make the canonical-model construction incomplete as written.
minor comments (4)
  1. [Definition 4.1] The valuation is described as a pair of homomorphisms VS : SD → X_P^+ and VP : PP → X_S^+, but the notation V(ϕ) := ([[ϕ]], ([ϕ])) is then used uniformly for both types; the intended type of each component should be stated explicitly to avoid confusion about which side stores the support and refutation maps.
  2. [Section 5] The similarity and recognition functions in the case study are stipulated examples rather than empirical measurements. The paper does note that it is not committing to a specific definition, but a sentence emphasizing the illustrative character at the start of the case study would help readers calibrate the status of the numerical values.
  3. [Appendix A, Lemma A.7] Several cases of the Truth Lemma are dismissed with 'the proof is analogous and omitted'. Given that the appendix is the only place where completeness is established, and given the frame-convention issue, it would be advisable to include at least one fully worked dual case (e.g. the ♦-case) or to provide a clear reduction.
  4. [Abstract and Section 5] The abstract contains raw TeX artifacts such as 'Plo\v{s}\v{c}ica', and the reference [4] is cited as forthcoming; these should be cleaned up and updated in the final version.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: the completeness proof is a direct canonical-model construction; the appendix's swapped frame convention is a correctness gap, not a circular reduction.

full rationale

The central claim, Theorem A.8, is proved by a canonical model construction over the Lindenbaum-Tarski algebra of the logic L. The only non-target input is Proposition 2.2, the soundness and completeness of L with respect to heterogeneous LMT-algebras, which is explicitly said to follow by a routine Lindenbaum-Tarski argument and does not assume the relational frame completeness being proved. The uses of that algebraic completeness in Lemma A.1 (e.g., to show that ✸π ⊢ ⊥ iff π ⊢ ⊥, and to prove the join-irreducibility of ⊤) are standard algebraic consequences, not the target result. The many self-citations ([4], [5], [6], [10]) supply background definitions and the general algebraic setting, but the completeness proof itself does not reduce to any of them: the cited results are invoked as lemmas about algebras, not as the relational completeness theorem. I find no step in which a prediction or first-principles result is equivalent by construction to its own inputs. One non-circular caveat should be flagged: Appendix A explicitly says it works with frames whose associated complex algebras are different from those of Definition 3.1, because it swaps ZA and ZX in the associated formal context, and no equivalence or transfer proof is supplied. This means Theorem A.8, as written, may not cover the graph-based frames defined in the body of the paper; that is a correctness/completeness gap, not a circularity.

Assumptions & free parameters 3 free parameters · 4 assumptions · 1 invented entities

The theoretical core rests on standard algebraic machinery from formal concept analysis and on a specified class of residuated lattices. The case study introduces many hand-picked numbers. The most consequential unstated assumption is the equivalence of the two frame conventions used in the completeness proof.

free parameters (3)
  • Case-study similarity relations ES and EP = Handpicked values in the diagram in Section 5
    These graded similarities between social groups and between political parties are chosen to make the example work, not fitted to real data.
  • Case-study recognition functions f_F, f_D, f_B, f_L, f_C, f_X = Tables in Section 5
    These functions encode how parties and groups recognize each other's issues; they are assigned arbitrarily for the illustration.
  • Case-study support tables for formulas pi_L, pi_C, pi_X, sigma_F, sigma_D, sigma_B = Tables in Section 5
    The truth values of the formulas in the example are stipulated by hand; no data source or error bars are provided.
assumptions (4)
  • domain assumption The truth-value algebra A is a complete, frame-distributive and dually frame-distributive, commutative, associative residuated lattice.
    Section 2.2: the proof of Lemma A.1.1 uses frame-distributivity, so the completeness result is limited to this class of algebras.
  • standard math The standard theory of formal A-concepts and A-Galois connections, including Lemma 2.3 from [6], guarantees that enriched formal A-contexts yield complete normal lattice expansions.
    This cited background is used to show that the complex algebra of a graph-based frame is a heterogeneous LMT-algebra.
  • ad hoc to paper The appendix's altered frame convention, where ZA := Z and ZX := A*Z instead of the reverse, preserves the intended semantics of Definition 3.1.
    Implicit in the proof of Theorem A.8; the appendix states the complex algebras are different from Definition 3.1 but no equivalence proof is given.
  • ad hoc to paper The case-study relations and valuations are stipulated examples, not measurements.
    Section 5 provides no data source or statistical fit; the numbers are illustrative and do not support empirical claims.
invented entities (1)
  • Two-type language LMT with social demands (SD) and political promises (PP) connected by heterogeneous modal operators diamond and box
    purpose: To model two simultaneous arenas of competition: parties testing demands and social groups testing promises
    This is a syntactic and semantic construct, not an empirical entity; it has no falsifiable consequences outside the model.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Modelling socio-political competition." pith.science (2026). https://pith.science/paper/ONZYUZZS

@misc{pith2026190804817,
  author       = {Pith},
  title        = {Pith review of: Modelling socio-political competition},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/ONZYUZZS}},
  note         = {Machine review of arXiv:1908.04817}
}
read the original abstract

This paper continues the investigation of the logic of competing theories, be they scientific, social, political etc. We introduce a many-valued, multi-type modal language which we endow with relational semantics based on enriched reflexive graphs, inspired by Plo\v{s}\v{c}ica's representation of general lattices. We axiomatize the resulting many-valued, non-distributive modal logic of these structures and prove a completeness theorem. We illustrate the application of this logic through a case study in which we model competition among interacting political promises and social demands within an arena of political parties social groups.

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

42 extracted references · 39 canonical work pages

  1. [4]

    Conradie, A

    W . Conradie, A. Craig, A. Palmigiano, and N. Wijnberg. Mo delling competing theories. In Proc. EUSFLAT 2019, Atlantis Studies in Uncertainty Modelling, page forthcom ing, 2019

  2. [7]

    Conradie, S

    W . Conradie, S. Frittella, A. Palmigiano, M. Piazzai, A. Tzimoulis, and N.M. Wijnberg. Categories: How I Learned to Stop Worrying and Love Two Sorts. In Proc. W oLLIC 2016, volume 9803 of LNCS, pages 145–164, 2016

  3. [1]

    Bˆ elohl´ avek

    R. Bˆ elohl´ avek. Fuzzy galois connections.Mathematical Logic Quarterly, 45(4):497–504, 1999

  4. [2]

    Heterogeneous algeb ras

    Garrett Birkhoff and John D Lipson. Heterogeneous algeb ras. Journal of Combinatorial Theory, 8(1):115– 133, 1970

  5. [3]

    Conradie and A

    W . Conradie and A. Craig. Relational semantics via TiRS g raphs. Proc. TACL 2015, page long abstract, 2015

  6. [5]

    Conradie, A

    W . Conradie, A. Craig, A. Palmigiano, and N.M Wijnberg. M odelling informational entropy. In Proc. W oLLIC 2019, volume 11541 of Lecture Notes in Computer Science , pages 140–160. Springer, 2019

  7. [6]

    Rough concepts

    W . Conradie, S. Frittella, K. Manoorkar, S. Nazari, A. Pa lmigiano, A. Tzimoulis, and N.M. Wijnberg. Rough concepts. Submitted, ArXiv preprint: arXiv:1907.00359, 2019

  8. [8]

    Conradie, S

    W . Conradie, S. Frittella, A. Palmigiano, M. Piazzai, A. Tzimoulis, and N.M. Wijnberg. Toward an epistemic-logical theory of categorization. In Proc. TARK 2017, volume 251 of EPTCS, pages 167–186, 2017. 13

Show all 42 references
  1. [9]

    Conradie and A

    W . Conradie and A. Palmigiano. Constructive canonicity of inductive inequalities. arXiv preprint arXiv:1603.08341, 2016

  2. [10]

    Conradie and A

    W . Conradie and A. Palmigiano. Algorithmic correspond ence and canonicity for non-distributive logics. Annals of Pure and Applied Logic , 170(9):923–974. DOI: 10.1016/j.apal.2019.04.003, 2019

  3. [11]

    Conradie, A

    W . Conradie, A. Palmigiano, and A. Tzimoulis. Goldblat t-Thomason for LE-logics. arXiv preprint arXiv:1809.08225, 2018

  4. [12]

    Constructive canonicity for lattice-based fixed point logics

    Willem Conradie, Andrew Craig, Alessandra Palmigiano , and Zhiguang Zhao. Constructive canonicity for lattice-based fixed point logics. In Proc. W oLLIC 2017, volume 10388 of Lecture Notes in Computer Science, pages 92–109. Springer, 2017. ArXiv preprint arXiv:1603. 06547

  5. [13]

    Craig, M

    A. Craig, M. Gouveia, and M. Haviar. TiRS graphs and TiRS frames: a new setting for duals of canonical extensions. Algebra universalis, 74(1-2):123–138, 2015

  6. [14]

    Craig, M

    A. Craig, M. Haviar, and H. Priestley. A fresh perspecti ve on canonical extensions for bounded lattices. Applied Categorical Structures, 21(6):725–749, 2013

  7. [15]

    Hannan et al

    M.T. Hannan et al. Concepts and Categories: F oundations for Sociological and Cultural Analysis . Columbia University Press, 2019

  8. [16]

    Ganter and R

    B. Ganter and R. Wille. F ormal concept analysis: mathematical foundations. Springer, 2012

  9. [17]

    Political spaces, dimensionality decline and party competition

    C´ esar Garc´ ıa-D´ ıaz, Gilmar Zambrana-Cruz, and Arjen V an Witteloostuijn. Political spaces, dimensionality decline and party competition. Advances in Complex Systems , 16(06):1350019, 2013

  10. [18]

    Greco, P

    G. Greco, P . Jipsen, F. Liang, A. Palmigiano, and A. Tzim oulis. Algebraic proof theory for LE-logics. arXiv preprint arXiv:1808.04642 , 2018

  11. [19]

    Greco, P

    G. Greco, P . Jipsen, K. Manoorkar, A. Palmigiano, and A. Tzimoulis. Logics for rough concept analysis. In Proc. ICLA 2019, volume 11600 of LNCS, pages 144–159, 2019

  12. [20]

    Kuijken, G

    B. Kuijken, G. Gemser, and N. M. Wijnberg. Categorizati on and willingness to pay for new products: The role of category cues as value anchors. Journal of Product Innovation Management, 34(6):757–771, 2017

  13. [21]

    Lowery, A

    D. Lowery, A. van Witteloostuijn, G. Peli, H. Brasher, S . Otjes, and S. Gherghina. Policy agendas and births and deaths of political parties. Party Politics, 19(3):381–407, 2013

  14. [22]

    R. M. Nosofsky. Stimulus bias, asymmetric similarity, and classification. Cognitive Psychology, 23(1):94– 140, 1991

  15. [23]

    Z. Pawlak. Rough set theory and its applications to data analysis. Cybernetics & Systems, 29(7):661–688, 1998

  16. [24]

    A. Tversky. Features of similarity. Psychological review, 84(4):327, 1977

  17. [25]

    van de Wardt and A

    M. van de Wardt and A. van Witteloostuijn. Adapt or peris h? how parties adapt to party system saturation in western democracies, 1945-2016. British Journal of Political Science , page forthcoming, 2019

  18. [26]

    N. M. Wijnberg. Classification systems and selection sy stems: The risks of radical innovation and category spanning. Scandinavian Journal of Management , 27(3):297–306, 2011. A Completeness For the sake of uniformity with previous settings (cf. e.g. [ 6, Section 7.2]) in this ...

  19. [27]

    If g : LS → A is an A-filter , then so is g −♦

  20. [28]

    If f : PP → A is a proper A-filter , then so is f −✸

  21. [29]

    If g : SD → A is a proper A-filter , then so is g −♦

  22. [30]

    If π 1,π 2 ∈ PP, then π 1 ∨ π 2 = ⊤ implies that π 1 = ⊤ or π 2 = ⊤

  23. [31]

    If σ 1,σ 2 ∈ SD, then σ 1 ∨ σ 2 = ⊤ implies that σ 1 = ⊤ or σ 2 = ⊤. Proof. 1. For all s,t ∈ LS, f −✸(⊤) = ⋁ { f (p) | ✸p ≤ ⊤} = ⋁ { f (p) | p ∈ L} = f (⊤) = 1 f −✸(s) ∧ f −✸(t) = ⋁ { f (p1) | ✸p1 ≤ s} ∧⋁ { f (p2) | ✸p2 ≤ t} = ⋁ { f (p1) ∧ f (p2) | ✸p1 ≤ s and ✸p2 ≤ b} frame-d...

  24. [32]

    f −✸(⊥) = ⋁ { f ([π ]) | [✸π ] ≤ [⊥]} =⋁ { f ([π ]) | ✸π ⊢ ⊥} =⋁ { f ([π ]) | π ⊢ ⊥} = f ([⊥]) = 0

    Let f : PP → A be a proper A-filter. f −✸(⊥) = ⋁ { f ([π ]) | [✸π ] ≤ [⊥]} =⋁ { f ([π ]) | ✸π ⊢ ⊥} =⋁ { f ([π ]) | π ⊢ ⊥} = f ([⊥]) = 0. The crucial inequality is the third to last, which holds si nce ✸π ⊢ ⊥ iff π ⊢ ⊥. The right to left implication can be easily derived in L. F...

  25. [33]

    Suppose, by contraposition, that ⊤ ⁄⊢π 1 and ⊤ ⁄⊢π 2. By the completeness theorem to which we have ap- pealed in the proof of item 2, there are heterogeneous algebr as H1 = (LS 1,LP 1 ,♦1,✸1) and H2 = (LS 2,LP 2 ,♦2,✸2) and corresponding assignments vi on Hi such that v1( π 1)...

  26. [34]

    finite join-preservation) of♦′ follow immediately by construction

    The monotonicity of ✸′ and normality (i.e. finite join-preservation) of♦′ follow immediately by construction. The normality (i.e. fin ite join-preservation) of ✸′ is verified by cases: if a ∨ b ⁄= ⊤′, then it immediately follows from the normality of ✸H1×H2. If a ∨ b = ⊤′, then b...

  27. [35]

    ⋀ s∈LS ( f −✸(s) → v(s)) =⋀ p∈LP( f (p) → v(✸p))

  28. [36]

    ⋀ p∈LP(g−♦(p) → u(p)) =⋀ s∈LS (g(s) → u(♦s)). Proof. 1. The fact that f (p) ≤ f −✸(✸p) implies that f −✸(✸p) → v(✸p) ≤ f (p) → v(✸p) for every p ∈ LP, which is enough to show that ⋀ s∈LS ( f −✸(s) → v(s)) ≤⋀ p∈LP( f (p) → v(✸p)). Conversely, to show that ⋀ p∈LP ( f (p) → v(✸p)...

  29. [37]

    V S(p) = ([ [p] ]S,( [p] )S) with [ [p] ]S : ZP A → A and ( [p] )S : ZP X → A defined by z ↦→gz(p) and ( α ,z) ↦→vz(p) → α , respectively

  30. [38]

    18 Lemma A.6

    V P(p) = ([ [p] ]P,( [p] )P) with [ [p] ]P : ZS A → A and ( [p] )P : ZS X → A defined by z ↦→fz(p) and (α ,z) ↦→uz(p) → α , respectively. 18 Lemma A.6. The structure G of Definition A.5 is a graph-based A-model. Proof. It is enough to show that for any p ∈ Prop,

  31. [39]

    [ [p] ][1] P = ( [p] )P and [ [p] ]P = ( [p] )[0] P

  32. [40]

    To show that ( [p] )P(α ,z) ≤ [ [p] ][1] P (α ,z) for any (α ,z) ∈ ZS X , by definition, we need to show that uz(p) → α ≤ ⋀ z′∈ZS A ([ [p] ]P(z′) → (ES(z′,z) → α )), i.e

    [ [p] ][1] S = ( [p] )S and [ [p] ]S = ( [p] )[0] S , and We only show 1. To show that ( [p] )P(α ,z) ≤ [ [p] ][1] P (α ,z) for any (α ,z) ∈ ZS X , by definition, we need to show that uz(p) → α ≤ ⋀ z′∈ZS A ([ [p] ]P(z′) → (ES(z′,z) → α )), i.e. that for every z′ ∈ ZS A, uz(p) →...

  33. [41]

    the maps [ [π ] ]P : ZS A → A and ( [π ] )P : ZS X → A coincide with those defined by the assignments z ↦→fz(π ) and (α ,z) ↦→uz(π ) → α , respectively

  34. [42]

    the maps [ [σ ] ]S : ZP A → A and ( [σ ] )S : ZP X → A coincide with those defined by the assignments z ↦→gz(σ ) and (α ,z) ↦→vz(σ ) → α , respectively. Proof. We proceed by simultaneous induction on π and σ . If π := p ∈ Prop (resp. σ := p ∈ Prop), the statement follows immedi...

Pith tools

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