Delft University of Technology
Modelling competing theories
Conradie, Willem; Craig, Andrew; Palmigiano, Alessandra; Wijnberg, Nachoem DOI
10.2991/eusflat-19.2019.100 Publication date
2020
Document Version Final published version Published in
Proceedings of the 11th Conference of the European Society for Fuzzy Logic and Technology, EUSFLAT 2019
Citation (APA)
Conradie, W., Craig, A., Palmigiano, A., & Wijnberg, N. (2020). Modelling competing theories. In V. Novak, V. Marik, M. Stepnicka, M. Navara, & P. Hurtik (Eds.), Proceedings of the 11th Conference of the European Society for Fuzzy Logic and Technology, EUSFLAT 2019 (pp. 721-739). (Proceedings of the 11th
Conference of the European Society for Fuzzy Logic and Technology, EUSFLAT 2019). Atlantis Press. https://doi.org/10.2991/eusflat-19.2019.100
Important note
To cite this publication, please use the final published version (if applicable). Please check the document version above.
Copyright
Other than for strictly personal use, it is not permitted to download, forward or distribute the text or part of it, without the consent of the author(s) and/or copyright holder(s), unless the work is under an open content license such as Creative Commons. Takedown policy
Please contact us and provide details if you believe this document breaches copyrights. We will remove access to the work immediately and investigate your claim.
See discussions, stats, and author profiles for this publication at: https://www.researchgate.net/publication/335811521
Modelling competing theories
Conference Paper · January 2019 DOI: 10.2991/eusflat-19.2019.100 CITATIONS 0 READS 7 4 authors:
Some of the authors of this publication are also working on these related projects:
The logics of categories, concepts, theories, and informational entropy View project
Strategic design View project Willem Conradie University of Johannesburg 45PUBLICATIONS 520CITATIONS SEE PROFILE Andrew Craig University of Johannesburg 16PUBLICATIONS 122CITATIONS SEE PROFILE Alessandra Palmigiano
Vrije Universiteit Amsterdam 86PUBLICATIONS 904CITATIONS SEE PROFILE Nachoem M. Wijnberg University of Amsterdam 109PUBLICATIONS 1,338CITATIONS SEE PROFILE
Modelling competing theories
Willem Conradieaand Andrew Craigband Alessandra Palmigianob,cand Nachoem Wijnbergd,e
aSchool of Mathematics, University of the Witwatersrand
bDepartment of Mathematics and Applied Mathematics, University of Johannesburg,
cFaculty of Technology, Policy and Management, Delft University of Technology
dCollege of Business and Economics, University of Johannesburg
eAmsterdam Business School, University of Amsterdam
Abstract
We introduce a complete many-valued seman-tics for two normal lattice-based modal logics. This semantics is based on reflexive many-valued graphs. We discuss an interpretation and possi-ble applications of this logical framework in the context of the formal analysis of the interaction between (competing) scientific theories.
Keywords: Non distributive modal logic,
Graph-based semantics, Competing theories.
1
Introduction
The contributions of this paper lie at the intersection of sev-eral strands of research. They are rooted in the gensev-eral- general-ized Sahlqvist theory for normal LE-logics [9, 8], i.e. those logics algebraically captured by varieties of normal lattice expansions (LEs) [16]. Via canonical extensions and dis-crete duality, basic normal LE-logics of arbitrary signa-tures and a large class of their axiomatic extensions can be uniformly endowed with complete relational semantics
of different kinds, of which those of interest to the present
paper are relational structures based on formal contexts [15, 13, 6, 7, 17] and reflexive graphs [3, 4]. In a math-ematical setting in which the original discrete duality for perfect normal LEs has been relaxed to a discrete adjunc-tion for complete normal LEs, these semantic structures have yielded uniform theoretical developments in the al-gebraic proof theory [17] and in the model theory [11] of LE-logics, and also insights on possible interpretations of LE-logics which have generated new opportunities for ap-plications. In particular, via polarity-based semantics, in [6], the basic non-distributive modal logic and some of its axiomatic extensions are interpreted as epistemic logics of categories and concepts, and in [7], the corresponding ‘common knowledge’-type construction is used to give an epistemic-logical formalization of the notion of prototype of a category; in [5, 18], polarity-based semantics for non-distributive modal logic is proposed as an encompassing
framework for the integration of rough set theory [20] and formal concept analysis [14], and in this context, the ba-sic non-distributive modal logic is interpreted as the logic of rough concepts; via graph-based semantics, in [4], the same logic is interpreted as the logic of informational en-tropy, i.e. an inherent boundary to knowability due e.g. to perceptual, theoretical, evidential or linguistic limits. In the graphs (Z, E) on which the relational structures are based, the relation E is interpreted as the indiscernibility rela-tion induced by informarela-tional entropy, much in the same style as Pawlak’s approximation spaces in rough set theory.
However, the key difference is that, rather than generating
modal operators which associate any subset of Z with its definable E-approximations, E generates a complete
lat-tice (i.e. the latlat-tice of Ec-concepts). In this approach,
con-cepts are not definable approximations of predicates, but rather they represent ‘all there is to know’, i.e. the theoreti-cal horizon to knowability, given the inherent boundary
en-coded into E (in their turn, Ec-concepts are approximated
by means of the additional relations of the graph-based re-lational structures from which the semantic modal opera-tors arise). Interestingly, E is required to be reflexive but in general neither transitive nor symmetric, which is in line with proposals in rough set theory [22, 23, 21] that indis-cernibility does not need to give rise to equivalence rela-tions.
In this paper, we start exploring the many-valued version of the graph-based semantics of [4] for two axiomatic ex-tensions of the basic normal non-distributive modal logic, and in particular their potential for modelling situations in which informational entropy derives from the theoretical frameworks under which empirical studies are conducted.
2
Preliminaries
This section is based on [4, Section 2.1] and [5, Section 7.2].
11th Conference of the European Society for Fuzzy Logic and Technology (EUSFLAT 2019) Atlantis Studies in Uncertainty Modelling, volume 1
2.1 Basic normal nondistributive modal logic
Let Prop be a (countable or finite) set of atomic proposi-tions. The language L of the basic normal nondistributive
modal logicis defined as follows:
ϕ := ⊥ | > | p | ϕ ∧ ϕ | ϕ ∨ ϕ | ϕ | ^ϕ,
where p ∈ Prop. The basic, or minimal normal L-logic is a set L of sequents ϕ ` ψ with ϕ, ψ ∈ L, containing the following axioms:
p ` p, ⊥ ` p, p ` >, p ` p ∨ q, q ` p ∨ q, p ∧ q ` p,
p ∧ q ` q, > `>, p ∧ q ` (p ∧ q), ^⊥ ` ⊥, ^p ∨ ^q ` ^(p ∨ q)
and closed under the following inference rules:
ϕ ` χ χ ` ψ ϕ ` ψ ϕ ` ψ ϕ(χ/p) ` ψ(χ/p) χ ` ϕ χ ` ψ χ ` ϕ ∧ ψ ϕ ` χ ψ ` χ ϕ ∨ ψ ` χ ϕ ` ψ ϕ ` ψ ϕ ` ψ ^ϕ ` ^ψ
An L-logic is any extension of L with L-axioms ϕ ` ψ. Relevant to what follows are the axiomatic extensions of L
generated by⊥ ` ⊥ and > ` ^>, and by ϕ ` ϕ and ϕ `
^ϕ. Let L0(resp. L1) be the axiomatic extension obtained
by adding⊥ ` ⊥ (resp. p ` p) to L. Notice that L1is an
extension of L0.
2.2 Many-valued enriched formal contexts
Throughout this paper, we let A= (D,1,0,∨,∧,⊗,→)
de-note an arbitrary but fixed complete frame-distributive and dually frame-distributive, commutative and associa-tive residuated lattice (understood as the algebra of
truth-values) such that 1 → α= α for every α ∈ D. For every set
W, an A-valued subset (or A-subset) of W is a map u : W →
A. We let AWdenote the set of all A-subsets. Clearly, AW
inherits the algebraic structure of A by defining the opera-tions and the order pointwise. The A-subsethood relation
between elements of AW is the map S
W : AW× AW → A
defined as SW( f , g) := Vz∈W( f (z) → g(z)). For every α ∈ A,
let {α/w} : W → A be defined by v 7→ α if v= w and v 7→ ⊥A
if v , w. Then, for every f ∈ AW,
f=_
w∈W
{ f (w)/w}. (1)
When u, v : W → A and u ≤ v w.r.t. the pointwise order, we write u ⊆ v. An A-valued relation (or A-relation) is a map
R: U × W → A. Two-valued relations can be regarded as
A-relations. In particular for any set Z, we let∆Z: Z × Z → A
be defined by∆Z(z, z0)= > if z = z0and∆Z(z, z0)= ⊥ if z ,
z0. An A-relation R : Z × Z → A is reflexive if∆Z⊆ R. Any
A-valued relation R : U × W → A induces maps R(0)[−] :
AW→ AU and R(1)[−] : AU→ AW defined as follows: for
every f : U → A and every u : W → A,
R(1)[ f ] : W → A
x 7→V
a∈U( f (a) → R(a, x))
R(0)[u] : U → A
a 7→V
x∈W(u(x) → R(a, x))
A formal A-context1or A-polarity (cf. [1]) is a structure
P = (A, X, I) such that A and X are sets and I : A × X → A.
Any formal A-context induces maps (·)↑: AA→ AX and
(·)↓: AX→ AAgiven by (·)↑= I(1)[·] and (·)↓= I(0)[·]. These
maps are such that, for every f ∈ AAand every u ∈ AX,
SA( f , u↓)= SX(u, f↑),
that is, the pair of maps (·)↑and (·)↓form an A-Galois
con-nection. In [1, Lemma 5], it is shown that every A-Galois connection arises from some formal A-context. A formal
A-concept of P is a pair ( f, u) ∈ AA× AXsuch that f↑= u
and u↓= f . It follows immediately from this definition that
if ( f , u) is a formal A-concept, then f↑↓= f and u↓↑= u,
that is, f and u are stable. The set of formal A-concepts can be partially ordered as follows:
( f , u) ≤ (g, v) iff f ⊆ g iff v ⊆ u.
Ordered in this way, the set of the formal A-concepts of P
is a complete lattice, which we denote P+.
An enriched formal A-context (cf. [5, Section 7.2]) is a
structure F = (P, R,R^) such that P = (A, X, I) is a
for-mal A-context and R: A × X → A and R^ : X × A → A
are I-compatible, i.e. R(0) [{α/x}], R(1) [{α/a}], R(0)
^ [{α/a}]
and R(1)
^[{α/x}] are stable for every α ∈ A, a ∈ A and x ∈
X. The complex algebra of an enriched formal A-context
F = (P, R,R^) is the algebra F+= (P+,[R], hR^i) where
[R], hR^i : P+→ P+ are defined by the following
assign-ments: for every c= ([[c]],([c])) ∈ P+,
[R]c = (R(0) [([c])], (R (0) [([c])])↑) hR^ic = ((R(0) ^ [[[c]]]) ↓,R(0) ^[[[c]]]). Lemma 2.1. (cf. [5, Lemma 15]) If F = (X, R,R^) is an
enriched formal A-context, F+= (X+,[R], hR^i) is a
com-plete normal lattice expansion such that[R] is completely
meet-preserving and hR^i is completely join-preserving.
1 In the crisp setting, a formal context [14], or polarity, is a
structure P = (A, X, I) such that A and X are sets, and I ⊆ A × X is a binary relation. Every such P induces maps (·)↑: P(A) → P(X) and (·)↓: P(X) → P(A), respectively defined by the assignments B↑:= I(1)[B] and Y↓:= I(0)[Y]. A formal concept of P is a pair c= ([[c]],([c])) such that [[c]] ⊆ A, ([c]) ⊆ X, and [[c]]↑= ([c]) and ([c])↓= [[c]]. The set L(P) of the formal concepts of P can be partially ordered as follows: for any c, d ∈ L(P),
c ≤ d iff [[c]] ⊆ [[d]] iff ([d]) ⊆ ([c]).
With this order, L(P) is a complete lattice, the concept lattice P+ of P. Any complete lattice L is isomorphic to the concept lattice P+of some polarity P.
3
Many-valued graph-based frames
A reflexive A-graph is a structure X = (Z, E) such that Z is a nonempty set, and E : Z × Z → A is reflexive. From now on, we will assume that all A-graphs we consider are reflexive even when we drop the adjective.
Definition 3.1. For any reflexive A-graph X = (Z, E), the formal A-context associated with X is
PX:= (ZA,ZX, IE),
where ZA:= A × Z and ZX:= Z, and IE: ZA× ZX→ A is
defined by IE((α, z), z0)= E(z,z0) → α. We let X+:= PX+.
Any R : Z × Z → A admits the following liftings:
IR: ZA× ZX→ A
((α, z), z0) 7→ R(z, z0) → α
JR: ZX× ZA→ A
(z, (α, z0)) 7→ R(z, z0) → α
Recall that for all f : A × Z → A, and u : Z → A, the maps2
f↑: Z → A and u↓: A × Z → A are respectively defined by
the assignments z 7→ ^ (α,z0)∈Z A [ f (α, z0) → (E(z0,z) → α)] (α, z) 7→ ^ z0∈Z X [u(z0) → (E(z, z0) → α)].
Definition 3.2. A graph-based A-frame is a structure G =
(X, R^,R) where X = (Z, E) is a reflexive A-graph, and R^
and Rare binary A-relations on Z such that the structure
FG:= (PX, IR, JR^) is an enriched formal A-context. That
is, R^and Rsatisfy the following E-compatibility
condi-tions: for any z ∈ Z and α, β ∈ A,
(R[0] [{β/z}])[10]⊆ R[0] [{β/z}] (R[1] [{β/(α, z)}])[01]⊆ R[1] [{β/(α, z)}] (R[1] ^ [{β/z}]) [10]⊆ R[1] ^ [{β/z}] (R[0] ^ [{β/(α, z)}]) [01]⊆ R[0] ^ [{β/(α, z)}].
where for all f: A × Z → A and u : Z → A,
u[0]= E[0][u] : A × Z → A
(α, z) 7→ IE(0)[u](α, z)= u↓(α, z)
f[1]= E[1][ f ] : Z → A
z 7→ I(1)E [ f ](z)= f↑(z)
2
Applying this notation to a graph X = (Z, E), we will abbrevi-ate E[0][u] and E[1][ f ] as u[0]and f[1], respectively, for each u, f as above, and write u[01] and f[10] for (u[0])[1]and ( f[1])[0], re-spectively. Then u[0]= I(0)E [u]= u↓and f[1]= IE(1)[ f ]= f↑, where the maps (·)↓and (·)↑are those associated with the polarity PX.
R[0] [u] : A × Z → A (α, z) 7→ I(0)R [u](α, z) R[1] [ f ] : Z → A z 7→ IR(1) [ f ](z) R[0] ^[ f ] : Z → A z 7→ JR(0) ^[ f ](z) R[1]^[u] : A × Z → A (α, z) 7→ J(1)R ^[u](α, z).
Hence, for any z ∈ Z and α ∈ A,
E[0][u](α, z) := V z0∈Z X[u(z 0) → (E(z, z0) → α)] E[1][ f ](z) := V(α,z0)∈Z A[ f (α, z 0) → (E(z0,z) → α)]. R[0] [u](α, z) := Vz0∈Z X[u(z 0) → (R (z, z0) → α)] R[1] [ f ](z) := V(α,z0)∈Z A[ f (α, z 0) → (R (z0,z) → α)] R[0] ^ [ f ](z) := V(α,z0)∈ZA[ f (α, z 0) → (R ^(z, z 0) → α)] R[1] ^ [u](α, z) := Vz0∈ZX[u(z 0) → (R ^(z 0,z) → α)].
The complex algebra of a graph-based A-frame G =
(X, R^,R) is the algebra G+ = (X+,[R], hR^i), where
X+ := PX+, and[R] and hR^i are unary operations on
X+defined as follows: for every c= ([[c]],([c])) ∈ X+,
[R]c = (R[0] [([c])], (R[0] [([c])])[1])
hR^ic = ((R[0]
^ [[[c]]])
[0],R[0]
^ [[[c]]]).
By definition, it immediately follows that
Lemma 3.3. If G is a graph-based A-frame, G+= FG+.
Hence, by the lemma above and Lemma 2.1,
Lemma 3.4. If G = (X, R,R^) is a graph-based A-frame,
G+= (X+,[R], hR^i) is a complete normal lattice
expan-sion such that[R] is completely meet-preserving and hR^i
is completely join-preserving.
The following lemma is an immediate consequence of [5,
Lemma 14] applied to FG.
Lemma 3.5. For every graph-based A-graph G =
(X, R,R^),
1. the following are equivalent:
(i) (R[0] [{α/z}])[10]⊆ R[0] [{α/z}] for every z ∈ Z and
α ∈ A;
(ii) (R[0] [u])[10]⊆ R[0] [u] for every u : ZX→ A;
(iii) R[1] [ f[10]] ⊆ R[1] [ f ] for every f : ZA→ A.
2. the following are equivalent:
(i) (R[1] [{α/(β, z)}])[01] ⊆ R[1] [{α/(β, z)}] for every
z ∈ Z and α, β ∈ A;
(iii) R[0] [u[01]] ⊆ R[0] [u] for every u : ZX→ A.
3. the following are equivalent:
(i) (R[0]^ [{α/(β, z)}])[01] ⊆ R[0] ^[{α/(β, z)}] for every z ∈ Z and α, β ∈ A; (ii) (R[0]^ [ f ])[01]⊆ R[0] ^[ f ] for every f : ZA→ A; (iii) R[1] ^ [u [01]] ⊆ R[1]
^[u] for every u : ZX→ A.
4. the following are equivalent :
(i) (R[1]
^ [{α/z}])
[10]⊆ R[1]
^[{α/z}] for every z ∈ Z and
α ∈ A;
(ii) (R[1]
^ [u])
[10]⊆ R[1]
^[u] for every u : ZX→ A;
(iii) R[0]
^ [ f
[10]] ⊆ R[0]
^[ f ] for every f : ZA→ A.
4
Many-valued graph-based models
Let L be the language of Section 2.1.
Definition 4.1. A graph-based A-model of L is a tuple M =
(G, V) such that G = (X, R,R^) is a graph-based A-frame
and V: L → G+is a homomorphism. For every ϕ ∈ L, let
V(ϕ) := ([[ϕ]],([ϕ])), where [[ϕ]] : ZA→ A and ([ϕ]) : ZX→ A
are s.t.[[ϕ]][1]= ([ϕ]) and ([ϕ])[0]= [[ϕ]]. Hence:
V(p) = ([[p]],([p])) V(>) = (1AZA,(1AZA)[1]) V(⊥) = ((1AZX)[0],1AZX) V(ϕ ∧ ψ) = ([[ϕ]] ∧ [[ψ]],([[ϕ]] ∧ [[ψ]])[1]) V(ϕ ∨ ψ) = ((([ϕ]) ∧ ([ψ]))[0],([ϕ]) ∧ ([ψ])) V(ϕ) = (R[0] [([ϕ])], (R[0] [([ϕ])])[1]) V(^ϕ) = ((R[0]^ [[[ϕ]]])[0],R[0] ^ [[[ϕ]]]).
Valuations induce α-support relations between value-state
pairs and formulas for each α ∈ A (in symbols: M, (β, z) α
ϕ), and α-refutation relations between states of models and
formulas for each α ∈ A (in symbols: M, z αϕ) such that
for every ϕ ∈ L, all z ∈ Zand all β ∈ A,
M, (β, z) αϕ iff α ≤ [[ϕ]](β,z),
M, z αϕ iff α ≤ ([ϕ])(z).
This can be equivalently expressed as follows:
M, (β, z) αp iff α ≤ [[p]](β,z);
M, (β, z) α> iff α ≤ 1AZA(β, z) i.e. always; M, (β, z) α⊥ iff α ≤ (1AZX)[0](β, z) = Vz0∈Z X[1 AZX (z0) → (E(z, z0) → β)] = Vz0∈Z X[E(z, z 0) → β] = β; M, (β, z) αϕ ∧ ψ iff M, (β, z) αϕ and M,(β,z) αψ; M, (β, z) αϕ ∨ ψ iff α ≤ (([ϕ]) ∧ ([ψ]))[0](β, z) = Vz0∈Z X[(([ϕ]) ∧ ([ψ]))(z 0) → (E(z, z0) → β)]; M, (β, z) αϕ iff α ≤ (R[0] [([ϕ])])(β, z) = Vz0∈Z X[([ϕ])(z 0) → (R (z, z0) →β)]; M, (β, z) α^ϕ iff α ≤ ((R[0]^[[[ϕ]]])[0])(β, z) = Vz0∈Z X[R [0] ^[[[ϕ]]](z 0) → (E(z, z0) →β)]; M, z αp iff α ≤ ([p])(z);
M, z α⊥ iff α ≤ 1AZX(z) i.e. always; M, z α> iff α ≤ (1AZA)[1](z) = V(β,z0)∈Z A[1(β, z 0) → (E(z0,z) → β)] = V(β,z0)∈Z A[E(z 0,z) → β] = β; M, z αϕ ∨ ψ iff M, z αϕ and M,z αψ; M, z αϕ ∧ ψ iff α ≤ ([[ϕ]] ∧ [[ψ]])[1](z) = V(β,z0)∈Z A[([[ϕ]] ∧ [[ψ]])(β, z 0) → (E(z0,z) → β)]; M, z α^ϕ iff α ≤ (R[0]^[[[ϕ]]])(z) = V(β,z0)∈Z A[[[ϕ]](β, z 0) → (R^(z, z0) → β)]; M, z αϕ iff α ≤ ((R[0] [([ϕ])])[1])(z) = V(β,z0)∈Z A[R [0] [([ϕ])](β, z0) → (E(z0,z) → β)].
Definition 4.2. A sequent ϕ ` ψ is true in a model M = (G, V) (notation: M |= ϕ ` ψ) if [[ϕ]] ⊆ [[ψ]], or equivalently,
if([ψ]) ⊆ ([ϕ]). A sequent ϕ ` ψ is valid on a graph-based
frame G (notation: G |= ϕ ` ψ) if ϕ ` ψ is true in every model M = (G, V) based on G.
Remark 4.3. It is not difficult to see that for all stable
val-uations, if p ∈ Prop and β, β0∈ A such that β ≤ β0, then
[[p]](β, z) ≤ [[p]](β0,z) for every z ∈ Z, and one can readily
verify that this condition extends compositionally to every ϕ ∈ L.
Before moving on to the case study, let us expand on how to understand informally the notion of α-support at value-state pairs. To this end, it is perhaps useful to start
analysing M, (β, z) α⊥. By definition, this is the case iff
α ≤ β. Hence, the role of β in the pair (β,z) is to indicate the maximum extent α to which the ‘state’ (β, z) is allowed to α-support a false statement. Equivalently, (β, z) does not α-support the falsehood for any α β. Hence, when A is linearly ordered, β indicates the ‘threshold’ beyond which (i.e. overcoming which by going up) α-support becomes meaningful at the given ‘state’ (β, z). These observations open the way to the possibility of imposing extra conditions on the extension functions [[ϕ]] : A × Z → A, depending on
the given situation to be modelled. These extra conditions are not required by the general semantic environment, but are accommodated by it. For instance, if considering this threshold β is not relevant to the given case at hand, then one can choose to restrict oneself to valuations such that,
if p ∈ Prop, then [[p]](β, z)= [[p]](β0,z) for every z ∈ Z and
every β, β0∈ A. One can readily verify that this condition
extends compositionally to every ϕ ∈ L.
5
Case study: competing theories
In the previous sections, we have illustrated how many-valued semantics for modal logic [12, 2] can be general-ized from Kripke frames to graph-based structures. This generalization is the parametric version (where A is the pa-rameter) of the graph-based semantics of [4], and the main motivation for introducing it is that it allows for a rich de-scription of certain essentials (in the present case, of the role of theories in the practice of empirical sciences), while still using basic intuitions from the crisp setting. For in-stance, in the many-valued setting, the basic intuition still holds that the generalization from classical Kripke frame semantics to graph-based semantics consists in thinking of the graph-relation E as encoding an inherent boundary to knowability (referred to as informational entropy) which disappears in the classical setting (in which E coincides with the identity relation). Informational entropy can be due to many factors (e.g. technological, theoretical, lin-guistic, perceptual, cognitive), and in [4], examples are dis-cussed in which the nature of these limits is perceptual and linguistic. In the present section, we discuss how the
theo-retical frameworksadopted by empirical scientists can be a
source of informational entropy.
For the purpose of this analysis, we consider graph-based
structures (Z, E, {RXi | Xi⊆ Var,0 ≤ i ≤ n}) in which X =
(Z, E) represents a network of databases, and Var is a set of variables which includes the variables structuring the in-formation contained in the databases of Z. In this context, L-formulas can be thought of as hypotheses which will be assigned truth values (more specifically, truth-degrees) at value-state pairs of models based on these frames. We will refer to any such pair (β, z) as a situation, the β component of which is understood as the maximum degree of flexi-bility in operationalizing variables in that given situation. This truth value assignment of a formula (hypothesis) at a value-state pair (situation) is then intended to represent the significance of the correlation posited by the hypothesis, when tested in the given database according to the degree of flexibility allowed at that situation, with higher truth
val-ues indicating higher levels of significance.3This
interpre-tation is coherent with the property mentioned in Remark
3However, in this paper we do not intend to set up a
system-atic correlation between significance levels and truth values. The values chosen in the example below are only supposed to be intu-itively plausible.
4.3: indeed, the higher the flexibility in operationalizing variables, the more leeway to obtain a higher α-support of hypotheses at situations.
Moreover, in the context of the graph-based structures above, an empirical theory is characterized by (and here identified with) a certain subset X of variables which are
relevantto the given theory; also, in what follows, for all
databases zj∈ Z, we let Xjdenote the set of variables
struc-turing the data contained in zj.4 Hence, the A-relation E
encodes to what extent database z2is similar to z1(e.g. by
letting E(z1,z2) record the percentage of variables of z1
that also occur in z2), while the relations RX encode to
what extent one database is similar to another, relative to
X(e.g. by letting RX(z1,z2) record the percentage of
vari-ables of X1∩ X that also occur in X2). Below, we give a
more concrete illustration of this environment by means of an example about dietary theories.
The first theory, known since antiquity, is that body-fat loss of individuals depends on what they ate and how much ex-ercise they did. We refer to it as the ancient theory (A), on the basis of which Aretaeus the Cappadocian might have
created a database zA recording how many kochliaria of
olive oil and of honey, how many minas of bread, of olives, of lamb, and how many kyathoi of wine a group of ath-letes and a group of rhetoric students ate each day, and how many stadia they walked or ran each day, and how many
minaseach individual weighed each day.
The second one, the modern theory (M), was developed
in Victorian times by Wilbur Olin Atwater.5 In line with
the Taylorist view on labour efficiency, the modern theory
explains body-fat loss in terms of a negative balance be-tween the daily caloric intake of individuals provided by food and their daily caloric expenditure, due e.g. to main-taining body temperature or to exercise. The modern the-ory improves over the ancient in that it provides a common ground of commensurability, which was absent in the an-cient theory, between the variables relative to food intake and those relative to exercise, by reducing all of them to their energetic import, measured in calories. Hence, an
imaginary database zM built by Atwater on the basis of
this theory would record how many calories individuals got from food and how many calories they spent per day, and their mass in kilograms measured each day.
The third theory, referred to as the hormonal response
the-ory(H),6postulates that body-fat loss is governed by a
hor-mone, insulin, which is released in response to the intake
4It is interesting to notice that this basic environment naturally
captures the idea that evidence is laden with theory: that is, we can think of each database zjas being constructed on the basis of
the theory corresponding to set of variables Xjassociated with zj. 5Source: https://www.sciencehistory.org/
distillations/magazine/counting-calories
6Source: https://idmprogram.com/
of certain macronutrients: namely, it is maximally released in response to intake of carbohydrates, less so but still sig-nificantly released in response to protein intake, while fat
intake does not trigger any significant insulin response.7
This theory posits that as long as insulin values are high, the body cannot access its own fat and use it as energy source, no matter how severe the caloric restriction. An imaginary
database zHbuilt by Banting and Best (who famously
dis-covered insulin and its function) on the basis of this theory would record how many calories from carbohydrates, how many calories from proteins, how many calories from fat individuals got from food, how many calories they spent per day, and their mass in kilograms measured each day. This scenario can be modelled as the graph-based A-frame
(Z, E, RA,RM,RH), where A is the 11-element Łukasiewicz
chain, Z := {zA,zM,zH}, and E : Z × Z → A is as indicated
in the following diagram:
zA zM zH 1 1 0.2 0.4 1 1 1 0.6 1
For any arrow in the diagram above, its value (i.e. the sim-ilarity degree of the target to the source) intuitively rep-resents to which extent the target database provides infor-mation about variables relevant to the theory according to which the source database has been built. This simility relation is reflexive by definition. Moreover, all ar-rows have non-zero values because the three databases
con-structed on the basis of the three different theories have
a minimal common ground, namely they all include the weight of individuals (which, as we will see, is the depen-dent variable in the hypotheses tested on them). We assign
value 1 to all the arrows which have zM as source or zAas
target, since the information relevant to the modern theory can be fully retrieved from all databases, and the informa-tion relevant to the modern and hormonal response theories
can be fully retrieved from the variables in zA. The arrow
from zAto zM is assigned the lowest non-zero value, since
from the information about the caloric intake and
expendi-ture contained in zMone cannot retrieve the actual types of
food the individuals ingested or the exercise they did.
For X ∈ {A, M, H}, and for any z, z0∈ Z, the value of the RX
-arrow from z to z0represents the similarity degree of z0to
z relative to X. A concrete way to picture this is the fol-lowing: assume that a scientist adopting theory X is asked
7Proviso: for the purpose of keeping this example simple, we
are oversimplifying the hormonal response theory.
to which extent s/he would swap database z for database
z0. If the scientist in question is Aretaeus, and he is asked
e.g. to give up zHfor zM, he would not be very happy, for
although zH is not particularly good for his purposes and
requires a substantial guesswork from him, he would be
even worse off with zM, and he would suffer the same loss
of information captured by the value E(zH,zM). This
jus-tifies letting RA(zH,zM) := E(zH,zM)= 0.4. However,
Are-taeus would certainly be willing to swap zM for zH, since
whatever little he can do with zM can be certainly done
with zH, and in fact possibly more. Hence we let again
RA(zM,zH) := E(zM,zH)= 1, and so on. Hence, RA:= E.
If the scientist in question is Atwater, and he was asked to
give up zAfor zH, he would be fine with it, because both
databases provide all the information relevant to the theo-retical framework he has adopted. In fact, he would be fine with swapping any database for any other database: that is,
the relation RM: Z × Z → A maps every tuple of databases
to 1. An analogous reasoning justifies the following
defini-tion for the reladefini-tion RH: Z × Z → A:
zA zM zH 1 1 0.3 0.5 1 1 1 0.9 1
where RH and E only differ in the value of the arrow
from zA to zH. The relations above are E-compatible
(cf. Definition 3.2), and E-reflexive (i.e. E ⊆ R for any R ∈
{RA,RM,RH}, see [4] Definition 6) hence (Z, E, RA,RM,RH)
is a graph-based A-frame for a multi-modal language with
modalities A,M,H and ^A,^M,^H, in which the
ax-iomsiϕ ` ϕ and ϕ ` ^iϕ are valid for every i ∈ {A, M, H}
(cf. Proposition A.1).8
Let the formula ϕ be the hypothesis stating that individuals who restrict their daily caloric intake to less than 20 calo-ries per kilogram of body mass will lose weight over time. This hypothesis is phrased in terms of the variables rele-vant to the modern theory, and hence it can be tested on
all databasesin Z. Let us assume that the results of the
tests of ϕ do not vary from one situation to another situa-tion with the same degree of flexibility β, and it turns out that, though 80% of the individuals restricting their daily caloric intake to less than 20 calories per kilogram of body mass indeed lost a bit of weight, generally not too much,
8Notice that, although the setting of [4] is crisp, the
corre-spondence results in [4] Proposition 4 remain verbatim the same when passing to the many-valued setting. This is a phenomenon already observed in the correspondence theory for many-valued logics [19].
10% of individuals remained at the same weight, and 10% even gained weight. Let us assume that in the statistical
model this results in moderate effect size, but a p-value of
0.1, which is considered to yield too low a level of signif-icance to reject the null-hypothesis (that caloric restriction has no effect). So we propose, for the sake of this example,
to assign [[ϕ]] : ZA→ A according to the following table9:
β zA zM zH 0.0 0.5 0.5 0.5 0.1 0.6 0.6 0.6 0.2 0.7 0.7 0.7 0.3 0.8 0.8 0.8 0.4 0.9 0.9 0.9 0.5 1.0 1.0 1.0 0.6 1.0 1.0 1.0 0.7 1.0 1.0 1.0 0.8 1.0 1.0 1.0 0.9 1.0 1.0 1.0 1.0 1.0 1.0 1.0
Let the formula ψ be the hypothesis stating that individ-uals who restrict their daily caloric intake to less than 20 calories per kilogram of body mass and who let at least 80% of their caloric intake come from fat will lose more weight than individuals on the same daily caloric regime but getting less than 80% of their calories from fat. This hypothesis is phrased in terms of the variables relevant to the hormonal response theory, and hence it can certainly be
tested on zAand zH. We wish to make a case that, modulo
some guesswork that of course will make the results less
reliable, the hypothesis ψ can be tested on zM as well. For
instance, if the database zM built by Atwater was based on
a group of individuals living in Connecticut in the years 1890-1895, and for some fortuitous circumstances an inde-pendent database exists about their eating habits (e.g. the list of customers of the local grocer’s and their weekly or-ders, and by chance these customers also include the
peo-ple in zM), then it would be possible to make some
esti-mates about which individuals in the sample of zM let at
least 80% of their daily caloric intake come from fat. This is of course an easy way out in our fictitious example, but it reflects a very common situation in the practice of em-pirical research, that databases do not perfectly match the hypotheses that scientists wish to test on them, and that some guesswork is needed to a greater or lesser extent. Notice that the imperfect match between the observations in databases and variables in hypotheses is independent from the (maximum) degree of flexibility in operationalis-ing variables (formally encoded in the value β of the pairs which we refer to as ‘situations’). Specifically, the degree of flexibility in operationalising any variables is an a priori parameter that we fix for each ‘situation’, independently of the hypotheses tested in the given situation. In contrast, the
9It can be checked that this valuation is stable.
discussion in the paragraph above is relative to the test of a specific hypothesis on a database, and hence depends in-herently on the given hypothesis. Furthermore, once such a suitable translation is found, its suitability will not de-pend on how the target variable is operationalised in each situation, but will depend only on the match between the theory according to which the database has been built and the theory to which the hypothesis pertains.
Let us imagine that ψ is confirmed for 95% of the individ-uals in the samples of all databases. Let us assume that
in the statistical model this results in a high effect size for
coefficient of the (dummy) variable recording whether the
high-fat diet was followed or not and a p-value of 0.01, which corresponds to a level of significance generally con-sidered to be high enough to reject the null-hypothesis (that the type of macronutrients from which restricted caloric
in-take proceeds has no effect on weight loss). In short, the
results in respect to this hypothesis seem very strong and
credible. So we propose, for β= 0, to assign a truth-value
of 0.8 to ψ at zAand zH, and a truth-value of 0.4 to ψ at zM,
a strong discount due to the guesswork needed to
accom-modate the testing of ψ on zM.10 The following table gives
the complete specification of [[ψ]]:
β zA zM zH 0.0 0.8 0.4 0.8 0.1 0.9 0.5 0.9 0.2 1.0 0.6 1.0 0.3 1.0 0.7 1.0 0.4 1.0 0.8 1.0 0.5 1.0 0.9 1.0 0.6 1.0 1.0 1.0 0.7 1.0 1.0 1.0 0.8 1.0 1.0 1.0 0.9 1.0 1.0 1.0 1.0 1.0 1.0 1.0
We are now in a position to compute the extensions ofMϕ,
Hϕ, Mψ and Hψ.11 Intuitively,Xχ can be understood
as what becomes of hypothesis χ when ‘seen through the
lenses’ of theory X.12
It can be verified that:
10For higher values of β, these values increase accordingly. It
can be checked that the valuation as specified in the table, is sta-ble.
11Since R
A:= E, the modal operators Aand ^Acoincide with
the identity on X+.
12These modal operators can be used to reason about
“compar-ative studies” which span across all databases and establish the degree of similarity between each databases and the focal one.
[[Mψ]] = β zA zM zH 0.0 0.4 0.4 0.4 0.1 0.5 0.5 0.5 0.2 0.6 0.6 0.6 0.3 0.7 0.7 0.7 0.4 0.8 0.8 0.8 0.5 0.9 0.9 0.9 0.6 1.0 1.0 1.0 0.7 1.0 1.0 1.0 0.8 1.0 1.0 1.0 0.9 1.0 1.0 1.0 1.0 1.0 1.0 1.0 ≤ β zA zM zH 0.0 0.5 0.5 0.5 0.1 0.6 0.6 0.6 0.2 0.7 0.7 0.7 0.3 0.8 0.8 0.8 0.4 0.9 0.9 0.9 0.5 1.0 1.0 1.0 0.6 1.0 1.0 1.0 0.7 1.0 1.0 1.0 0.8 1.0 1.0 1.0 0.9 1.0 1.0 1.0 1.0 1.0 1.0 1.0 = [[ϕ]] and [[Mψ]] = β zA zM zH 0.0 0.4 0.4 0.4 0.1 0.5 0.5 0.5 0.2 0.6 0.6 0.6 0.3 0.7 0.7 0.7 0.4 0.8 0.8 0.8 0.5 0.9 0.9 0.9 0.6 1.0 1.0 1.0 0.7 1.0 1.0 1.0 0.8 1.0 1.0 1.0 0.9 1.0 1.0 1.0 1.0 1.0 1.0 1.0 ≤ β zA zM zH 0.0 0.8 0.4 0.8 0.1 0.9 0.5 0.9 0.2 1.0 0.6 1.0 0.3 1.0 0.7 1.0 0.4 1.0 0.8 1.0 0.5 1.0 0.9 1.0 0.6 1.0 1.0 1.0 0.7 1.0 1.0 1.0 0.8 1.0 1.0 1.0 0.9 1.0 1.0 1.0 1.0 1.0 1.0 1.0 = [[ψ]]
It can also be checked that [[Hϕ]] = [[ϕ]], [[Hψ]] = [[ψ]]
and [[Mϕ]] = [[ϕ]].
These identities and inequalities can be interpreted as fol-lows: each theory leaves unchanged the hypotheses for-mulated in terms of its own variables, or proper subsets thereof; however, if a hypothesis formulated according to a more expressive theory is ‘seen through the lenses’ of a less
expressive theory (this is the case ofMψ), it is expected to
score worse. Finally, ϕ and ψ are prima facie incomparable. But is it really so?
6
Epilogue
Although very stylised and simplified, the scenario above illuminates a number of interesting notions and their inter-relations. First, we have identified each theory with the set of its relevant variables. This move naturally provides a connection with a strand of research we have been recently
developing, based on the idea that lattice-based modal log-ics can be interpreted as the loglog-ics of categories or formal concepts [6, 7, 5]. This connection can be articulated in general terms by modelling theories as categories, exten-sionally captured by sets of hypotheses, and intenexten-sionally captured by their relevant variables.
Having identified theories with sets of variables has al-lowed us to associate states of the models (understood as databases) with theories, thereby giving a very simple and concrete representation of the otherwise abstract idea that ‘observations are laden’, and that this
theory-ladenneslays at the core of the informational entropy that
this paper sets out to studying. In the toy example of the previous section, states (databases) bijectively correspond to theories, but this does not need to be the case in general. Related to this, we have captured a local and a global way in which similarity ensues from theory-driven infor-mational entropy. Specifically, the relation E captures the
localperspective, in which a given database z0is similar to
a database z to the extent to which z0is amenable to test
hypotheses formulated using the variables of the theory
as-sociated with z, that is, to the extent to which z0is suitable
to answer questions pertaining to ‘the theory of z’, while
the relations RXcapture the global perspective; i.e., RX
en-codes information on how similar any one database is to another in respect to their relative performances in testing hypotheses formulated using variables of X.
These formal tools can be used to illuminate a very com-mon situation in the practice of empirical research, namely that databases do not perfectly match the hypotheses that scientists wish to test on them, and that a key underlying aspect in empirical research concerns precisely how to ad-dress this imperfect match. In this paper, we have laid the groundwork for addressing this issue with bespoke logi-cal tools, by means of the modal operators interpreted
us-ing the relations RX, which, as discussed above, translate
hypotheses from the ‘language’ (variables) of one theory to the ‘language’ (variables) of another, and what is lost in translation depends on the relationship between the two theories.
Finally, we can try and discuss whether the formalization above throws light on the following two questions: what does it mean for theories to compete? And how do we as-sess whether one theory has outcompeted the other? We propose the following view: theories can compete,
most obviously when hypotheses that belong to different
theories (as ϕ and ψ in our example belong to M and H respectively) predict the same dependent variable (weight loss in our example). The most direct way in which two theories (e.g. M and H) can compete is when their respec-tive hypotheses (ϕ and ψ) are tested on each member of a set of databases. Each of these databases will be more or less suitable to test a given hypothesis. In particular, any
hypothesis is expected to get its best scores13if tested either on databases which are constructed in accordance with the theory in the variables of which the hypothesis is formu-lated, or on databases that are maximally similar to those. We refer to all these databases as being ‘home-ground’ to that given hypothesis. For instance, in the case study of the previous section, every database is ‘home-ground’ to
ϕ, while only zA and zH are ‘home-ground’ to ψ. When
a hypothesis is tested on a database that is not its ‘home-ground’, it will typically find no or less adequate values for its variables. The solution, as in our example of
test-ing ψ on the database zM, is to look for proxies that
rep-resent to some extent the missing variable (or recover the values of the missing variables by some motivated guess-work). These proxies are often second-best or worse, mak-ing the results of the test less credible, even if they lead to accepting the hypotheses. This results in assigning the hypothesis a lower truth value at the database where
prox-ies/guesswork were needed to test the hypothesis.
How-ever, precisely due to the disadvantage of not being on ‘home-ground’, if a hypothesis pertaining to theory X is tested on a database z which is not ‘home-ground’ to it and gets more than half as good results as the competing hypothesis, pertaining to theory Y, to which z is ‘home-ground’, this should be considered an impressive victory of
theory X and its hypothesis, just as is the effect of the rule
that goals scored by soccer teams (in e.g. the Champions League) in away matches count double.
Applying this view to the case of ϕ and ψ, we can hence argue that ψ outcompetes ϕ, since, as discussed above,
ev-ery database is ‘home-ground’ to ϕ, while only zAand zH
are ‘home-ground’ to ψ, and moreover, ψ scores systemat-ically better than ϕ on each database that is ‘home-ground’
to both and, even when β= 0, the lower score of ψ on zM
(0.4) is very close to the score of ϕ on zM(0.5).
7
Conclusions
In this paper, we have introduced a complete many-valued semantic environment for (multi) modal languages based on the logic of general (i.e. not necessarily distributive) lat-tices, and, by means of a toy example, we have illustrated its potential as a tool for the formal analysis of situations arising in the theory and practice of empirical science. As this is only a preliminary exploration, many questions arise, both technical and conceptual, of which here we list a few.
A range of protocols for comparing theories. As
dis-cussed in Sections 5 and 6 hypotheses that look prima facie incomparable can become comparable through the lenses
13We do not mean ‘best scores’ in absolute terms, but in relative
terms: that is, a bad hypothesis will score low on every database, but it will still get its higher scores on databases that are max-imally compatible with the theory in the language of which the hypothesis is formulated.
of the modal operators. In this paper we do not insist on a specific protocol to establish a winner among competing theories. However, we wish to highlight that the framework introduced can accommodate a wide range of possible pro-tocols, including those involving common-knowledge-type constructions.
More expressive languages. We conjecture that the
proof of completeness of the logic of Section 2.1 given in Appendix B can be extended modularly to more expressive languages that display essentially “many valued” features in analogy with those considered in [2]. This is current work in progress.
Sahlqvist theory for many-valued non-distributive
log-ics. A natural direction of research is to develop the
gen-eralized Sahlqvist theory for the logics of graph-based A-frames, by extending the results of [19] on Sahlqvist theory for many-valued logics on a distributive base.
Towards an analysis theory dynamics. We have shown
that using the many-valued environment allows us to dis-cuss competition between theories in an intuitively appeal-ing and formally sound manner. This lays the basis for a host of further developments to model the dynamics of the-ories and databases, to better understand what distance be-tween theories means, as well as studying the hierarchical relations between theories, in analogy with the hierarchical structure of categories.
Socio-political theories and scientific theories. The
present semantic environment naturally lends itself not only to the analysis of competition of scientific theories but also to the analysis of a wide spectrum of phenomena in which theories, broadly construed, play a key role. For instance, building on the present work, in [10], a formal environment is introduced in which the similarities can be analysed between the competition among political theories (both in their institutional incarnations as political parties, and in their social incarnations as social blocks or groups) and the competition between scientific theories.
Acknowledgement
The authors would like to thank Apostolos Tzimoulis for insightful discussions and for his substantial contributions to the proof of the completeness theorem.
References
[1] R. Bˆelohl´avek, Fuzzy galois connections, Mathemat-ical Logic Quarterly 45 (4) (1999) 497–504.
[2] F. Bou, F. Esteva, L. Godo, R. O. Rodr´ıguez, On the minimum many-valued modal logic over a finite residuated lattice, Journal of Logic and Computation 21 (5) (2011) 739–790.
[3] W. Conradie, A. Craig, Relational semantics via TiRS graphs, TACL 2015.
[4] W. Conradie, A. Craig, A. Palmigiano, N. Wijnberg, Modelling informational entropy, in: Proc. WoLLIC 2019, Vol. 11541 of LNCS, 2019, pp. 140–160. [5] W. Conradie, S. Frittella, K. Manoorkar, S. Nazari,
A. Palmigiano, A. Tzimoulis, N. Wijnberg, Rough concepts, Submitted.
[6] W. Conradie, S. Frittella, A. Palmigiano, M. Piaz-zai, A. Tzimoulis, N. Wijnberg, Categories: How I Learned to Stop Worrying and Love Two Sorts, in: Proc. WoLLIC 2016, Vol. 9803 of LNCS, 2016, pp. 145–164.
[7] W. Conradie, S. Frittella, A. Palmigiano, M. Piaz-zai, A. Tzimoulis, N. Wijnberg, Toward an epistemic-logical theory of categorization, in: Proc. TARK 2017, Vol. 251 of EPTCS, 2017, pp. 167–186. [8] W. Conradie, A. Palmigiano, Constructive
canon-icity of inductive inequalities, arXiv preprint
arXiv:1603.08341.
[9] W. Conradie, A. Palmigiano, Algorithmic correspon-dence and canonicity for non-distributive logics, An-nals of Pure and Applied Logic 170(9) (2019) 923– 974.
[10] W. Conradie, A. Palmigiano, C. Robinson, A. Tzi-moulis, N. Wijnberg, Modelling socio-political com-petition, Submitted.
[11] W. Conradie, A. Palmigiano, A. Tzimoulis,
Goldblatt-Thomason for LE-logics, arXiv preprint arXiv:1809.08225.
[12] M. Fitting, Many-valued modal logics, Fundam. In-form. 15 (3-4) (1991) 235–254.
[13] N. Galatos, P. Jipsen, Residuated frames with appli-cations to decidability, Transactions of the American Mathematical Society 365 (3) (2013) 1219–1249. [14] B. Ganter, R. Wille, Formal concept analysis:
mathe-matical foundations, Springer, 2012.
[15] M. Gehrke, Generalized Kripke frames, Studia Log-ica 84 (2) (2006) 241–275.
[16] M. Gehrke, J. Harding, Bounded lattice expansions, Journal of Algebra 238 (1) (2001) 345–371.
[17] G. Greco, P. Jipsen, F. Liang, A. Palmigiano, A. Tz-imoulis, Algebraic proof theory for LE-logics, arXiv preprint arXiv:1808.04642.
[18] G. Greco, P. Jipsen, K. Manoorkar, A. Palmigiano, A. Tzimoulis, Logics for rough concept analysis, in: Proc. ICLA 2019, Vol. 11600 of LNCS, 2019, pp. 144–159.
[19] C. le Roux, Correspondence theory in many-valued modal logics, Master’s thesis, University of Johannes-burg, South Africa (2016).
[20] Z. Pawlak, Rough set theory and its applications to data analysis, Cybernetics & Systems 29 (7) (1998) 661–688.
[21] D. Vakarelov, A modal characterization of indiscerni-bility and similarity relations in Pawlak’s information systems, in: International Workshop on Rough Sets, Fuzzy Sets, Data Mining, and Granular-Soft Comput-ing, Springer, 2005, pp. 12–22.
[22] U. Wybraniec-Skardowska, On a generalization of approximation space, Bulletin of the Polish Academy of Sciences. Mathematics 37 (1-6) (1989) 51–62. [23] Y. Yao, T. Y. Lin, Generalization of rough sets using
modal logics, Intelligent Automation & Soft Comput-ing 2 (2) (1996) 103–119.
A
Correspondence results
In what follows, for every graph-based L-frame G, we
let R: Z × Z → A be defined by the assignment (z, z0) 7→
R^(z0,z).
Proposition A.1. The following are equivalent for every graph-based L-frame G:
1. G |= ⊥ ` ⊥ iff for any (β, z) ∈ ZA,
^ z0∈Z X [R(z, z0) → β] ≤ ^ z0∈Z X [E(z, z0) → β].
2. G |= > ` ^> iff for any z ∈ ZX,
^ (α,z0)∈Z A [R^(z, z0) → α] ≤ ^ (α,z0)∈Z A [E(z0,z) → α]. 3. G |= p ` p iff E ⊆ R. 4. G |= p ` ^p iff E ⊆ R. Proof. 1. ⊥ ≤ ⊥ iff R[0] [([⊥])] ≤ [[⊥]] iff R[0] [1AZX] ≤ (1AZX)[0] iff R[0] [1AZX](β, z) ≤ (1AZX)[0](β, z) ∀(β, z) ∈ ZA iff Vz0∈Z X[1(z 0) → (R (z, z0) → β)] ≤V z0∈Z X[1(z 0) → (E(z, z0) → β)] ∀(β, z) ∈ Z A iff Vz0∈Z X[R(z, z 0) → β] ≤V z0∈Z X[E(z, z 0) → β] for any (β, z) ∈ Z A.
2. > ≤ ^> iff R[0] ^ [[[>]]] ≤ ([>]) iff R[0] ^ [1 AZA] ≤ (1AZA)[1] iff R[0] ^ [1 AZA](z) ≤ (1AZA)[0](z) for any z ∈ Z X iff V(α,z0)∈Z A[1(α, z 0) → (R ^(z, z 0) → α)] ≤V (α,z0)0∈Z A[1(α, z 0) → (E(z0,z) → α)] ∀z ∈ Z X iff V(α,z0)∈Z A[R^(z, z 0) → α] ≤V (α,z0)∈Z A[E(z 0,z) → α] for any z ∈ Z X. 3. ∀p[p ≤ p] iff ∀m[m ≤ m] (ALBA [9]) iff ∀α∀z[R[0] [{α/z}[01]] ≤ {α/z}[0]] (m := {α/z}) iff ∀α∀z[R[0] [{α/z}] ≤ {α/z}[0]] (Lemma 3.5) iff ∀α,β∀z,w[α → (R(w, z) → β) ≤α → (E(w,z) → β) (∗) iff E ⊆ R. (∗∗)
To justify the equivalence to (∗) we note that
R[0] [{α/z}](β, w) = Vz0∈Z X[{α/z}(z 0) → (R (w, z0) → β)] = α → (R(w, z) → β), and moreover {α/z}[0](β, w)= V z0∈Z X({α/z}(z 0) → (E(w, z0) → β))= α → (E(w,z) → β).
For the equivalence to (∗∗), note that instantiating α := 1
and β := R(w, z) in (∗) yields 1 ≤ E(w, z) → R(w, z)
which, by residuation, is equivalent to (∗∗). The converse direction is immediate by the monotonicity of → in the second coordinate and its antitonicity in the first coordinate. 4. p ≤ ^p iff ∀j[j ≤ ^j] iff ∀α,β∀z[R[0] ^[{α/(β, z)} [01]] ≤ {α/(β, z)}[1]] iff ∀α,β∀z[R[0] ^[{α/(β, z)}] ≤ {α/(β, z)} [1]] iff ∀α,β∀z,w[α → (R^(w, z) → β) ≤α → (E(z,w) → β) (∗) iff E ⊆ R. (∗∗)
As to the equivalence to (∗), note that R[0]
^ [{α/(β, z)}](w)= V (γ,z0)∈Z A[{α/(β, z)}(γ, z 0) → (R ^(w, z 0) → γ)] = α → (R^(w, z) → β), and that {α/(β,z)}[1](w) = V (γ,z0)∈Z A({α/(β, z)}(γ, z 0) → (E(z0,w) → γ)) = α →
(E(z, w) → β). For the equivalence to (∗∗) note that
instantiating α := 1 and β := R^(w, z) = R(z, w) in (∗)
yields 1 ≤ E(z, w) → R(z, w) which, by residuation, is
equivalent to (∗∗). The converse direction is immediate by the monotonicity of → in the second coordinate and its
antitonicity in the first coordinate.
Remark A.2. Clearly, E-reflexivity (i.e. condition E ⊆ R
in Proposition A.1.3) implies the inequality in Proposi-tion A.1.1; however, this inequality is also verified under
weaker but practically relevant assumptions. For instance, if A is a finite chain, the inequality in Proposition A.1.1 is
equivalent tomin{R(z, z0) → β | z0∈ ZX} ≤ min{E(z, z0) →
β | z0∈ Z
X}= E(z,z) → β = 1 → β = β. Hence, this
condi-tion is equivalent to the condicondi-tion that for every β ∈ A and
z ∈ Z, some z0∈ Z exists such that R(z, z0) → β ≤ β. This
condition is satisfied if for every z ∈ Z some z0∈ Z exists
such that R(z, z0)= 1. Similar considerations apply to the
remaining items of the proposition above.
B
Completeness
This section is an adaptation and expansion of the com-pleteness result of [10, Appendix B], of which Apostolos Tzimoulis and Claudette Robinson are prime contributors.
We will use the validity of⊥ ` ⊥ in the proof of the
case in Lemma B.7. As discussed in Section 5, this axiom is valid in the model of our case study.
For the sake of uniformity with previous settings (cf. e.g. [5, Section 7.2]) in this section, we work with
graph-based frames G = (X, R,R^) the associated
com-plex algebras of which are order-dual to the one in Def-inition 3.2. That is, for the sake of this section, we
de-fine the enriched formal context PG:= (ZA,ZX, IE, IR, JR^)
by setting ZA := Z, ZX := A × Z and IE : ZA× ZX → A
and IR: ZA× ZX→ A and JR^: ZX× ZA→ A be defined
by the assignments (z, (α, z0)) 7→ E(z, z0) → α, (z, (α, z0)) 7→
R(z, z0) → α and ((α, z), z0) 7→ R^(z, z
0) → α, respectively.
For any lattice L, an A-filter is an A-subset of L, i.e. a map
f: L → A, which is both ∧- and >-preserving, i.e. f (>) = 1
and f (a ∧ b)= f (a) ∧ f (b) for any a,b ∈ L. Intuitively,
the ∧-preservation encodes a many-valued version of clo-sure under ∧ of filters. An A-filter is proper if it is also
⊥-preserving, i.e. f (⊥)= 0. Dually, an A-ideal is a map
i: L → A which is both ∨- and ⊥-reversing, i.e. i(⊥) = >
and i(a ∨ b)= i(a) ∧ i(b) for any a,b ∈ L, and is proper if
in addition i(>)= 0. The complement of a (proper) A-ideal
is a map u : L → A which is both ∨- and ⊥-preserving,
i.e. u(⊥)= 0 and u(a∨b) = u(a)∨u(b) for any a,b ∈ L (and
in addition u(>)= 1). Intuitively, u(a) encodes the extent
to which a does not belong to the ideal of which u is the
many-valued complement. We let FA(L), IA(L) and CA(L)
respectively denote the set of proper filters, proper A-ideals, and the complements of proper A-ideals of L. For any L-algebra (L, , ^), and any A-subset k : L → A, let
k−^: L → A be defined as k−^(a)= W{k(b) | ^b ≤ a} and
let k−: L → A be defined as k−(a)= V{k(b) | a ≤ b}. By
definition one can see that k(a) ≤ k−^(^a) and k−(a) ≤
k(a) for every a ∈ L. Let Fm (resp. Fm0, Fm1) be the
Lindenbaum-Tarski algebra of the basic L-logic L (resp.
L0, L1). Moreover, in what follows we write Fm∗for the
Lindenbaum-Tarski algebra of an arbitrary (not necessarily
proper) extension L∗of L. In the remainder of this section,
we abuse notation and identify formulas with their
Lemma B.1.
1. If f : L → A is an A-filter, then so is f−^.
2. If f : Fm∗→ A is a proper A-filter, then so is f−^.
3. If u: L → A is the complement of an A-ideal, then so
is u−.
4. If u: Fm∗→ A is the complement of a proper A-ideal,
then so is u−.
5. If ϕ, ψ ∈ Fm∗, then ϕ ∨ ψ= > implies that ϕ = > or
ψ = >.
6. If ϕ, ψ ∈ Fm∗, then ϕ 0 ⊥ and ψ 0 ⊥ imply that ϕ ∧ ψ 0
⊥.
Proof. 1. For all a, b ∈ L,
f−^(>) = W{ f (b) | ^b ≤ >} = W{ f (b) | b ∈ L} = f(>) = 1 f−^(a) ∧ f−^(b) = W{ f (c1) | ^c1≤ a} ∧W{ f (c2) | ^c2≤ b} = W{ f (c1) ∧ f (c2) | ^c1≤ a and ^c2≤ b} (?) = W{ f (c1∧ c2) | ^c1≤ a and ^c2≤ b} (]) = W{ f (c) | ^c ≤ a and ^c ≤ b} (∗) = W{ f (c) | ^c ≤ a ∧ b} = f−^(a ∧ b),
the equivalence marked with (?) being due to frame dis-tributivity, the one marked with (]) to the fact that f is and A-filter, and the one marked with (∗) to the fact that
^(c1∧ c2) ≤ ^c1∧ ^c2.
2. In general, f−^ need not be a proper filter, even if f
is. However, let us show that this is the case when f is
a proper filter of Fm. Indeed, in this algebra, f−^(⊥)=
W{ f ([ϕ]) | [^ϕ] ≤ [⊥]} = W{ f ([ϕ]) | ^ϕ ` ⊥} = W{ f ([ϕ]) | ϕ ` ⊥} = f ([⊥]) = 0. The crucial inequality is the third to last, which holds since ^ϕ ` ⊥ iff ϕ ` ⊥. The right to left implication can be easily derived in L. For the sake of the left to right implication we appeal to the completeness of L with respect to the class of all normal lattice expansions of the appropriate signature [9] and reason contrapositively. Suppose ϕ 0 ⊥. Then, by this completeness theorem, there is a lattice expansion C and assignment v on C such that
v(ϕ) , 0. Now consider the algebra C0 obtained from C
by adding a new least element 00 and extending the
^-operation by declaring ^00= 00. We keep the assignment
vunchanged. It is easy to check that C0is a normal lattice
expansion, and that v(^ϕ) ≥ 0 > 00and hence ^ϕ 0 ⊥.
Items 3 and 4 are proven by arguments which are dual to the ones above.
5. As to proving item 5, we reason contrapositively. Sup-pose > 0 ϕ and > 0 ψ. By the completeness theorem to which we have appealed in the proof of item 2, there are
lattice expansions C1 and C2 and corresponding
assign-ments vi on Ci such that v1(ϕ) , >C1 and v2(ψ) , >C2.
Consider the algebra C0obtained by adding a new top
el-ement >0 to C
1× C2, defining the operation ^0= ^C
0 by
the same assignment of ^C1×C2 on C
1× C2and mapping
>0 to (^>)C1×C2, and the operation0= C0 by the same
assignment ofC1×C2on C
1× C2, and mapping >0to itself.
The normality (i.e. finite meet-preservation) of0and the
monotonicity of ^0 follow immediately by construction.
The normality (i.e. finite join-preservation) of ^0is verified
by cases: if a ∨ b , >0, then it immediately follows from the
normality of ^C1×C2. If a ∨ b= >0, then by construction,
ei-ther a= >0or b= >0(i.e. >0is join-irreducible), and hence,
the join-preservation of ^0is a consequence of its
mono-tonicity. Consider the valuation v0: Prop → C0defined by
the assignment p 7→ e(v1(p), v2(p)), where e : C1× C1→ C0
is the natural embedding.
Let us show, for all χ ∈ L, that if (v1(χ), v2(χ)) , >C1×C2,
then v0(χ) , >0. We proceed by induction on χ. The
cases for atomic propositions and conjunction are imme-diate. The case for disjunction uses the join-irreducibility
of >0. When χ := ^θ, then v0(^θ) = ^0v0(θ) , >0, since, by
construction, >0is not in the range of ^0.
If χ := θ, then v0(χ)= v0(θ) = 0v0(θ). Then the
as-sumption that (v1(χ), v2(χ)) , >C1×C2 implies that v0(θ) ,
>0. Indeed, if v0(θ)= >0, then, by induction
hypothe-sis, (v1(θ), v2(θ))= (>C1,>C2) and hence (v1(θ), v2(θ)) =
>C1×C2. Therefore, from v0(θ) , >0, it follows from the
def-inition of0that v0(θ) = 0v0(θ) , >0, which concludes the
proof of the claim.
Clearly, v1(ϕ) , >C1 and v2(ψ) , >C2 imply that
(v1(ϕ), v2(ϕ)) , >C1×C2 and (v1(ψ), v2(ψ)) , >C1×C2. So, by
the above claim, v0(ϕ) , >0and v0(ψ) , >0, and hence, since
>0is join-irreducible, v0(ϕ ∨ ψ) , >0.
The proof of item 6 is dual to the one above.
Lemma B.2. For any f ∈ FA(L) and any u ∈ CA(L),
1. V
b∈L( f−^(b) → u(b))= Va∈L( f (a) → u(^a));
2. V
b∈L( f (b) → u−(b))= Va∈L( f (a) → u(a)).
Proof. For (1) we use the fact that f (a) ≤ f−^(^a)
im-plies that f−^(^a) → u(^a) ≤ f (a) → u(^a) for every
a ∈ L, which is enough to show thatV
b∈L( f−^(b) → u(b)) ≤
V
a∈L( f (a) → u(^a)). Conversely, to show that
^
a∈L
( f (a) → u(^a)) ≤^
b∈L
( f−^(b) → u(b)),
it is enough to show that, for every b ∈ L, ^
a∈L
i.e. by definition of f−^(b) and the fact that → is com-pletely join-reversing in its first coordinate,
^
a∈L
( f (a) → u(^a)) ≤ ^
^c≤b
( f (c) → u(b)).
Hence, let c ∈ L such that ^c ≤ b, and let us show that ^
a∈L
( f (a) → u(^a)) ≤ f (c) → u(b).
Since u is ∨-preserving, hence order-preserving, ^c ≤ b im-plies u(^c) ≤ u(b), hence
^
a∈L
( f (a) → u(^a)) ≤ f (c) → u(^c) ≤ f (c) → u(b),
as required. For (2), we use u−(a) ≤ u(a) and the fact that
→ is order-preserving in the second coordinate to show the
inequalityV
b∈L( f (b) → u−(b)) ≤Va∈L( f (a) → u(a)). To
show ^ a∈L ( f (a) → u(a)) ≤^ b∈L ( f (b) → u−(b))
we can show that for any b ∈ L ^
a∈L
( f (a) → u(a)) ≤ f (b) → u−(b).
After applying the definition of u−(b) and the fact that →
is completely meet-preserving in its second coordinate, the above inequality is equivalent to
^
a∈L
( f (a) → u(a)) ≤ ^
b≤c
( f (b) → u(c)).
Let c ∈ L with b ≤ c. Since f is order-preserving we get ^
a∈L
( f (a) → u(a)) ≤ f (c) → u(c) ≤ f (b) → u(c).
Definition B.3. The canonical graph-based A-frame
asso-ciated with any Fm∗is the structure GFm∗= (Z, E,R^,R)
defined as follows:14
Z:= {( f,u) ∈FA(Fm∗) ×CA(Fm∗) |
^
ϕ∈Fm∗
( f (ϕ) → u(ϕ))= 1}.
For any z ∈ Z as above, we let fz and uz denote the first
and the second coordinate of z, respectively. Then E: Z ×
Z → A, R^: Z × Z → A and R: Z × Z → A are defined as
follows:
E(z, z0) := ^
ϕ∈Fm∗
( fz(ϕ) → uz0(ϕ));
14Recall that for any set W, the A-subsethood relation between
elements of A-subsets of W is the map SW: AW× AW→ A
de-fined as SW( f , g) := Vw∈W( f (w) → g(w)). If SW( f , g)= 1 we also write f ⊆ g. R^(z, z0) := ^ ϕ∈Fm∗ ( fz−^0 (ϕ) → uz(ϕ))= ^ ϕ∈Fm∗ ( fz0(ϕ) → uz(^ϕ)); R(z, z0) := ^ ϕ∈Fm∗ ( fz(ϕ) → u−z0(ϕ))= ^ ϕ∈Fm∗ ( fz(ϕ) → uz0(ϕ)).
We will write G = (Z, E, R^,R) for GFm∗ = (Z, E,R^,R)
whenever Fm∗is clear from the context.
Lemma B.4. The structure GFm∗ of Definition B.3 is a
graph-based A-frame, in the sense specified at the begin-ning of the present section.
Proof. We need to show that R^is E-compatible, i.e.,
(R[1] ^[{β/(α, z)}]) [10]⊆ R[1] ^[{β/(α, z)}] (R[0] ^ [{β/z}]) [01]⊆ R[0] ^[{β/z}],
and that Ris E-compatible, i.e.,
(R[0] [{β/(α, z)}])[10]⊆ R[0] [{β/(α, z)}]
(R[1] [{β/z}])[01]⊆ R[1] [{β/z}].
Considering the second inclusion for R^, by definition, for
any (α, w) ∈ ZX, R[0] ^ [{β/z}](α, w) = Vz0∈Z A[{β/z}(z 0) → (R ^(w, z 0) → α)] = β → (R^(w, z) → α) (R[0] ^ [{β/z}]) [01](α, w) = Vz0∈Z A[(R [0] ^ [{β/z}]) [0](z0) → (E(z0,w) → α)],
and hence it is enough to find some z0∈ Z such that
(R[0]^[{β/z}])[0](z0) → (E(z0,w) → α) ≤ β → (R^(w, z) → α), i.e. V (γ,v)∈ZX[β → (R^(v, z) → γ)] → (E(z0,v) → γ) → (E(z0,w) → α) ≤ β → (R^(w, z) → α) (∗)
Let z0∈ Z such that uz0: Fm∗→ A maps ⊥ to 0 and every
other ϕ ∈ Fm∗to 1, and fz0:= f−^
z (cf. Lemma B.1.2). Then
E(z0,w) = Vϕ∈Fmfz−^(ϕ) → uw(ϕ)
= R^(w, z),
and likewise E(z0,v) = R^(v, z). Therefore, for this choice
of z0, inequality (∗) can be rewritten as follows:
V
(γ,v)∈ZX[β → (R^(v, z) → γ)] → (R^(v, z) → γ)
→ (R^(w, z) → α) ≤ β → (R^(w, z) → α)
The inequality above is true if
β ≤ ^
(γ,v)∈ZX
i.e. if for every (γ, v) ∈ ZX,
β ≤ [β → (R^(v, z) → γ)] → (R^(v, z) → γ),
which is an instance of a tautology in residuated lattices.
Let us show that (R[1]
^ [{β/(α, z)}])
[10]⊆ R[1]
^ [{β/(α, z)}]. By
definition, for every w ∈ ZA,
R[1] ^[{β/(α, z)}](w) = V (γ,z0)∈Z X[{β/(α, z)}(γ, z 0) → (R ^(z0,w) → γ)] = β → (R^(z, w) → α) (R[1] ^[{β/(α, z)}]) [10](w) = V (γ,z0)∈Z X[(R [1] ^[{β/(α, z)}]) [1](γ, z0) → (E(w, z0) → γ)].
Hence it is enough to find some (γ, z0) ∈ ZXsuch that
(R[1]^ [{β/(α, z)}])[1](γ, z0) → (E(w, z0) → γ) ≤β → (R^(z, w) → α), i.e. V v∈Z(β → (R^(z, v) → α)) → (E(v, z 0) → γ) → (E(w, z0) → γ) ≤ β → (R ^(z, w) → α) (∗)
Let (γ, z0) := (α,z0) such that fz0 : Fm∗→ A maps > to 1
and every other ϕ ∈ Fm∗to 0, and uz0: Fm∗→ A is defined
by the assignment
uz0(ϕ)=
(
1 if > ` ϕ
uz(^ϕ) otherwise.
by definition, uz0 maps > to 1 and ⊥ to 0; moreover,
us-ing Lemma B.1.5, it can be readily verified that uz0 is
∨-preserving. Then E(v, z0) = Vϕ∈Fm∗( fv(ϕ) → uz0(ϕ)) = Vϕ∈Fm∗( fv(ϕ) → uz(^ϕ)) = Vϕ∈Fm∗( f −^ v (ϕ) → uz(ϕ)) = R^(z, v),
and likewise E(w, z0)= R^(z, w). Therefore, for this choice
of z0, inequality (∗) can be rewritten as follows:
V
v∈Z(β → R^(z, v) → α) → (R^(z, v) → α)
→ (R^(z, w) → α) ≤ β → (R^(z, w) → α) (∗)
which is shown to be true by the same argument as the one concluding the verification of the previous inclusion.
Let us show that (R[0] [{β/(α, z)}])[10]⊆ R[0] [{β/(α, z)}]. For
any w ∈ ZA, R[0] [{β/(α, z)}](w) = V (γ,z0)∈Z X[{β/(α, z)}(γ, z 0) → (R (w, z0) → γ)] = β → (R(w, z) → α), (R[0] [{β/(α, z)}])[10](w) = V (γ,z0)∈Z X[(R [0] [{β/(α, z)}])[1](γ, z0) → (E(w, z0) → γ)].
Hence, it is enough to find some (γ, z0) ∈ ZXsuch that
(R[0] [{β/(α, z)}])[1](γ, z0) → (E(w, z0) → γ) ≤ β → (R(w, z) → α), i.e. V v∈Z(β → (R(v, z) → α)) → (E(v, z0) → γ) → (E(w, z0) → γ) ≤ β → (R(w, z) → α) (∗)
Let (γ, z0) := (α,z0) such that fz0 : Fm∗ → A maps > to 1
and every other ϕ ∈ Fm∗ to 0, and uz0:= u−
z (cf. Lemma
B.1.4). Then
E(v, z0) = Vϕ∈Fm[ fv(ϕ) → u−z(ϕ)]
= R(v, z),
and likewise E(w, z0)= R(w, z). Therefore, for this choice
of z0, inequality (∗) can be rewritten as follows:
V
v∈Z(β → (R(v, z) → α)) → (R(v, z) → α)
→ (R(w, z) → α) ≤ β → (R(w, z) → α).
The inequality above is true if
β ≤^
v∈Z
(β → (R(v, z) → α)) → (R(v, z) → α),
i.e. if for every v ∈ ZA,
β ≤ (β → (R(v, z) → α)) → (R(v, z) → α),
which is an instance of a tautology in residuated lattices.
For the last inclusion, for any (α, w) ∈ ZX,
R[1] [{β/z}](α, w) = Vz0∈Z A[{β/z}(z 0) → (R (z0,w) → α)] = β → (R(z, w) → α), (R[1] [{β/z}])[01](α, w) = Vz0∈Z A[(R [1] [{β/z}])[0](z0) → (E(z0,w) → α)],
and hence it is enough to find some z0∈ ZAsuch that
(R[1] [{β/z}])[0](z0) → (E(z0,w) → α) ≤ β → (R(z, w) → α), i.e. V (γ,v)∈ZX[β → (R(z, v) → γ)] → (E(z 0,v) → γ) → (E(z0,w) → α) ≤ β → (R (z, w) → α) (∗)
Let z0∈ ZAsuch that uz0: Fm∗→ A maps ⊥ to 0 and every
other ϕ ∈ Fm∗ to 1, and fz0 : Fm∗→ A is defined by the
assignment
fz0(ϕ)= (
0 if ϕ ` ⊥
