Knowability as continuity:
a topological account of informational dependence
Abstract
We study knowable informational dependence between empirical questions, modeled as continuous functional dependence between variables in a topological setting. We also investigate epistemic independence in topological terms and show that it is compatible with functional (but non-continuous) dependence. We then proceed to study a stronger notion of knowability based on uniformly continuous dependence. On the technical logical side, we determine the complete logics of languages that combine general functional dependence, continuous dependence, and uniformly continuous dependence.
1 Introduction and preview
Dependence in the world
Dependence occurs when objects or phenomena constrain each other’s behavior. These constraints range from complete functional determination to milder forms of correlation. At the opposite extreme lies independence: complete freedom of behavior, regardless of what the other object or phenomenon does. A common mathematical model for all this uses a family of variables for relevant items that can take values in their ranges, where correlations arise when not all a priori possible value combinations can occur. The laws of physics provide many examples: Newton’s law of gravity constrains the values that can arise for the masses of two objects, their distances, and their accelerations toward each other. Dependence is at the heart of the physical universe and our theories about it, but just as well our social world and the many dependencies in human behaviors. Logicians have long been interested in modeling this pervasive notion and studying its basic laws [Väänänen, 2007], [Baltag and van Benthem, 2021]. In this line, the present paper offers a new dependence logic in a richer topological setting that applies to empirical inquiry.
Dependence, knowledge and information flow
In a complementary sense to its physical manifestation, dependence can also be seen as an information-carrying relation. If depends functionally on , then, given the information which values the variables in have right now, we automatically know the value of . And weaker forms of correlation license weaker forms of knowledge transfer. This dual perspective was proposed in Situation Theory, where realism about constraints between situations in the world [Barwise and Perry, 1983] led to logical theories of information flow for human agents [Barwise and Seligman, 1995]. But dependence also underlies (Dynamic) Epistemic Logic, the basic theory of semantic information [Baltag and Renne, 2016], [van Ditmarsch et al., 2015], [van Benthem, 2011]. If some players get a card each from a set whose composition is common knowledge, then the card dealt to the first player constrains the card combinations available for the other players. Or epistemically, if we know the card of the first player, we also know more about which cards are held by which other player. In this paper, we will mainly pursue this informational-epistemic perspective on dependence.
Variables as wh-questions
As used in empirical sciences, ‘variables’ differ in an essential way from the First-Order Logic notion with the same name: while in FOL variables are simple placeholders, with no meaning of their own, in empirical science they are specific “what” questions (e.g. what is the position of a particle, or its velocity, momentum or acceleration, etc?). The values of a variable are the possible exact answers to the question (e.g. the exact position, etc). A variable will take different values in different possible states of the world, so in this sense variables are functions from a state space to a range of values . On the other hand, the corresponding propositional question can be understood as a partition of the state space: each cell of the partition represents (the set of worlds satisfying) a specific answer to the question. We obtain a correspondence between variables and (propositional) questions: any variable induces a partition on , whose cells are given by the sets , for all .
Functional dependence and propositional determination
Unlike in FOL, in empirical sciences the values of different variables are not necessarily independent: answering some questions may already be enough to answer other questions. In this sense, dependence is all about logical relations between questions. The standard logical setting for this is provided by the notion of functional dependence between variables/questions, expressed as a global statement in [Väänänen, 2007], and denoted in this paper by : essentially, this captures the existence of a function that maps the values of the variables in at all states into the value of at the same states. There is also a local, state-dependent version , introduced in [Baltag and van Benthem, 2021], which can be thought of as semantic determination: fixing the -values to the current ones (realized at the current state ) also fixes the value for . In the epistemic reading, a dependence statement can be seen as a conditional knowledge claim: an observer can know the current value of if given the current values of the variables in . As a special case, when is a Boolean variable associated to some proposition , we obtain a natural ‘determination modality’ , which says that fixing the -values to the current ones (at ) ‘determines’ the truth of (i.e. fixes its value to ‘true’).
The complete logic of these notions was investigated in [Baltag and van Benthem, 2021]. Our concern in this paper is lifting an important idealization in the preceding framework, which is necessary to make dependence logics function in a setting of empirical investigation.
From idealized sharp values to empirical measurement
Standard scenarios in epistemic logic are discrete, and it then makes sense to work with sharp values of variables, such as truth values for proposition letters. However, in the empirical sciences, and in daily life, values are usually determined by imprecise observations or measurements. Even if not in error, these deliver only intervals or other sets of values containing the real value. Of course, one can perform more measurements and combine outcomes, or turn to a more precise measuring device, but sharp individual values for variables will still not be delivered. Thus, in empirical inquiry, the view of dependence as conditional knowledge of sharp values becomes unrealistic.
Here we arrive at the main question of this paper. How should we model dependence and its logic in an empirical setting where only measurements with limited precision are available? We need a richer style of modeling for outcomes of observations or measurements, and we need a way of describing how empirical knowledge can arise though a process of approximation.
Topological models for empirical inquiry and knowledge
As it happens, a suitable richer style of modeling exists. Topological models have been around since the 1930s for modeling intuitionistic and modal logics [van Benthem and Bezhanishvili, 2007], where the surplus of topological spaces over plain sets elucidates epistemic notions such as knowledge or verifiability. In our present setting, open sets in a topological space represent possible outcomes of experiments or measurements, while propositions of interest are modeled by arbitrary subsets. In this way, topological notions acquire epistemic meaning. For instance, a property denoting an open set is ‘verifiable’ in that, for any point satisfying , there exists an experiment that can tell us that the point has that property. Dually, properties denoting closed sets are falsifiable. In this setting, even technical separation properties for topological spaces make epistemic sense: e.g., the -property says that any point can be identified uniquely by experiments, since any other point can be separated by some measurement. The area of Epistemic Topology exploits all these features, witness important studies like [Kelly, 1996], [Dabrowski et al., 1996], [Baltag et al., 2019]. Our analysis of dependence follows up on this, by looking at further structure in dependence models with topologies over the value ranges for the variables.
Empirical variables as topological maps
We are thus lead to a natural modeling of empirical variables as functions from a state space onto a topological space : in this way, in addition to the exact value of variable at state (an idealization which typically is not accessible by measurements), we also have observable approximations of this value, given by open neighborhoods with . Finally, topological spaces allow us to treat sets of variables as single new entities taking tuples as values, by using the product topology on the Cartesian product value spaces for the separate . This uniform treatment of single variables and finite sets of these greatly simplifies epistemic analysis.
Propositionalization: empirical questions as topologies
If we move from empirical variables to the corresponding propositional questions, this requires refining the partitional view of questions into a topology on the state space ; any open neighborhood of the current state in the question’s topology will represent a partial, “inexact” answer to the given question: these are the “feasible” answers, that one can determine by observations (measurements).111The underlying partition of into cells (representing the ‘exact’ answers) can still be recovered from this topological representation: the cell of state consists of all states that are “topologically indistinguishable” from , i.e. that belong to exactly the same open sets as . The above-mentioned correspondence between variables and questions-as-partitions extends to their topological versions: the topology on the range of values of variable naturally induces a topology on the state domain , having open sets of the form , for any open .
Continuity as information-carrying dependence
We have presented dependence as delivering conditional knowledge of given . But note that this required being given the exact value(s) of . In an empirical setting such precision is seldom achievable: all we can observe are measurable approximations. Thus, a useful and truly ‘epistemic’ dependence should allow us to approximate the value of arbitrarily closely given suitable approximations for the values of . In its global form, this requires that the dependence function mapping -values to -values be globally continuous with respect to the underlying topologies. This is the definition of our known epistemic dependence : the observer knows that she can get to know the value of as accurately as needed if given accurate enough approximations of . What makes this dependence “epistemic” is the fact that it requires only observable approximations, and what makes it “known” is its globality. As in the case of exact dependence, there is also a local version of epistemic dependence, which only requires that the dependence function is continuous on some open neighborhood of the exact value(s) (of at the current state ). We read as knowable epistemic dependence: the observer can come to know (after doing an accurate enough measurement of ) that she can get to know the value of as accurately as needed if given accurate enough approximations of .222There exists an even “more local” version of epistemic dependence, requiring only point-continuity at . But this is in a sense “too local”, too sensitive to the actual value of , at the risk of being “unknowable”: may hold without ever being known to the observer, no matter how accurate her observations. In epistemological terms, point-continuity is not an ‘introspective’ fact.
Special case: conditional knowability of a proposition
As in the case of exact dependence, we can apply epistemic dependence to the case when is a Boolean variable associated to a proposition , obtaining a natural notion of knowability of a proposition given (accurate enough approximations of) : holds at if there is if there is some -open neighborhood of (in the topology induced by on the state space) all of whose members satisfy . This means that one can come to know that was the case by measuring with enough accuracy. The modality connects back to the standard topological semantics for modal logic, more precisely to the so-called interior semantics: note that satisfies iff it is in the interior of the set of states satisfying (where interior is taken wrt the topology induced by on the state space). As such, this notion fits well with the recent epistemic interpretations of the interior operator in terms of “knowability”.
Further notions: full independence versus topological independence
In mathematical practice, independence of variables often makes for greater simplicity than dependence. The probability of two independent events is just their product, no analysis of correlations is required. Independence, too, has a natural interpretation in the above models. Two sets of variables and are fully independent if, given the states that occur in our model, knowing the exact values of the variables in tells us nothing new about the values of (i.e. it still leaves them free to take on any combination of values that the model allows them anywhere). Independence is zero-correlation of -values with -values, functional dependence is total correlation.333There are also intermediate forms of correlation, as in the above epistemic models, but we will not study these as such in this paper. However, various forms of value correlation can be expressed in the logical languages for dependence models to be introduced later. But for empirical variables, this notion of independence is epistemically irrelevant (since typically we cannot know the exact values of ). The richer topological setting offers a more subtle concept: two sets of variable and are topologically independent if no matter how accurate measurements of we are given, we can never learn anything new about . Interestingly enough, topological independence is compatible with global functional dependence! So we can have a total correlation (which in principle would give us complete knowledge of the exact values of if we only were given the exact values of ), while at the same time having topological independence (so that no approximate observation of can tell us anything about ). In our paper, we characterize such situations mathematically in terms of the dependence function being “everywhere surjective” [Bernardi and Rainaldi, 2018], thus significantly expanding the current interfaces of Epistemic Topology with mathematics. More philosophically, the extended framework obtained in this way allows us to reason about in-principle learnability and unlearnability on a par.
Special topologies
While our discussion may have suggested that we abandon standard (relational) epistemic logic, the topological setting contains in fact standard epistemic models as the special case of discrete topologies on the range of values (where all subsets of the space are open). In this case, the topologies induced on the state space are partitional, and we can thus interpret the corresponding propositional questions as “agents” (modeled using the accessibility relations associated to these partitions). and collapse to the same notion in this case (capturing ‘epistemic superiority’ of group over [Baltag and Smets, 2020]), and similarly and collapse to the standard notion of distributed knowledge. Another special class of topologies, to be used extensively in our later technical proofs, are Alexandrov spaces where each point has a smallest oopen neighborhood. These spaces match the usual models for modal and support a reduction to relational models where the accessibility relation is the standard topological specialization order . In what follows, such relational models will allow us to use standard modal techniques.
‘Knowing how’: from plain continuity to uniform continuity
Even a known epistemic dependence leaves something to be desired. The inverse map associated with a continuous function , from open neighborhoods of values to open neighborhoods of , is state dependent. So, the agent knows that she can approximate as accurately as desired given an accurate enough approximation of , but she may not know in advance how accurate needs the measurement of be (in order to obtain the desired accuracy for ). To have in advance such an explicit ‘epistemic know-how’ (as to which approximation works) she needs the dependence function to be uniformly continuous. Formalizing this stronger notion of conditional knowability how (to find from ) requires an even richer setting. We chose to use for this the well-known framework of metric spaces [Willard, 1970], mostly for reasons of accessibility to a general philosophical audience; but uniform continuity can also be defined in a more qualitative way in the much more general framework of uniform spaces [Isbell, 1964], and the even more general setting of quasi-uniform spaces, and our notions and results do carry through to these qualitative generalizations.
The content of this paper can be viewed in two ways. Technically, it presents a natural next step for current Logics of Dependence, moving from set-based models to topological ones, and leading to several new completeness, representation, and decidability theorems proved by extending modal techniques to this setting. More philosophically, however, what we offer in analyzing and defining notions of information-based dependence is an invitation to Epistemic Topology, an area of formal philosophy where many new concepts become available once we go beyond its already established interfaces with mathematics and computer science. In line with this, we see both our definitions and our theorems as main contributions of this paper.
Plan of this paper
Section 2 introduces the basic notions of empirical wh-questions, in two equivalent versions: empirical variables as topological maps, and propositional questions as topologies. Section 3 introduces and investigates various notions of dependence and the corresponding modalities: exact functional dependence (in both its global and local versions) and the determination modality, knowledge and knowability of a proposition given a set of variables, and most importantly the key notion of continuous (epistemic) dependence (in both its global and local versions). Section 4 contains the formal syntax and semantics of our decidable logic of continuous dependence , a sound and complete proof system to reason about epistemic dependence, as well as some concrete examples. Section 5 discusses the notions of full independence and topological independence, and their interplay with functional dependence in a topological setting. Section 6 extends the setting to uniformly continuous dependence on metric models, and presents the syntax and semantics of the decidable logic of uniform dependence (which in fact also comprises all the other forms of dependence and modalities encountered in this paper), as well as a sound and complete axiomatization of this logic. Section 7 lists some further directions of immediate epistemic relevance, including richer dynamic logics of approximation, a notion of computable dependence understood as Scott continuity, the use of ‘point-free topologies’, etc. A summary of results and general conclusions is found in Section 8. All the proofs of completeness and decidability are found in the Appendix.
2 Basic framework: empirical questions
In this section, we present a topological setting for imprecise observations. Our first task is the introduction of empirical questions, for which only imprecise partial answers may be observable. These will come in two variants: ‘wh-questions’ (whose answers are non-propositional objects or ‘values’: numbers, names or some other form of data), and propositional questions (whose answers are propositions). The first type (wh-questions) will be modeled as ‘empirical variables’, i.e. quantities that take values in some appropriate value space. Formally, empirical variables are maps from the state space to some topological space (where the open neighborhoods of the actual value of the variable in a state representing the measurable approximations of that exact value). The second type (propositional questions) will be represented as topologies on a state space , with the (inexact) propositional answers being given by the open neighborhoods of the actual state. This generalizes the traditional ‘partitional’ view of propositional questions (in which the possible exact answers form a partition of the state space) to the case of empirical questions, for which typically only inexact, approximative answers are epistemically available: such answers can be more or less precise, and so they are only partial answers, which can thus overlap, or even refine each other.
As we shall see, the two settings (wh-questions as empirical variables, and propositional questions as topologies) are in some sense equivalent: we can always ‘propositionalize’ any wh-question, and conversely we can associate a quantitative variable to every propositional question. Moreover, these correspondences are structure-preserving, and so the two settings obey the same logic . However, the correspondence is not one-to-one: many different wh-questions correspond to the same propositional one. This reflects the intuitive fact that the first setting (of wh-questions as variables) is richer, giving us more information (in the form of the ‘actual values’ of the variable). For this reason, we will choose this first setting as the preferred formal semantics for our logic (as a logic of dependence between empirical variables).
2.1 Preliminaries on topology
While in this paper we assume familiarity with basic notions of General Topology, we briefly review some of them here, mainly in order to fix the notation.
Topologies, neighborhoods and local bases Recall that a topological space consists of a set (the domain, consisting of ‘points’ or ‘values’ ), together with a family of ‘open’ sets, assumed to include and itself, and to be closed under finite intersections and arbitrary unions. The complements of open sets are called ’closed’. For a point , we put
for the family of open neighborhoods of . A family of opens is a basis (or ‘base’) for the topology if every open set is a union of open sets from . In this case, we also say that is the topology generated by the basis .
Interior and closure The well-known topological interior and closure operators are defined as usual, as maps , defined by putting for all sets of values :
In words, is the largest open subset of , while is the smallest closed superset of .
Specialization preorders, topological indistinguishability and separation axioms Given a space , we denote by the specialization preorder for its topology, defined by putting, for all :
We also denote by the topological indistinguishability relation, defined as:
For any point , we will denote its equivalence class modulo the indistinguishability relation by
The space is -separated if topologically indistinguishable points are the same, that is, implies (for all ); equivalently, iff every equivalence class is just a singleton ; and again equivalently: iff the specialization preorder is a partial order (i.e., also anti-symmetric).
The space is -separated if the specialization preorder is the identity, i.e. implies .
Continuity at a point A function between topological spaces is continuous at a point if we have
or equivalently: for every open neighborhood of , its preimage is an open neighborhood of .
Global and local continuity is (globally) continuous if it is continuous at all points . is locally continuous at (around) a point if it is continuous at all points in some open neighborhood of .
Subspaces and quotients Every subset of (the domain of) a topological space determines a subspace , obtained by endowing with its subspace topology
Every equivalence relation on (the domain of) a topological space determines a quotient space , having as set of values/points the set
of equivalence classes modulo , endowed with the quotient topology , given by putting for any set of equivalence classes:
The quotient topology is the largest (“finest”) topology on that makes continuous the canonical quotient map , that maps every point to its equivalence class .
Compactness and local compactness A topological space is compact if every open cover of has a finite subcover; i.e., for every collection of open subsets s.t. , there exists a finite subcollection s.t. . A subset of a topological space is compact if the subspace determined by it is compact. A space is locally compact if every point has a compact neighborhood; i.e. for every there exists some open set and some compact set s.t. .
Metric spaces, pseudo-metric spaces and ultra-(pseudo-)metric spaces A pseudo-metric space consists of a set of points, together with a ‘pseudo-metric’ (or ‘pseudo-distance’) , satisfying three conditions: ; ; . A metric space is a pseudo-metric space satisfying an additional condition, namely: implies . In this case is called a metric (or ‘distance’). Every pseudo-metric space is a topological space, with a basis given by open balls
Note that the interior of any set is the union of all the open balls included in :
while dually the closure is the intersection of all the closed balls that include :
Metric spaces are -separated, hence also -separated.444But pseudo-metric spaces are not necessarily so: in fact, a pseudo-metric space is -separated only iff it is a metric space.
A familiar concrete example of metric spaces are the Euclidean spaces of integer dimensions , consisting of -tuples of real numbers , endowed with the Euclidean distance . Euclidean spaces have the important property that they are locally compact (but not compact).
Another example are the ultra-(pseudo-)metric spaces: a (pseudo-)metric is said to be an ultra-(pseudo-)metric if it satisfies a stronger version of the above triangle inequality, namely .555A concrete example of ultra-metric spaces are the so-called -adic fields , for any prime number : in a certain mathematical sense, these are ultra-metric analogues of the field of real numbers .
Uniform continuity A function between two pseudo-metric spaces is uniformly continuous if we have
In contrast, global continuity corresponds in a metric space to swapping the quantifiers and in the above statement to the weaker form
A function is locally uniformly continuous at (around) a point if its restriction to (the subspace determined by) some open neighborhood is uniformly continuous.
These various forms of continuity may collapse to the same notion in especially favorable situations, of which we give here two examples.
Proposition 2.1.
(Heine-Cantor Theorem) If is a map from a compact metric space to another metric space, then is (globally) continuous iff it is (globally) uniformly continuous.
If is a map from a locally compact metric space to another metric space, then is locally continuous (on a neighborhood) around a point iff it is locally uniformly continuous (on a neighborhood) around .
For our second example, we need a few more definitions.
Lipschitz, locally Lipschitz and pseudo-locally Lipschitz functions A function between two pseudo-metric spaces is Lipschitz if there exists a constant (called ‘Lipschitz constant’) s.t. for all we have that
is locally Lipschitz if for every there exists some open neighborhood of , such that the restriction to (the subspace determined by) is Lipschitz.
Finally, is pseudo-locally Lipschitz666Unlike the other concepts in this Preliminaries’ section, the notion of pseudo-local Lipschitz functions seems to be novel. if for every there exists some open neighborhood of , and some open neighborhood of , such that the restriction to (the subspace determined by) the intersection of with the preimage is Lipschitz.
Proposition 2.2.
A Lipschitz function between pseudo-metric spaces is uniformly continuous.
For every point , a locally Lipschitz function is locally uniformly continuous around .
A pseudo-locally Lipschitz function is continuous at some point iff it is locally uniformly continuous around (and so also iff it is locally continuous around ).
Proof.
The proofs of all the above results are standard, with the exception of the last item. To justify it, assume is pseudo-locally Lipschitz, and let and be s.t. is Lipschitz on . Assume now that is continuous at in , hence we have , and thus is an open neighborhood of . Since is Lipschitz on the open neighorhood , it is also uniformly continuous on it (by the first item of our Proposition), and therefore it is locally uniformly continuous around .∎
In conclusion, the notions of local continuity and local uniform continuity are equivalent on locally compact spaces; while all three notions of localized continuity (-continuity at a point, local continuity around the point, and local unform continuity around the point) coincide for pseudo-locally Lipschitz functions! As we’ll show, these facts have interesting epistemological and logical consequences, with a special relevance to our completeness and expressivity results.
2.2 Empirical variables as inexact wh-questions
In this section, we fix a state space . A proposition is just a subset of the state space . To stress this reading, we sometimes write for , and read it as “ is true at ”.
As traditionally understood, a wh-question is one that starts with “what”, “who”, “which”, “where”, “when” etc. Examples are “What is the speed of light?”, “Where on Earth I am?” (i.e. what is my position on the globe), “When did you first arrive to Amsterdam?”. The exact answer to a wh-question is not necessarily a proposition, but can be some other type of object, e.g. a number, a pair or triplet of coordinates, a date, a name etc. Here, we will think of each such object as the “value” assigned to a variable in a given state of the world. Note that, unlike the variables of predicate logic (which are just abstract, interchangeable placeholders with no intrinsic meaning, that can take any arbitrary values independent of each other), ours are “variables” in the sense used in empirical sciences and databases: they denote specific quantities or qualitative data (e.g. time, position, velocity, money, persons, shapes etc.), each with its own range of possible values, that may be subject to restrictions and inter-variable correlations. The generic form of a wh-question can thus be reduced to “What is the value of variable ?”, where “the value” refers to the current value of in the actual world.
When calling our variables “empirical”, what we mean is that their exact value might typically be inaccessible to observation. Instead, one can usually observe only approximations of that value (e.g. a time interval, an area on the surface of the Earth, a range of speeds, a set of possible suspects, etc). So, when thinking of an empirical variable as a wh-question, its feasible answers (the ones one could obtain via some kind of empirical process e.g. an observation or experiment) are typically “imprecise” or partial answers, in the sense that may not completely match the exact answer.
We now proceed to formalize this key notion within a topological setting.
Definition 2.3.
(Empirical variables as topological maps) Given a state space , an empirical variable is a surjective map from states to ‘values’ in a -separated topological space .
Intuitively, the open neighborhoods represent observable approximations of the value of at state , obtainable e.g. as a result of a measurement of the value of . Both the surjectivity condition, saying that , and the requirement of -separation are innocuous: we can always enforce them by taking first a subspace (restricting to both the codomain and its topology), and then a quotient (identifying all indistinguishable points in ). The point of these requirements is that they simplify several definitions and statements of results below.
Example: Euclidean variables A well-known example is that of Euclidean variables , for some : here, is the -dimensional Euclidean space for some (consisting of all real-number vectors ), and is the standard Euclidean topology, generated by the family of all -dimensional open balls of the form
where , , and is the standard Euclidean distance. Any open ball , with , can be considered as a measurement of the value of with margin of error .
Example: a particle in space For a more concrete example, consider a point-like particle in three-dimensional space. The state space is . Consider the question “What is the -coordinate of the particle?”. As a wh-question, this is an empirical variable , with and the natural topology is given by the family of rational open intervals , where with .777The restriction to intervals with rational endpoints corresponds to the fact that actual measurements always produce rational estimates. Suppose the particle is actually in the point : so this triplet =is the actual state. Then the exact answer to the wh-question is the actual exact value of the variable at state , while the feasible approximations at are rational intervals with . The similar wh-questions regarding the other two coordinates and are similarly represented by empirical variables , with the same topology as before.
All topological notions introduced in the Introduction relativize to the range space of some empirical variable , simply by labeling them with the subscript : so e.g. is the specialization preorder for the topology . Note that we don’t need a special symbol for the corresponding indistinguishability relation on : since the space is assumed to be , indistinguishability on simply boils down to equality .
Special case: exact questions An exact wh-question on a state space is just a variable mapping states into values living in a discrete space, i.e. s.t. . Intuitively, this means that at every state one can observe the exact value of the variable . The topology is then irrelevant: the complete answer to the question can be determined, so no partial approximations are really needed.
2.3 Abstraction: propositional questions
A special case of empirical questions are the ones whose answers are propositions: we call these “propositional questions”. Traditionally, a propositional question is taken to be a partition of the state space : the partition cells are the possible (complete) answers to the question, while the unique cell that contains a given state is the true answer at state . But, once again, in empirical sciences the complete answer may be impossible to determine by observations; typically, only partial answers are empirically given. Hence, the partition into complete answers must be replaced by a family of propositions, called ‘feasible’ or ‘observable’ answers.
Definition 2.4.
(Empirical questions of the propositional kind) A (propositional) empirical question is just a topology on the set of states . If the actual state is , then the open neighborhoods with represent the feasible or ‘observable’ answers. So is the family of all partial answers to the question that are (true and) observable at state .
The closure properties of make obvious sense in this interpretation. Closure under binary intersections reflects the fact that the conjunction of two (true) feasible answers is itself (true and) feasible: indeed, is empirically established iff both and are. Closure under arbitrary unions means that any arbitrary disjunction of (true) feasible answers is itself a (true and) feasible answer to the question: indeed, is empirically established iff at least one of the ’s is.888Note that the corresponding closure condition for arbitrary conjunctions does not apply to feasible answers: indeed, while for establishing an infinite disjunction is sufficient (and necessary) to establish only one of the disjuncts, establishing an infinite conjunction would necessitate to first establish all of the conjuncts. This would require waiting an infinite amount of time, hence it is unfeasible in an empirical context. Finally, the tautological ’answer’ (corresponding to the trivially true proposition given by the whole state space ) is surely feasible, albeit uninformative.
Complete answers are not necessarily feasible. The complete ’answer’ to the question at state is the equivalence class of wrt the topological indistinguishability relation for . The complete answer is the propositional analogue of the ‘exact’ value of an empirical variable. The fact that the complete answer might not be feasible is reflected in the fact that this equivalence class is not necessarily an open set. The indistinguishability relation induces a partition on , whose cells are the equivalence classes modulo , corresponding to all the possible complete answers to the question.
Example continued: the particle in space Recall our example of a point-like particle situated in the point . Instead of answering the wh-question “what is the -coordinate?” by simply specifying the exact value of the corresponding empirical variable, we can interpret the question as a propositional one, whose complete answer is , which in English corresponds to the proposition “The -coordinate of the particle is ”. Similarly, if only an approximation of (with and ) is feasible or measurable, then the same information can be packaged in a partial answer to the corresponding propositional question: in English, this is the proposition “The -coordinate is between and ”.
As seen in this example, every wh-question can be “propositionalized”, i.e. converted into a propositional question, by abstracting away the actual values. We proceed now to formalize this process of abstraction from values.
From variables to propositional questions: the (weak) -topology on . To any empirical variable , we can associate a propositional empirical question , called the -topology on : this is the so-called ‘weak topology’ induced by on , defined as the coarsest topology on that makes continuous. More explicitly, is given by
We can interpret the -topology as the result of ‘propositionalizing’ the wh-question . An -neighbourhood of a state is just a neighbourhood of in the -topology on , i.e. a set with for some . As usual, for a state , we denote by the family of open -neighborhoods of . Similarly, the -interior of any set is the interior of in the -topology, and the same for the -closure . Finally, note that the -topology is not necessarily -separated (unlike the topology on the value range of , which was assumed to be ): indeed, the value of a variable can well be the same in two different states.999However, it would be natural to further assume that any two states that agree on the values of all the relevant variables are the same state: that would allow us to identify our ‘states’ with tuples of values (or rather assignments of values to all the relevant variables), obtaining a ‘concrete’ representation of the state space, in the style typically used in Physics and other empirical sciences. This additional assumption will be embodied in the so-called “concrete models”, defined in the next section as a special case of our more general topo-models.
-relations on states The relations and on the range space naturally induce corresponding relations on states in , defined by putting for all :
The first relation coincides with the specialization preorder for the weak (-)topology on states; while the second relation corresponds to the (indistinguishability for the -topology, which by -separation is the same as the) equality of -values on the two states.
Special case: partitions as exact propositional questions Note that the propositional counterpart of an exact wh-question on a state space is a partition of , whose partition cells are sets of the form , with . Conversely, every partition of can be viewed as a propositionalized exact question. So, from a purely propositional perspective, exact questions are just partitions of the state space.
2.4 Equivalence between variables and (propositional) questions
As we saw, we can go from wh-questions (modeled as empirical variables) to propositional questions, by abstracting away from the actual values: replacing the variable with the (weak) -topology . We show now that we can also go back (from questions to empirical variables), essentially by taking the complete answers as actual values, with the topology induced by the feasible answers.
From propositional questions to variables: the quotient topology. Given any propositional empirical question (topology) , we can convert it into a wh-question by taking as our associated empirical variable the canonical quotient map from to the quotient space modulo the topological indistinguishability relation for ; more precisely, we take
to be the set of all equivalence classes wrt ; is the quotient map , given by
and we endow with the quotient topology , given by
It is easy to see that these two operations are inverse to each other. First, if we start with an empirical variable , take its associated -topology on , then take the canonical quotient map (modulo the indistinguishablity relation for , which as we saw is exactly the relation of equality of -values), then the result is ‘isomorphic’ to the original variable : more precise, the topological range space (with the quotient topology) is homeomorphic to the original space via the canonical homeomorphism that maps every value to the equivalence class modulo ; and moreover, the quotient variable coincides with the functional composition of the homeomorphism and the original variable . Vice-versa, if we start with a propositional question/topology on , take its canonical quotient map (modulo its topological indistinguishability relation ), and take the associated weak topology on , we obtain exactly the original topology .
This equivalence between empirical variables on (wh-questions) and topologies on (propositional questions) extends to all the notions defined in this paper, and will form the basis of two equivalent semantics for our logic (topo-dependence models and standard topo-models). However, note that this equivalence is not a bijection. While the second correspondence (going from propositional questions to variables, via our quotient construction) is injective, the first correspondence (going from variables to propositional questions, via ‘propositionalization’) is not injective: many different variables can give rise to the same weak topology on the state space. This fact captures the intuition that the setting of empirical variables is in some sense ‘richer’ than the one of propositional questions.
2.5 Joint questions
In an inquiry, we are typically interested in answering multiple questions simultaneously: e.g. we want to find the spatial , and coordinates of a point, as well as its temporal coordinate (with respect to some system of reference). We can combine such a set of questions into a single joint question, e.g. “what are the space-time coordinates of the point?”. A propositional answer to such a joint question will be a conjunction of propositional answers to each of the underlying simple questions, so a joint propositional question can be seen a the coarsest topology that refines all underlying topologies; while a value/object answer to a joint wh-question will be a tuple of values (each answering one of the underlying wh-questions), so a joint wh-question can be modeled using the product topology.
We first start with the propositional case.
Sets of propositional questions as joint questions: the join topology Given a set of topologies on a state space (interpreted as empirical questions), we can regard it as a single question, given by the supremum or “join” (in the lattice of topologies on with inclusion) of all the topologies . This is the topology generated by the union of the underlying topologies: the coarsest topology on that includes all of them. The indistinguishability relation for this join topology coincides with the intersection of the indistinguishability relations of each topology . The complete answer to the join propositional question at state is thus the intersection of the complete answers at to all the propositional questions ; while a partial answer to the join question, i.e. an open set , is an intersection of partial answers to all the underlying questions .
Some special cases When is the empty family of topologies, is the trivial (‘indiscrete’) topology on . When is a singleton, the joint question corresponding to the set is the same as the question/topology .
We now move on to the more interesting case of joint empirical variables.
Sets of variables as joint wh-questions: the product topology A finite set of empirical variables can itself be regarded as a single variable (hence, our use of the same notation for both variables and sets of variables, a common practice in, e.g., Statistics when dealing with random variables), essentially given by taking the product map into the topological product space (suitably restricted in its range to make this map surjective). More precisely, given such a finite set of empirical variables, we can associate to it a single variable, also denoted by , as follows:
-
the set of values ;
-
the topology is the restriction to of the product topology on , generated by the restrictions to of all products of open sets (in their own topologies );
-
finally, the map is given by .
Essentially, we can interpret the products as the possible results of a simultaneous measurement of all these variables. Since there might be correlations between the variables, the actual range of results as defined above is not necessarily the whole Cartesian product, but a subset of it. Putting it in our earlier interrogative terms, the variable represents the joint question obtained by simultaneously asking all the wh-questions in the set , and is a joint approximate answer to all these questions.
Some special cases When is empty, with the empty string, the trivial topology on (which in this case coincides with the discrete topology!), and the map given by for all . Note that, since the weak -topology is the trivial topology on , its indistinguishability relation is the universal relation on (relating every two states). When is a singleton, the single variable corresponding to the set is the same as itself.
Given the preceding, from now on we will use the notation for both single variables and for finite sets of variables, identifying the set with the associated single variable (and dually identifying a single variable with the associated set ).
Sanity check: equivalence between the two notions of joint questions It is easy to see that above-mentioned equivalence between propositional empirical questions and empirical variables extends to the notion of joint question/variable. Indeed, the weak topology induced on by the product variable is exactly the join supremum) of all the topologies (with ).
3 Information-carrying dependence as topological continuity
In this section, we present a conceptual analysis of notions of epistemic dependence that make sense in a topological setting for imprecise observations. The outcome is a series of definitions, for which we prove some simple clarificatory characterizations. Deeper technical results on the resulting topological dependence logics are deferred to the next section.
We start by reviewing the older notion of exact (non-epistemic) dependence as it occurs in the Logic of Functional Dependence in [Baltag and van Benthem, 2021], then we move to exploring various types of known/knowable dependence.
For this purpose, we fix once again a set of epistemic states or ‘worlds’ : intuitively, these are all the states that are consistent with some (implicit) agent’s background information.
3.1 Background: exact dependence in
The form of dependence studied in Dependence Logic () [Väänänen, 2007], denoted in literature by and here by , is both exact and global: it requires the existence of a global functional dependence, that maps all exact values of the variable (or set of variables) into the exact values of the (set of) variable(s) . The Logic of Functional Dependence () introduced in [Baltag and van Benthem, 2021] goes beyond this, by introducing a local, but still exact, version of dependence : the current exact value of (in the actual world) uniquely determines the current exact value of (in the same actual world).111111This local version of dependence introduced in is more fundamental, in a sense, than the global one of : it turns out that local (combined with local determination modality ) can define global , but not the other way around. In addition, in one considers propositional dependence operators (“exact determination”): the (current) exact value of determines to be true, These modalities that can be seen as a special case of local dependence , in which the determined variable is propositional (denoting a Boolean function from states to truth values, seen as the characteristic function of a set of states ) and its uniquely determined value is (‘true’).
In this section we review the basics of . Note that these definitions are set-theoretical in nature: they do not use the topological structure of our space of values, but only the (set of) values themselves. This expresses the fact that this form of dependence is exact and ‘informational’ (i.e. the exact value of carries full information about the exact value of ), rather than approximate and ‘epistemic’ (having to do with an observer’s ability to infer as good estimates as needed for the value of from sufficiently precise approximations of ’s value). The epistemic versions will come in subsequent sections.
We start with the special case of propositional dependence operators:
Exact determination of a proposition by a variable Given a state space , a (finite set of) empirical variable(s) and a proposition , we say that is determined by at state , and write , if the (exact) value of (at ) carries the information that is true (at ):
where is the equality of -values (defined as above: iff ). Note that is just a standard relational modality, having as its accessibility relation. In particular, since holds for all , is the universal modality (quantifying over all states):
This motivates an abbreviation , saying that is true in all states:
Abstraction: exact determination by a propositional question By abstracting away from the specific values of the variable, we can ‘lift’ this notion to the level of propositional questions. Given a state space , a proposition and a (empirical) propositional question (i.e. topology) on , we say is determined by (the answer of) at state , and write , if the (complete) answer to (at ) carries the information that is true (at ):
where recall that is the equivalence class of wrt the indistinguishability relation for the topology . One can easily recognize as a standard relational modality having topological indistinguishability as its underlying accessibility relation:
Note again that the topology itself plays no role, but only the associated equivalence relation , or equivalently the corresponding partition of the state space into equivalence classes: in effect, this is really about the information carried by the underlying “exact” (partitional) question.
Exact dependence between variables Given two (finite sets of) empirical variables and over the same state space , we say that exactly determines at state , and write , if the value of at uniquely determines the value of :
Since holds for all , the statement holds iff is a constant: its value is the same in all states. We can thus introduce an abbreviation (saying that “ is a constant”):
Abstraction: exact dependence between propositional questions By abstracting again from the specific values, this notion is lifted to the level of propositional questions: given topologies and on the same state space , we say that exactly determines at state , and write , if the exact answer to at uniquely determines the exact answer to :
where and are equivalence classes wrt indistinguishability relations for and .
Once again, the topologies themselves play no role, but only the corresponding partitions of the state space into equivalence classes. In effect, this notion is purely about the dependence between partitional questions: the (true) answer to the first question gives us full information about the (true) answer to the second question.
The logic of functional dependence The operators and are at the heart of the simple Logic of Functional Dependence ()121212This logic was introduced, in a purely set-theoretical setting, devoid of topological features, in [Baltag and van Benthem, 2021]., with the following syntax:
where the letters range over finite sets of variables (coming from a fixed set ), the letters are predicate symbols (coming from a finite set of such symbols) each having a specific arity , and is any -tuple of variables in .
Given the above discussion, it should be clear that this logic has two equivalent interpretations: one in terms of empirical variables (regarded purely set-theoretically, as simple assignments of values to states, with no topological structure), and another one in terms of partitions (or equivalence relations, hence the name “relational semantics”).
In particular, variable-based dependence models come with: a state space ; a way to assign to each syntactic variable some map that associates to each state some value (in some range of values ); and a way to interpret each -ary predicate symbol as an -ary relation between values. The value assignment can be naturally extended to (finite) sets of variables , by putting for all , and then equality of values can be defined as above, by putting: iff . The variable-based semantics of the atoms is given as usual by putting
The equivalent relational semantics only assumes given a family of equivalence relations (or partitions) on , one for each basic variable , and simply treats the atoms using a valuation (subject to additional constraints, see the Appendix for details). In both versions, the semantics for Boolean connectives uses the classical Tarskian clauses, while the semantics of exact dependence and determination operators is given by putting:
The operators (for universal modality) and (for “ is a constant) can be defined as abbreviations in this logic, as mentioned above: , and .
Global dependence As already mentioned, the standard notion of (functional) dependence in Dependence Logic is global: using our notation , this is usually defined by putting
which can equivalently be stated in terms of equality of values:
For propositional questions, given by topologies on , the corresponding notion is simply the global version of local dependence :
(where recall that and are the equivalence classes of wrt the indistinguishability relations for the topologies and ). Once again, note that this is a purely set-theoretic notion, in which the topologies do not play any role in themselves, but only vis the induced equivalence relations: global functional dependence is also in effect a relation between partitional questions. Also, it is again easy to see that these two notions of global dependence fit together, via the correspondence given by the weak topology; i.e., we have that
In , global dependence is not a primitive notion, but can be defined via the abbreviation:
Indeed, it is easy to see that the semantics of the formula matches the above semantic clause for .
A sound and complete proof system Here is a version of the axiomatic proof system for the Logic of Functional Dependence, whose completeness is the main technical result in [Baltag and van Benthem, 2021]:
(I) | Axioms and rules of Propositional Logic |
(II) | Axioms for Determination: |
(-Necessitation) | From , infer |
(-Distribution) | |
(Factivity: axiom ) | |
(Axiom ) | |
(Axiom ) | |
(III) | Axioms for exact dependence: |
(Inclusion) | , provided that |
(Additivity) | |
(Transitivity) | |
(Determined Dependence) | |
(Transfer) | |
(Determined Atoms) |
3.2 Propositional knowledge and conditional knowability of a proposition
Next, we take a look at some epistemic attitudes in an empirical setting. We start with propositional ‘knowledge’, then proceed to analyze when a proposition is ‘knowable’ given (a good enough approximation of the value of) some empirical variable .
Propositional knowledge as universal quantification over epistemic possibilities We say that a proposition is known, and write , if holds in all epistemically possible states, i.e., if in fact we have that . So, in our setting, the knowledge operator is simply the above-defined universal modality, quantifying over all epistemic states:
Conditional knowability, given (approximate values of) a variable Given a proposition and an empirical variable , we say that is knowable given at state (or knowable conditional on ), and write , if the truth of at is determined by some (good enough) approximation of the value , i.e. if we have
Intuitively, this means that one can come to know that is true, after observing a sufficiently accurate estimate of .
Once again, there is a natural analogue of this notion for propositional questions, obtained by abstracting away from the actual values:
Abstraction: conditional knowability as interior operator Given a proposition and a propositional question (topology) , we say that is knowable given question (topology) at state , and write , if one can come to know that is true at after learning some (true feasible) answer to question ; i.e. if there exists some feasible answer such that . It is obvious that we have:
Equivalence between the two notions One can easily see that conditional knowability given an empirical variable is equivalent to conditional knowability given its associated propositional question :
Proposition 3.1.
The following are equivalent, for any variable and proposition :
-
1.
-
2.
.
Our notion of conditional knowability (of a proposition given a variable or question) can thus be seen as a variant of the well-known interior semantics for modal logic.
Special case: Knowledge as unconditional knowability When we take the empty set of variables , we obtain the above notion of (unconditional) knowledge :
3.3 Knowing the value of a variable
In a next step, we look at the various ways in which one can be said to know the value of an empirical variable.
Exact knowledge For a start, we say that a variable is exactly known, and write , if there exists a value such that the proposition is known, i.e. if holds for all states ; equivalently, iff is a singleton . So, holds iff is a constant map:
Approximate observations The act of observing a given variable at state within some given approximation can be modeled as restriction of the state space: we move from the original space to the subspace . All the variables are thus also restricted to , so we obtain where , , and is the subspace topology on .
Approximate knowledge For empirical variables, we also have a more inexact form of knowledge, namely approximate knowledge. Given any open set , we say that the value of is known with approximation if we have , that is, for all states .
Arbitrarily accurate knowledge We say that the value of is known with arbitrary accuracy at state , and write if: for every open neighborhood of , the value of is known with approximation ; i.e., we have that
Proposition 3.2.
-
1.
iff the singleton is dense w.r.t. the topology (i.e., ).
-
2.
Knowledge of arbitrarily accurate knowledge of is the same as exact knowledge of : i.e. we have .
-
3.
If is -separated, then arbitrarily accurate knowledge of is the same as exact knowledge of : i.e. we have .
3.4 Known dependence versus knowable dependence
The local version of (exact) dependence is not necessarily known, or even knowable: does not imply , nor it implies . Things change if we consider the notion of global functional dependence introduced above: using the universal modality , we can express the fact that holds globally via the identity
Global dependence is known dependence This follows directly from the interpretation of the universal modality as “knowledge” , which together with the above identity gives us
So captures a situation in which the existence of an exact dependence of on is known at .
But now we can also consider a virtual version of this:
Knowable dependence A knowable dependence of on holds at iff the existence of an (exact) dependence can be known if one is given some sufficiently accurate estimate of the value . This is captured by the expression
This holds at a state whenever holds on some open neighborhood .
However, an important observation is that (for inexact variables) both known dependence and knowable dependence may still be epistemically useless, as far as knowability of from is concerned. They do not automatically guarantee that any estimate of the value of (no matter how vague) is ever known after observing the value of with any accuracy (no matter how precise)!
What we need instead is a notion of epistemic dependence, i.e. one that ensures knowledge transfer: we should be able to infer the value of with any desired accuracy from a sufficiently accurate measurement of the value of . This forms the topic of the next section.
3.5 Epistemic dependence as continuous correlation
We now introduce the key notion of our paper: the concept of epistemic dependence between (inexact) empirical variables. This is not the same as known or knowable dependence: what we want is rather an information-carrying dependence: given two (sets of) empirical variables and , when can one be said to know how to find the value of (with any desired accuracy) given (a sufficiently accurate estimate of) the value of ? The answer will be given below by the notion of known epistemic dependence, to be written , which requires global continuity of the dependence map.
A related, but weaker notion is that of knowable epistemic dependence : this is the case in which a known epistemic dependence between and can be acquired after learning some (sufficiently accurate) estimate of . Topologically, this is a more local property, obtained by requiring continuity only over a neighborhood of the current value of . We proceed now to formally define these key concepts.
Known epistemic dependence We introduce now a global concept , obtained by adding the continuity requirement to the definition of (global) functional dependence:
To understand why continuity makes this global notion of dependence “epistemic” (in contrast to global exact dependence ), it is useful to provide a number of other useful equivalent formulations of this notion:
Proposition 3.3.
The following are equivalent for empirical variables and :
-
1.
-
2.
-
3.
-
4.
for all states and sets , if then
-
5.
is continuous (in the -topology on )
-
6.
the identity function is continuous, if we endow its domain with the -topology and its codomain with the -topology.
Essentially, this second and third clause say that, for every state , one can know the value of with any desired accuracy, after observing a sufficiently accurate estimate of the value of . Since this fact holds globally (for all states), it is known to the observing subject: so the meaning of is that the subject knows how to determine the value of with any desired degree of accuracy, if she was given accurate enough approximations of the value of .
By relaxing now this knowledge condition to knowability, we get a more “local” version of the same concept, obtained by restricting it to an open neighborhood of the actual state:
Epistemic dependence We write , and say that there exists a (knowable) epistemic dependence between and at state , if a known dependence can be achieved after observing some accurate enough approximation of the value (of variable at a state ). This happens when holds on the subspace (even if it does not hold on the whole original space ):
By unfolding this definition, we can easily see that we have: iff there exists , and a continuous map , s.t. holds on .
The next result gives us other useful characterizations of .
Proposition 3.4.
The following are equivalent for empirical variables and :
-
1.
-
2.
there exists an open neighborhood of , and a continuous map , s.t. holds on
-
3.
-
4.
there is some open -neighborhood of , s.t. for all states and sets , if then
-
5.
is continuous in the -topology on some -open neighborhood of
-
6.
the restriction of the identity function to some open -neighborhood is continuous, if we endow its domain with (the topology induced on by) the -topology and its codomain with the -topology.
So, unlike the local version of exact dependence , local epistemic dependence is inherently knowable: i.e. we always the validity
As in the case of exact dependence, it turns out that the local version of epistemic dependence is more fundamental than the global one: can define via the equivalence
but not the other way around.
3.6 A side issue: continuity at a point
There is in fact an even “more local” form of dependence , that requires only continuity at a point. We call this notion “conditional knowability of given ”. As we’ll see, this form of dependence is in general epistemically opaque. As such, it will not play any role in this paper, but it may still be useful to define it, in order to better understand our key notion of epistemic dependence : the two are closely related, but nevertheless subtly different in important ways.
Conditional knowability of variables as point-continuous dependence We write , and say that is conditionally knowable given at state if we have
i.e. if one can approximate the value(s) of with any desired accuracy if given a sufficiently accurate estimate of the value(s) of .
We can characterize conditional knowability in a similar way to the way we did for and :
Proposition 3.5.
The following are equivalent for empirical variables and :
-
1.
-
2.
-
3.
for all sets , if then
-
4.
is continuous at point in the -topology
-
5.
the identity function is continuous at point , if we endow its domain with the -topology and its codomain with the -topology
However, unlike and , conditional knowability is itself not necessarily knowable (based on observing ):
In other words, even if is actually knowable given at , this very fact may forever remain unknown: no matter how precise her measurements of , the agent may never be in a position to know this fact. The epistemic opacity of this form of dependence is due to its extreme sensitivity to small deviations or errors: if the value of happened to be even slightly different than the exact current value , then would no longer hold. As a result, any imprecision, however small, is enough to cast doubt upon conditional knowability.
Counterexample: Thomae’s function An extreme form of unknowable conditional dependence is given by Thomae’s function. Let and be two single variables, (the set of real numbers), with being the standard topology on , and we set to be the identity map, and be given by Thomae’s function:
This function is continuous at all irrational points, and discontinuous at all rational points.131313Note that , since by convention is the only natural number s.t. . As such, is never continuous on any open interval, and as a consequence, we have in this case that
is valid on the space . This is the extreme opposite of inherent knowability: in this space, whenever is true, then it is unknowable!
In fact, conditional knowability is only knowable (based on observing ) when we have a full-fledged epistemic dependence , as witnessed by the following equivalence:
In other words, the ‘knowable’ version of conditional knowability is exactly the epistemic dependence . For this reason, we consider to be a somewhat irrelevant notion from an epistemological point of view, and we will not explore it in any depth in this paper.141414Nevertheless, we will later specify sufficient conditions in which is inherently knowable (and thus equivalent to ): as we’ll see, such a ‘paradisiacal’ epistemic situation is guaranteed in a special kind of metric dependence models (“pseudo-locally Lipschitz models”).
4 The logic of continuous dependence
In this section we develop a formal language for an epistemic Logic of Continuous Dependence , that can express both (exact) functional dependence and (continuous) epistemic dependence. The language we will use includes the syntax of the Logic of Functional Dependence introduced in Section 3.1, but the semantics is topological, and the syntax is enriched with topological interior modalities (for ‘knowability’ of a proposition given an empirical variable ) and continuous-dependence atoms (for ‘epistemic dependence’ between variables and ). We provide a sound and complete proof system for reasoning about these forms of dependence, and we illustrate our setting with some examples.
4.1 Syntax and semantics
We assume given a (finite or infinite) set of basic variables , and a relational vocabulary consisting of a set of predicate symbols, together with an arity map , associating to each symbol a natural number . We denote by finite sets of variables in , and denote by finite tuples of variables.
Definition 4.1 (Syntax of ).
The logic of continuous dependence has a language defined recursively by the following clauses:
where is the arity of and is any -tuple of variables in .
Abbreviations Knowledge , knowable dependence , known dependence and exact knowledge are defined in this language as abbreviations:
It is easy to see that these abbreviations fit the semantic definitions of the corresponding operators given in previous sections, e.g. we have
Definition 4.2 (Topo-dependence models).
A typed topological model is a multi-typed structure , indexed by variables (each thought as having its own distinct type), where: for each , is a set, giving the range of values of variable ; is a topology on ; and is an interpretation function, mapping each predicate symbol of arity into an -ary relation on the union .
A topological dependence model (‘topo-dependence model’ for short) is a structure , consisting of: a typed topological model ; a set of abstract states; and, for each variable , a corresponding empirical variable, i.e. a surjective map .
For every set of variables, stands for the single joint empirical variable associated to the set , as defined in the preceding section: for all . We also use all the associated notation introduced in the previous section: in particular, for every , we consider the -topology on , given by , and the -interior (defined as the interior operator in the -topology).
Definition 4.3 (Semantics of ).
Truth of a formula in a topo-dependence model at a state (written , where we drop the index when the model is understood) is defined as in for the atoms, as well as for all the operators of , and in addition by the following clauses:
The paradigmatic examples in topology are metric spaces, which give us our paradigmatic type of topo-dependence models:
Special case: metric models A metric dependence model (‘metric model’, for short) is a topo-dependence model , in which each of the topologies is given by a metric on . The underlying typed metric model comes with designated metrics instead of topologies, but each of them induces of course a topology having the family of open -balls as its basis. For joint empirical variables given by finite sets of variables , the induced (product) topology on is also metric, and is easily seen to be generated by open balls wrt the (the restriction to of) the so-called Chebyshev distance (also known as the supremum metric, or metric):151515 This metric is uniformly equivalent with the more standard Euclidean metric on the product space.
Note that, for (finite) non-empty sets of variables , this amounts to taking the maximum of all distances
while for , recall that where is the empty string, so that we have that
The corresponding (weak) -topologies induced on the state set are not necessarily metric, but they are pseudo-metric, being generated by open balls of the form
with , and where the pseudo-metric on is given by setting:
Note that as a result, coincides with the supremum pseudo-metric induced by single-variable pseudo-distances:
With these notations, it is easy to see that in a metric model our topological semantics amounts to the following:
In many applications, it is useful to think of the states employed so far as being ‘concrete’, i.e., represented by means of tuples of values for each of the fundamental variables; in other words, assignments of values to variables:
Special case: concrete models A concrete topo-dependence model is a structure , consisting of: a typed topological model ; and a set of ‘concrete’ states, i.e. type-respecting assignments of values to variables. This structure is subject to the additional requirement that for every .161616Once again, this condition is innocuous (we can always restrict the codomain to the actual range of values taken by ), and is just meant to enforce the surjectivity of the corresponding empirical variables. A concrete topo-dependence model is indeed a special case of a topo-dependence model: we can associate to each variable an empirical variable , given by .
Example: Euclidean models An example of topo-dependence models that are both metric and concrete are Euclidean models. For a finite set , a Euclidean model is simply given by a subset of the Euclidean space of dimension , consisting of assignments of real values to variables . The metric on each copy of is the standard Euclidean distance , and so the topology is the subspace topology induced on by the standard Euclidean topology on .
4.2 The proof system
We are now prepared to present our axiomatic proof system for the Logic of Continuous Dependence. The axioms and rules are given in Table 2. The system includes, as group (I) in the Table, the axioms and rules of the system for the Logic of Functional Dependence, as already listed in Table 1. The additional axioms and rules are divided into three further groups: (II) Axioms for propositional knowability, (III) Axioms for knowable (epistemic) dependence, and (IV) Connecting Axioms (that connect the epistemic/inexact notions with the corresponding exact notions).
Note the analogy of the axioms in groups (II) and (III) of Table 2 with the similar axioms in groups (II) and (II) of Table 1 (which are of course also included in , within group (I) of Table 2). This is to be expected, since epistemic dependence is in a sense the “feasible” generalization of exact dependence to inexact variables; mathematically speaking, is the topological analogue of . But note first that not all the have analogues for epistemic dependence: axiom (5) for has no analogue for , and the same applies to the axiom of Determined Atoms; and second, that even in the case of the analogue axioms which do hold for inexact dependence, their meaning is different in the topological setting. We discuss this shift in some detail.
(I) | Axioms and rules of |
(II) | Axioms for Knowability: |
(-Necessitation) | From , infer |
(-Distribution) | |
(Veracity) | |
(Positive Introspection) | |
(III) | Axioms for Knowable Dependence: |
(-Inclusion) | , provided that |
(-Additivity) | |
(-Transitivity) | |
(Knowability of Epistemic Dependence) | |
(Knowability Transfer) | |
(IV) | Connecting Axioms: |
(Knowable Determination) | |
(Knowable Dependence) | |
(Knowledge of Necessity) | |
(Knowledge of Constants) |
What the axioms mean Mathematically, the axioms for in Group II capture the main properties of the interior operator, as given by the Frechet axioms of topology. In addition, Veracity asserts that knowable facts are true.171717This axiom is listed here only for expository reasons, since is in fact derivable from the axiom of Knowable Dependence, together with the axiom of Factivity. Similarly, one can easily see that the old rule of -Necessitation is now derivable in from -Necessitation together with Knowable Dependence.
The Axioms of Knowable Dependence in Group III are similar to the corresponding axioms for exact dependence, and they are familiar from Database Theory, where they are known as the Armstrong axioms of dependence. Inclusion expresses “epistemic superiority”: (the approximate answers to) a larger set of questions carry all the information (and more) that is carried by (the approximate answers to) a subset of those questions. Additivity says that, if (the inexact answers to) two sets of questions are knowable then (the inexact answers to) all the questions in their union are knowable. Transitivity captures a version of Dretske’s Xerox Principle [Dretske, 1983]: if carries all the information about , and carries all the information about , them carries all the information about .
Mathematically, these Axioms of Knowable Dependence capture the main properties of the category of topological spaces, with product space as a categorical product: the Inclusion axiom holds because of the continuity of the projection maps for (where recall that is a subspace of with the product topology); the Additivity axiom captures the universality property of the product, saying that a pair of continuous functions and on two opens gives rise to a continuous function into the product space, given by ; and Transitivity captures the closure of continuous functions under composition. Next, the axiom of Knowability of Epistemic Dependence expresses the fact that is ‘topologically local’ (-it holds at a point only if it holds on a whole open neighborhood of that point), and that it is stronger, in general, than simple functional dependence. Epistemically, this says that epistemic dependence is indeed a knowable dependence: whenever it holds, one can come to know it (after observing some good enough approximation of ). Going further, the Knowability Transfer axiom captures the continuity of dependence: if is continuous, then the inverse of any open subset of its domain is open. Epistemically: if is knowable given , then any proposition that is knowable given is also knowable given .
Finally, the Connection Axioms in Group IV spell out the relationship between epistemic (inexact) dependence and knowability and their exact analogues in . Knowable Determination says that knowability implies determination: if a statement is knowable based on some approximation of the value of , then the truth of that statement is determined by the (exact) value of . Knowable Dependence is the analogue claim for empirical variables: if is epistemically dependent on , then the exact value of could be determined of one was given the exact value of . Mathematically, this just follows from the fact that a continuous dependence is a (functional) dependence. The last two Connection Axioms tell us that the converses of these statements hold (only) in the special case when is the empty set of variables: mathematically, this is because is by definition the discrete topology (so that is the global quantifier on , while simply means that is a constant). Epistemically, Knowledge of Necessity says that, if a statement is necessary (true in all epistemically possible worlds), then it is known. Similarly, Knowledge of Constants says that, if a constant (having the same value in all epistemically possible worlds), then its value is known.
Theorem 4.4.
The proof system in Table 1 is a sound and complete axiomatization of the logic of continuous dependence on any of the following classes of models: (a) arbitrary topo-dependence models; (b) metric dependence models; (c) concrete topo-dependence models; (d) pseudo-locally Lipschitz metric dependence models. Moreover, the logic is decidable.
Proof.
Proofs for these assertions are found in the Appendix to this paper. ∎
Remark 4.5 (A first-order perspective).
Why do we succeed in axiomatizing the logic of topological dependence? It is well-known that many modal logics, including the basic dependence logic , admit a faithful effective translation into the language of first-order logic. Thus, in principle, these logics are completely axiomatizable, and other properties follow as well. For our topological semantics, an obvious translation would use a three-sorted first-order language, with sorts for states, values of variables, and open sets. However, the standard requirement on topological spaces that opens be closed under arbitrary unions is not first-order. But then, in our motivation for topological models, we thought of open sets as outcomes of possible measurements. Usually not all open sets qualify for this. For instance, in the reals, open intervals are just a base for the topology: closed under finite intersections, but not under arbitrary unions. If we think of our second sort as an open base for the topology, requirements remain first-order expressible. Moreover, it is easy to add explicit first-order descriptions for the behavior of variables viewed as names of functions, and as a result, at least in principle, we are still in a first-order setting that predicts axiomatizability in general for the systems of reasoning investigated in this paper. Of course, to find explicit complete logics, we still have to do real work.
Note that the point-continuity atom introduced in Section 3.6 (capturing the epistemically opaque notion of “conditional knowability of given ”) is not a part of the syntax of . And indeed, we can use part (d) of Theorem 4.4 to show that:
Proposition 4.6.
Conditional knowability is not expressible in the language of . As a consequence, the language based only on the operators and conditional knowability atoms (i.e. the language obtained by replacing in the local continuity atoms by point-continuity atoms ) is more expressive than .181818The fact that is at least as expressive as follows already from the fact that is definable in (as ).
Proof.
If were definable in , then the formula would be expressible in . This formula is obviously satisfiable: just take the Counterexample constructed in Section 3.6 (involving Thomae’s function). By the soundness of the proof system , this formula must then be consistent with the axioms and rules of this proof system. But by part (d) of Theorem 4.4, the formula must be satisfiable in a pseudo-locally Lipschitz models: this is a contradiction (as pseudo-locally Lipschitz models validate the implication , thus contradicting our formula).∎
This result suggests an obvious question:
Open problem What is the complete logic of the language based only on the operators and conditional knowability atoms ? Is that logic decidable?
4.3 A concrete example
After all these abstract notions, some simple concrete illustration may be helpful.
Example 4.7 (Car speed detection).
An aircraft police officer determines a car’s velocity , by measuring the time it takes the car to pass between two highway markings, say 1 km apart. An abstract topo-dependence model for this situation has a set of possible worlds or ‘states’, as well as two variables , whose common range comes the standard Euclidean topology .191919We assume that it is known that the car is already in motion, so we exclude the case . We could also consider a concrete model for the same situation: the set of possible states consists then of possible assignments for the basic variables , with , . A basis of observable properties consists of the open intervals , with rational endpoints. The variables stand in a (continuous) dependence relation, for all states :
Assuming that the legal speed limit is km per hour, there is a unary predicate (‘speeding’) denoting . In terms of ontic dependence, the exact value of the speed carries the information on whether the car is speeding or not:
Since the speed functionally depends on the time, we also have the (global) dependence:
Putting these together (and using the Transfer Axiom), we see that the models also validates:
In other words: the exact value of the time (needed to pass between the two markings) carries the information on whether the car is speeding or not.
By itself, this does not make the police officer know that the car is speeding. But as the speeding property is an open set, the officer can come to know that the car is speeding (if this is indeed the case):
So the fact that the car is speeding is knowable: in principle, the officer can learn this by performing an accurate enough measurement of the speed . However, the velocity will typically not be directly available to him for measurement. Luckily though, the functional dependence between speed and time is continuous, so we have the (global, and therefore known) epistemic dependence:
Once again, by putting the last two statements together, and using this time the Knowability Transfer axiom, we obtain:
In other words: by doing an accurate enough measurement of the time (needed to pass between the two markings), the policeman can come to know that the car is speeding.
In contrast, the police may never get to know that the car is not speeding, since the complement of is not an open set: the implication
is not valid in the above model, and neither is the time-dependent knowability version
Of course, this epistemic difficulty only arises when the car is exactly at the speed limit : in this case, the car is not speeding, but the policemen will never be sure of this, no matter the accuracy of his measurements. On the other hand, is the only counterexample in this case: since the interior , every state with will satisfy the implication (and thus also the implication ). Hence, if the speed is not exactly 120, the policeman can eventually come to know whether the car is speeding or not (assuming there is no absolute limit to the accuracy of his measurements or perception).
There are also further statistical aspects to this practical scenario, e.g. with aggregating results of repeated measurements, but these are beyond the scope of this paper.
5 Epistemic Independence
Known dependence versus epistemic dependence Recall the exact dependence operators and of the logic , as well as the associated ‘epistemic’ abbreviations
(both equivalent to the corresponding notions defined in ), and the ‘global’ dependence
which captures a form of known dependence: it is known that the exact value of determines uniquely the exact value of . Let us now draw some comparisons.
It is easy to see that our notion of epistemic dependence implies the existence of a knowable exact dependence, as shown by the following validities:
But the converse implications fail: epistemic dependence is stronger than knowable dependence , and known global epistemic dependence is stronger than known global dependence . The first notion requires as a surplus that good enough approximations of are enough to give any desired estimate of . Topologically, the distinction shows in the existence of non-continuous dependence maps.
In fact, even more extreme cases are possible: the exact dependence might be known, while at the same time it is known that there is no knowable epistemic dependence. This situation is topologically characterized by the following result.
Proposition 5.1.
The following are equivalent in topo-dependence models :
-
1.
holds in (at any/all states)
-
2.
there exists some map s.t. and has a dense set of discontinuities (i.e., ).
There is nevertheless one type of variables for which known/knowable exact dependencies are equivalent to their epistemic counterparts. A variable is called exact if its value topology is discrete (i.e. ).
Proposition 5.2.
For exact variables , the following implications are valid:
Complete ignorance as topological independence Going further with the above discrepancies, we now move to even more extreme situations where, while globally determines , it is known that no observable estimate of will give any information about ! The dual opposite of epistemic dependence is the case when no observable approximation of the value of can give any information concerning the value of . We refer to this notion as epistemic (or ‘topological’) independence, and denote it by (from ‘ignorance’).
The notion is not a simple negation , but a much stronger concept, capturing a type of zero-knowledge situation: all is completely uninformative as far as is concerned.
This is to be distinguished from simple ontic independence between the exact values in the sense of the original dependence logic , given by
Again we draw some comparisons. For a start, both notions have a global counterpart:
The relationships between these notions are given by the following implications:
In particular then, epistemic independence is weaker than ontic independence! Moreover, as in the case of probabilistic independence, both global versions are symmetric, i.e. we have:
The most interesting conceptual observation is that we can have full (known) exact dependence while at the same time having full (known) epistemic independence.
Proposition 5.3.
The following are equivalent for topo-dependence models :
-
1.
holds in (at any/all states)
-
2.
there exists some everywhere-surjective map s.t. .
Here, we used the following mathematical notion from Analysis: is everywhere-surjective iff we have for all non-empty open sets . Everywhere-surjectivity implies everywhere-discontinuity (hence also the above-mentioned density of the set of discontinuities), but it is a much stronger condition.
Example 5.4.
Each everywhere-surjective function yields an example of known exact dependence with (knowledge of) epistemic independence. A simple example is the Dirichlet function: is the set of real numbers with the standard topology, is the set with the discrete topology (which is the same as the subspace topology induced by the standard topology), with iff is rational, and otherwise. More interesting examples are the ones in which the domain and codomain of are the same (i.e., is the common range of both variables), preferably a nice space. See [Bernardi and Rainaldi, 2018] for many examples, where the common range is , or other interesting spaces.
Example 5.5 (Pythagorean drivers).
Unlearnability in the sense of, say, the Dirichlet function may be rare, though in our earlier car speeding example, one could think of a Platonic police officer trying to book a Pythagorean driver who dematerializes at any irrational value of .
Unlearnability is related to the behavior of chaotic dynamical systems, [Lorenz, 1995], where predictions of future behavior may be impossible. However, we must leave this interface of Epistemic Topology and mathematics to another occasion.
Instead, we end with a technical logical issue. It is known that the joint logic of ontic independence and ontic dependence is undecidable, [Baltag and van Benthem, 2021], but topological indepenence had its own behavior. This suggests the following question about the purely topological component of our logic:
Open problem Is the logic of topological independence and dependence decidable?
6 Uniform dependence: a stronger notion of knowability
Up till now, we identified the approximations of the current value of variable at state with open neighborhoods . In this sense, our global continuous dependence captures known dependence, both in the sense of knowing that/whether and in the sense of knowing how: for any desired estimate , the agent knows how to determine that if given a sufficiently good estimate of . This is full how-to-knowledge: in fact, the agent knows how to find the weakest appropriate estimate that will determine whether or not.
But the topological notion of estimation is local: there is no way to compare the accuracies of estimates of different values and in different states. Things change radically if we introduce a global notion of accuracy or error , as e.g. the one given by real-numbered open intervals of a given length, or more generally by open balls in a metric space. In such a setting, full how-to knowledge of a dependence would require that: for any given desired accuracy in determining the value of , the agent knows how to find an appropriate accuracy , such that an estimate of with accuracy (in any state ) will yield an estimate of with accuracy (in the same state ). Essentially, this stronger form of (global) epistemic dependency requires uniform continuity of the underlying dependence map.
6.1 Uniform dependence in metric spaces
The notion of uniform dependence takes us beyond topology: its semantics requires the move to metric dependence models.
Empirical variables over metric spaces As already noticed in Section 4, one may consider as a special case empirical variables of the form , whose range of values has a metric topology induced by a metric on . From now we will restrict ourselves to such “metric variables”. Closeness relations of the form will then give us global notions of accuracy for the values of : margins of error for measurements (or more generally, for observations) of the value of .
Sets of variables as joint variables As we already saw in Section 4 (when giving the semantics of on metric dependence models), a finite set of empirical variables over metric spaces can itself be regarded as a single metric variable. More precisely, given such a finite set of metric variables , each coming with its own metric space, we can associate to it a single metric variable, also denoted by , whose set of values is as usual , while the metric is (the restriction to of) the so-called Chebyshev distance (also known as the supremum metric):
Strong epistemic dependence We say that there is a strong (or ‘uniform’) epistemic dependence between empirical variables and , and write , if for every margin of error for -measurements there exists some margin of error for -measurements, such that every estimate of with accuracy entails an estimate of with accuracy :
In contrast, if we apply the definition of known epistemic dependence in the metric topology, and unfold the definition in terms of the underlying accuracies, we obtain:
So the difference between known epistemic dependence and strong epistemic dependence is the position of the universal state quantifier (before or after the existential accuracy quantifier ), similarly to the analogue difference between continuity and uniform continuity. This analogy is not accidental, witness the following result in the style of earlier characterizations:
Proposition 6.1.
Given two empirical variables and , the following are equivalent:
-
1.
-
2.
there exists a uniformly continuous map s.t. holds on
-
3.
is uniformly continuous (wrt the -topology on induced by the pseudo-metric )
-
4.
the identity function is uniformly continuous (wrt to the -topology given by on its domain and the -topology given by on its codomain).
Note that strong epistemic dependence is a global notion. We can also introduce a topologically local notion of locally strong epistemic dependence:
Once again, if we denote by the topology induced by the metric , this is equivalent to:
Proposition 6.2.
The following are equivalent:
-
1.
-
2.
there exists an open neighborhood of , and also a uniformly continuous map s.t. holds on
-
3.
is locally uniformly continuous around
-
4.
the identity function is locally uniformly continuous around .
Moreover, in analogy to the case of (simple) epistemic dependence, strong epistemic dependence is inherently known, while locally strong epistemic dependence is inherently knowable:
However, there are some significant differences with our earlier topological notions. For both simple and epistemic dependence, the global versions are equivalent to known local ones:
Knowing a dependence (between and ) is the same as knowing that you could know the dependence (if given enough info on ). However, this is not the case for strong epistemic dependence in our new sense of uniform continuity:
The explanation is that knowing how to find from (with any desired accuracy) is not the same as knowing that you could know how to do it, if given enough info on . The second notion is in general much weaker! We can provide counterexample to the equivalence of and by taking a fresh look at our car speeding scenario:
Example 6.3 (Car speeding revisited).
A priori, the police officer has a known epistemic dependence , but not a strong one: is false! For any speed estimate , the officer can find a such that after measuring time with accuracy , (s)he will know whether the velocity is in interval . But, given a desired accuracy for the speed (with no further information on the interval), the officer cannot know in advance what accuracy is needed in measuring time to determine velocity within . This is because, given a fixed , there is no s.t., for all :
However, is strongly knowable from in the sense of a locally strong dependence: in fact, holds globally, so this strong dependence is known:
Indeed, after performing just one reasonably accurate measurement of time (with ), the officer will know, for any desired velocity accuracy , how to determine the needed time accuracy ; i.e. one s.t. the following will hold for all :
This finishes our counterexample, but there are more interesting things going on in our car-speeding scenario: note that in this example both and hold globally, so the two notions are actually equivalent on this model, i.e. we have
Of course, the left-to-right implication always holds, but the converse gives us a kind of “epistemic bootstrapping”: when the value space we are working in is conducive to epistemic inquiry, epistemic dependence automatically gives us strong (uniform knowability).
We now proceed to generalize this last observation.
Important special case: locally compact spaces When the underlying spaces are locally compact (i.e. every value in has a compact neighborhood), epistemic dependence implies locally strong dependence: the formula
holds on locally compact spaces. In contrast, global (known) epistemic dependence still does not imply strong epistemic dependence: even on locally compact spaces, we still have that
Of course, the global implication will hold on fully compact spaces, but those are less pervasive, being specific to very circumscribed situation: in particular, our Euclidean space is not compact, though it is locally compact.
Interpretation: bootstrapping knowability Since Euclidean spaces are locally compact, the natural topology of our space is arguably epistemically fertile: fit to ‘bootstrap knowability’. Every epistemic dependence between Euclidean variables and is a locally strong dependence. Indeed, if such a dependence is knowable (i.e., if holds between Euclidean variables), then it is also knowable that (given enough information about ) you could come to know how to find from with any desired accuracy. Since Euclidean variables are the ones most often encountered in empirical science, one could say that Nature makes us a free gift: it is enough to gain knowledge of an epistemic dependence to obtain potential ‘how-to knowability’, and thus, if you wish, pass from science to engineering.
Remark 6.4 (Agents and environments).
These observations have a more general epistemological import. Epistemic notions may ‘upgrade’ automatically when the learning environment is favorable. What this highlights is that epistemic success involves an interplay of two parties: the nature of the knowing agents and of the environments (adversarial or helpful) they operate in, cf. also [Barwise and Perry, 1983]. This point transcends our technical setting: in a sense, all epistemology is about the balance of the structure of agents and the world they live in.
The next class of models is a example of an even more favorable type of environment, that facilitates a kind of ‘epistemic super-bootstrapping’:
A stronger form of epistemic bootstrapping: pseudo-locally Lipschitz models A metric dependence model is called pseudo-locally Lipschitz if every basic empirical variable is pseudo-locally Lipschitz wrt to every other basic variable ; i.e.: for any two basic variables , the map is pseudo-locally Lipschitz. It is easy to see that this is equivalent to requiring that the identity map is pseudo-locally Lipschitz for all non-empty sets of variables . As a consequence, such models afford an even stronger form of epistemic bootstrapping:
Every pseudo-locally Lipschitz model validates the implication , for all . So in such models, our three ‘localized’ forms of continuous dependence (point-continuous dependence , locally-continuous dependence and locally uniformly-continuous dependence ) are all equivalent, for all .
Remark 6.5 (’Paradisiacal’ environments versus our world).
Pseudo-locally Lipschitz models describe a kind of “paradisiacal” epistemic situation, in which the weakest and most fragile form of dependence (conditional knowability , that typically is epistemically opaque) becomes in fact transparent, being bootstrapped all the way to the strongest form of know-how dependence (). Unfortunately, while our Euclidean space is compact, typical Euclidean variables encountered in empirical science are not usually pseudo-locally Lipschitz with respect to each other. In this sense, although our world is epistemically fertile, it is not paradisiacal!
6.2 The logic of uniform dependence
We proceed to extend the earlier language of to capture the properties of uniform dependence. We start with a very simple extension: just add uniform dependence atoms . The resulting logical system is a straightforward extension of .
Definition 6.6 (Syntax of ).
Given a set of predicates and a set of variables , the Logic of Uniform Dependence () has a language given by adding uniform dependence atoms to the language of ; in other words, the set of formulas is recursively given by:
where are finite sets of variables, is a predicate and is a string of variables of the same length as the arity of .
Definition 6.7 (Semantics of ).
Given a metric dependence model over some typed metric model , we define the satisfaction relation by using the usual recursive clauses for atomic formulas and the operators (using the metric topologies on ), and interpreting the uniform dependence atoms in the obvious way:
where, as in Section 4, we use
to denote the pseudo-metric induced on the state space by the Chebyshev distance on .
Theorem 6.8.
The proof system in Table 3 is a sound and complete axiomatization of the Logic of Uniform Dependence on metric dependence models (as well as on concrete metric models). The same proof system is also sound and complete with respect to pseudo-locally Lipschitz models. Moreover, the logic is decidable.
The completeness proof is deferred to the Appendix. Essentially, it is based on refining the model construction in the completeness proof for to obtain a pseudo-metric model, whose associated metric dependence model happens to be pseudo-locally Lipschitz.
(I) | All axioms and rules of the system |
(II) | Axioms for uniform dependence : |
(-Inclusion) | , provided that |
(-Additivity) | |
(-Transitivity) | |
(Uniform Dependence is Known) | |
(Uniformity implies Continuity) | |
(Uniformity of Knowledge) |
Note again the analogy of the axioms in group (II) of Table 3 with some of the axioms in groups (III) and (IV) of Table 2 (which are of course also included in , within group (I) of Table 3). And indeed, if we replace by in the above axioms, we obtain valid theorems of . Once again, this is to be expected, since uniform dependence is a strengthening of epistemic dependence, in the same sense in which epistemic dependence was a strengthening of exact dependence. But note that more properties are lost in the transition from to , in comparison to the earlier transition from to . There is e.g. no analogue of the Transfer axiom for uniform dependence, since does not come with an accompanying modality (in contrast to and , which come together with and respectively ). The reason is that Boolean variables have a discrete range of truth values, so there is no sense in ‘uniformizing’ the meaning of .202020Things would be different if we moved to a multi-valued logic with a continuum set of values: one could then talk about “uniform knowability” of a proposition .
Another difference is that, unlike the case of exact dependence and epistemic dependence (where we took the local versions and as primitive notions in our syntax), in we chose to take the global version as basic, and indeed we did not even include the local version in our syntax. One of the reasons is that, as we already mentioned, cannot define in any obvious way (unlike the case of exact dependence and epistemic dependence); and since we are in the end mainly interested in (global) uniformity, we must take as primitive.
Nevertheless, this limitation suggests extending our language of with local atoms , obtaining an extended language . The following result shows that this move does increase expressivity:
Proposition 6.9.
Local uniform dependence is not expressible in the language of . So the language of both local and global uniform dependence (obtained by adding local atoms to ) is more expressive than the language of .
Proof.
The proof is completely similar to the corresponding inexpressivity result for (Proposition 4.6), involving instead the formula . This formula is obviously satisfiable on metric dependence models (just take any example in which is mapped into by some function that is locally continuous around some point, but not locally uniformly continuous around it). By the soundness of the proof system , this formula must then be consistent with the axioms and rules of this proof system. By the last part of Theorem 6.8 (completeness of wrt pseudo-locally Lipschitz models), if were expressible in , then the formula would be satisfiable in a pseudo-locally Lipschitz models. But this is a contradiction, as pseudo-locally Lipschitz models validate the implication , thus contradicting our formula.∎
Remark 6.10.
In themselves, the inexpressivity results claimed in Propositions 4.6 and 6.9 are not surprising: there was no reason to expect that the missing notions ( and respectively ) were expressible in languages ( and respectively ) that did not explicitly include them. But such results on expressive limitations are often hard to prove, involving intricate counterexamples. So it comes as a pleasant surprise that in these two cases, the expressivity-limitation results simply follow from the special additional features of the model constructed in the completeness proof!
Furthermore, Proposition 6.9 leads us to yet another obvious question:
Open problem What is the complete logic of the language of both local and global uniform dependence? Is that logic decidable?
7 Directions for future work
Given the analysis presented here, many natural follow-up topics arise, of which we briefly list a few.
Further system issues The systems introduced in this paper raise many further technical questions. One immediate issue concerns definability. As we have noted, performs a double epistemization of existing modal dependence logics. First we added topological modalities for knowability based on measuring values of variables , and after that, we also introduced continuous dependence . Is the latter step necessary, or more precisely, is definable in the logic extended only with the topological interior modalities? We believe that the answer is negative, but we have not pursued the definability theory of our topological languages. Other natural open problems concern axiomatization.
Another immediate open problem is providing a complete axiomatization of the topological logic of conditional knowability based on the operators and the point-continuity atoms for conditional knowability . As we mentioned, this language is strictly more expressive than . But our methods for proving completeness and decidability do not seem to work for this extended logic. The reason is that, as noted earlier, is an ‘unstable’ property: it is very sensitive to any small changes of values. This sensitivity gives rise to technical difficulties. Is this logic decidable, or at least axiomatizable?
Other open problems that we noted were axiomatizing the logic of topological independence, as well as finding an axiomatization of the logic of both local and global uniform dependence.
A final set of questions concerns computability. For several logics in this paper, we do not know if they are decidable, and we know for none of our decidable logics what is its exact computational complexity.
Richer languages for metric spaces
While the language of is a good abstract vehicle for dependence in topological spaces in general, even the extended logic of uniformly continuous dependence seems poor in expressive power over the rich structure of metric spaces. One extension adds explicit accuracy variables and constants to the language, with corresponding modalities. One can then talk about -closeness, compute with margins of error, and determine the complete modal logic for explicit versions of continuity and uniform continuity.212121This setting covers Margin-of-Error Principles for knowledge that have been widely discussed in the philosophical literature, cf. [Baltag and van Benthem, 2020] for a logical analysis.
Uniform spaces
There is also a qualitative approach to the epistemic surplus structure in metric spaces by using so-called uniform spaces, [Isbell, 1964]. Here a family of reflexive symmetric ‘closeness relations’ is given on the topologized state space, closed under sequential compositions representing combined refinement. We can now define continuity and uniform continuity in terms of closeness intuitions (close arguments should yield close values), and study dynamic modalities for the effects of closeness refinement. We have a logical formalism for this setting and a plausible sound axiomatization, but proving completeness has so far eluded us.
Computable dependence as Scott-continuity
While uniform continuity strengthens knowable dependence in terms of state-independent approximations, another strengthenings would make knowability a form of computability. In this interpretation, the exact value of a variable might be the limit of an infinite process of computation. The computable approximations can then be understood as approximate values, living in the same domain as the exact value (rather than as open neighborhoods of the exact value), corresponding to partial results obtainable at finite stages of the computation. A natural semantic setting for this interpretation are Scott domains, and Domain Theory [Abramsky and Jung, 1995] fits within our topological framework, when we use the Scott topology. Again this allows us to use relational models in which the given topology does not match the modal semantics but the computational convergence given by Scott topology. Computability (to any desired degree of approximation) of a variable from a variable then amounts to existence of a Scott-continuous dependence function between them. We have a first completeness result for a logic of Scott-continuous dependence which extends the logic with an axiom reflecting the special structure of domains..222222Domain Theory is an elegant abstract approach to computability, but it does not contain actual manipulation with code. For that, we might have to provide a logical analysis in our style for Recursive Analysis, [Goodstein, 1961], getting closer to the syntax of dependence functions as laws that we can compute with.
We plan to explore these issues in a forthcoming paper [Baltag and van Benthem, 2024b]. The next topics we list here concern more drastic extensions of our framework.
Point-free topology
In the approach of this paper, dependence in empirical settings assumes the original set-based functional dependence and adds extra conditions of continuity. However, the very spirit of approximation might seem to make the use of underlying points debatable. One could also work in a point-free topology, [Vickers, 1996], where there are only opens with some suitable (lattice) structure, and points only arise through representation theorems. Then, the requirement of continuity has to be replaced with conditions on maps from open approximations for values to open approximations for arguments. Again, our current topo-dependence models might then arise only in the limit as the result of some representation construction. For some first thoughts on this inn a category-theoretic perspective, see [Ye, 2022].
Learning dependence functions
Learning the actual state of the world, the paradigmatic issue in this paper, is a task when relevant dependencies exist, and are known in an informative manner. But in science, we also want to learn the regularities themselves. One way to go here is ‘lifting’ our setting of single dependence models to families of these, as in the dependence universes introduced in [Baltag and van Benthem, 2021], where we may not know which precise dependencies govern our actual world. In this lifted setting, there is now a richer repertoire of relevant update actions: one can perform measurements, but one might also learn about regularities through mathematical reasoning or in other ways.
Dynamical systems
Much of science is about dynamical systems transitioning to new states over time. While our logics can include temporal variables denoting points in time on a par with other variables, there is also a case for enriching our dependence logics with temporal operators describing the future and past of system evolution where the universe of states has a global stat transition function. What this would require is a topological extension of the dependence logic for dynamical systems in [Baltag and van Benthem, 2024a], which would link up also with the more abstract temporal logic of topological dynamical systems of [Kremer and Mints, 2007]
Probabilistic dependence and statistical learning
The topological view of opens as results of measurements pursued in this paper says little about how measurements are combined in scientific practice. A major challenge emerges here: how should one interface our approach with the use of statistical techniques in Measurement Theory?
8 Conclusion
This paper has presented an extensive conceptual analysis of dependence in topological models for empirical inquiry. We gave new formal languages incorporating our main notions, and proved representation, completeness and decidability results for the resulting logics of continuous and uniformly continuous dependence.
These offerings can be viewed in several ways. First, we extended the area of Epistemic Topology with notions and systems that we believe to be of philosophical interest. We believe that our logics sit at the intersection of several epistemological perspectives. Our introduction of dependence merges two traditions to information and knowledge that have often been considered separate or even incompatible: Epistemic Logic and Situation Theory. Also, our two-step topologization of dependence logic is reminiscent of the move from classical to constructive systems like Intuitionistic Logic, where open sets replace arbitrary sets, and where, equally crucially, continuous functions replace arbitrary functions. In addition, one can see our systems as a further step toward a general logic underneath Formal Learning Theory. Finally, while these are all interfaces with formal epistemology, we believe that our questions-based perspective also links up with General Epistemology, and it might be very interesting, for instance, to see what the moves to continuous functions and even to uniformly continuous functions mean in a more informal common sense setting.
At the same time, our technical results also enrich the logical study of mathematical theories, such as topological semantics for modal logics, [van Benthem and Bezhanishvili, 2007]. The system is a multi-index topological modal logic which can also talk about continuous dependencies between variables. This suggests extended dependence versions of classical results in the area like the Tarski-McKinsey Theorem for completeness over standard metric spaces, [McKinsey and Tarski, 1944]. The models constructed in our completeness proof do have logic-induced metric structure, but it remains to be seen if completeness holds wrt the standard Euclidean metric. But also new types of modal correspondence results arise. For instance, the epistemic desideratum that knowledge-that of propositions should imply uniform know-how for inquiry corresponds, in a precise modal sense, with a restriction to (locally) compact classes of metric spaces. Other connections of this technical sort have been identified at earlier points in the paper, such as interfaces with Domain Theory and with Topological Dynamic Logic.
Thus, Epistemic Topology, as pursued in the style of this paper, is both Epistemology endowed with topological tools and Topology/Analysis enriched with epistemological perspectives.
Acknowledgments We thank the constructive audiences at many venues in Amsterdam, Pittsburgh, Paris, Beijing and Stanford where these ideas or some of their precursors have been presented since 2013. In particular, we thank Adam Bjorndahl, Konstantin Genin, Valentin Goranko, Kevin Kelly, Dazhu Li, J. Väänänen, Fan Yang and Lingyuan Ye for their helpful feedback.
References
- [Abramsky and Jung, 1995] Abramsky, S. and Jung, A. (1995). Domain Theory. Departments of Computer Science, University of Birmingham and Oxford University.
- [Baltag et al., 2019] Baltag, A., Gierasimczuk, N., and Smets, S. (2019). Truth-tracking by belief revision. Studia Logica, 107:917 – 947.
- [Baltag and Renne, 2016] Baltag, A. and Renne, B. (2016). Dynamic epistemic logic. Stanford Encyclopedia of Philosophy, https://plato.stanford.edu/.
- [Baltag and Smets, 2020] Baltag, A. and Smets, S. (2020). Learning what others know. In Kovacs, L. and Albert, E., editors, Proceedings of LPAR ’23, volume 73 of EPiC Series in Computing, pages 90–100.
- [Baltag and van Benthem, 2020] Baltag, A. and van Benthem, J. (2020). Some thoughts on the logic of imprecise measurement. In Ying, X., editor, Xuebufendongxi: Essays in Tsinghua Philosophy, pages 329 – 364. Tsinghua University Press.
- [Baltag and van Benthem, 2021] Baltag, A. and van Benthem, J. (2021). A simple logic of functional dependence. J. Phil. Log., 50:939–1005.
- [Baltag and van Benthem, 2024a] Baltag, A. and van Benthem, J. (2024a). Dependence logics in temporal settings.
- [Baltag and van Benthem, 2024b] Baltag, A. and van Benthem, J. (2024b). Topological dependence, approximation dynamics, and domain theory. Working paper, ILLC, University of Amsterdam.
- [Barwise and Perry, 1983] Barwise, J. and Perry, J. (1983). Situations and Attitudes. The MIT Press, Cambridge MA.
- [Barwise and Seligman, 1995] Barwise, J. and Seligman, J. (1995). Information Flow. The Logic of Distributed Systems. Cambridge University Press, Cambridge UK.
- [Bernardi and Rainaldi, 2018] Bernardi, C. and Rainaldi, C. (2018). Everywhere surjections and related topics: Examples and counterexamples. Le Matematiche, LXXIII, pages 71–88.
- [Blackburn et al., 2001] Blackburn, P., de Rijke, M., and Venema, Y. (2001). Modal Logic. Cambridge University Press.
- [Dabrowski et al., 1996] Dabrowski, A., Moss, L., and Parikh, R. (1996). Topological reasoning and the logic of knowledge. Annals of Pure and Applied Logic, pages 73–110.
- [Dretske, 1983] Dretske, F. (1983). Knowledge and the Flow of Information. The MIT Press.
- [Goodstein, 1961] Goodstein, R. (1961). Recursive Analysis. Dover Books, Minneola NY.
- [Isbell, 1964] Isbell, J. (1964). Uniform Spaces. American Mathematical Society, Providence.
- [Kelly, 1996] Kelly, K. (1996). The Logic of Reliable Inquiry. Oxford University Press, Oxford.
- [Kremer and Mints, 2007] Kremer, P. and Mints, G. (2007). Dynamic topological logic. In Handbook of Spatial Logics, pages 565–606. Springer.
- [Lorenz, 1995] Lorenz, E. (1995). The Essence of Chaos. The University of Washington Press, Seattle.
- [McKinsey and Tarski, 1944] McKinsey, J. C. C. and Tarski, A. (1944). The algebra of topology. Ann. of Math., 45:141–191.
- [Väänänen, 2007] Väänänen, J. (2007). Dependence Logic: Theory and Applications. Cambridge University Press, Cambridge UK.
- [van Benthem, 2011] van Benthem, J. (2011). Logical Dynamics of Information and Interaction. Cambridge University Press, Cambridge UK.
- [van Benthem and Bezhanishvili, 2007] van Benthem, J. and Bezhanishvili, G. (2007). Modal logics of space. In Aiello, M., Pratt-Hartman, I., and van Benthem, J., editors, Handbook of Spatial Logics, pages 217–298. Springer Science, Heidelberg.
- [van Ditmarsch et al., 2015] van Ditmarsch, H., Halpern, J., van der Hoek, W., and Kooi, B., editors (2015). Handbook of Epistemic Logic. College Publications, London.
- [Vickers, 1996] Vickers, S. (1996). Topology via Logic. Cambridge University Press, Cambridge UK.
- [Willard, 1970] Willard, S. (1970). General Topology. Addison-Wesley Publishing Co., Reading, Mass.-London-Don Mills, Ont.
- [Ye, 2022] Ye, L. (2022). A structural study of information in a logical perspective. Bachelor’s thesis, Tsinghua University.
Appendix A Appendix: Proofs of Completeness and Decidability for the Logical Systems and
It is easy to verify the soundness of the axioms and rules of (and respectively ) on topo-dependence models (and respectively metric dependence models). As for completeness, it is enough to prove (for both logics) completeness with respect to a smaller class of models, namely metric dependence models. However, the usual Modal Logic techniques [Blackburn et al., 2001] (in particular, canonical model construction and filtration) will only give us (finite) non-standard relational models (more precisely, what we will call preorder models). To unify the two types of models (metric/topological and relational), we will introduce a further generalization, that subsumes both under a more abstract notion: topo-models.
A.1 Abstract topo-models
Essentially, topo-models are abstract models, that combine a standard relational semantics for the modalities (in terms of equivalence relations) together with a standard topological semantics for the modalities in terms of topological interior operators, while treating all atoms as just standard atomic sentences whose semantics is given by a valuation, as usual in Modal Logic. We just need to impose a number of constraints on the relations, topology and valuation, to ensure the soundness of our axioms.
Definition A.1 (Topo-models for and ).
A topo-model for is a relational-topological structure
where: is a set of abstract states (‘possible worlds’); for each set of variables, is an equivalence relation on and is a topology on ; and is a valuation, that associates to each atom of the form , , or some subset of the set of states, in the usual way. These ingredients are required to satisfy the following conditions:
- (1)
-
if and , then we have iff ;
- (2)
-
is the total relation , and is the discrete topology on ;232323Given condition (7), the second part of this clause follows in fact from the first part.
- (3)
-
if and , then and ;
- (4)
-
Inclusion, Additivity and Transitivity for all atoms of the form , or :
, whenever ;
, and similarly for and ;
, and similarly for and ); - (5)
-
;
- (6)
-
if , then every -open neighborhood includes some -open neighborhood (i.e., );
- (7)
-
if and , then ;
- (8)
-
;
- (9)
-
;
- (10)
-
;
- (11)
-
(or equivalently: if , then ).
Topo-models for are simply obtained by skipping from the above definition all references to the uniform dependence atoms and all clauses involving them.
Definition A.2 (Abstract Topo-Semantics).
As already announced, the topo-model semantics of is specified (when given a topo-model for ) by using the standard relational semantics for the operators (seen as modalities for ), as well as the interior semantics for the topological modalities , while the semantics of the all atoms (be they propositional or dependence atoms or ) is given by the valuation :
Of course, the semantics of Boolean connectives and is the usual one. The topo-model semantics of is obtained (when given a topo-model for ) by simply skipping the clause for in the above definition.
Topo-dependence models are topo-models Every topo-dependence model of the form , based on a typed topological model , gives rise to an associated topo-model for , obtained by putting:
where is the restriction to of the product topology on and is the joint empirical variable associated to the set of variables .
It should be obvious that the topo-model semantics for on the associated topo-model is the same as the semantics on the original topo-dependence model . Therefore, from now on we will identify a topo-dependence model with the associated topo-model, and thus include topo-dependence models in the class of topo-models. We will later be able to precisely characterize this class among all topo-models: topo-dependence models correspond to standard topo-models for .
Definition A.3 (Topo-morphisms).
Given topo-models and , a map is a topo-morphism if it satisfies the following properties:
-
1.
for each set of variables, is an interior map (i.e., a map that is both open and closed in the standard topological sense for functions) between the topologies and ;
-
2.
is a relational p-morphism (in the usual Modal Logic sense)242424A -morphism (also known as a bounded morphism) is a functional bisimulation between relational structures. See [Blackburn et al., 2001] for details. wrt to the relations and the atoms , , and (in the case of topo-models) .
A topo-model is said to be a topo-morphic image of another topo-model if there exists a surjective topo-morphism from to .
Proposition A.4.
If is a topo-morphism between topo-models and , then the states and satisfy the same formulas of :
The proof is an easy induction on the complexity of , and in fact it simply combines the standard proofs of the similar result for relational and topological structures for modal logic. An immediate consequence is:
Corollary A.5.
If is a topo-morphic image of , then the same formulas of , and respectively , are satisfiable/globally true in and in .
A.2 Special case 1: preorder models
We say that a topo-model is Alexandroff if all topologies are Alexandroff (i.e., the open sets are closed under arbitrary intersections). Alexandroff topo-models can be given a purely relational description, as a special case of modal-relational models for and , seen as purely modal languages:
Definition A.6 (Preorder models).
A preorder model for is a relational model , where: is a set of abstract states (‘possible worlds’); are equivalence relations on , and are preorders252525A preorder is a binary relation that is reflexive and transitive. on (one for each set of variables); and is a valuation that associates to each atom of the form , , or some subset of the set of states, in the usual way. These ingredients are required to satisfy the following conditions:
- (1)
-
if and , then we have iff ;
- (2)
-
both and are equal to the total relation ;262626Once again, the second part of this clause follows in fact from the first part together with condition (7).
- (3)
-
if and , then and ;
- (4)
-
atoms , and satisfy Inclusion, Additivity and Transitivity;
- (5)
-
if and , then ;
- (6)
-
if and , then ;
- (7)
-
if , then ;
- (8)
-
;
- (9)
-
;
- (10)
-
;
- (11)
-
Preorder models for are again simply obtained by skipping from the above definition all references to the atoms and all clauses involving them.
Definition A.7 (Preorder Semantics).
The preorder semantics for uses the standard modal semantics for (as relational modalities for ) and (as relational modalities for the preorders ), while the semantics of all atoms (be they propositional or dependence atoms or ) is again given by the valuation :
and again the semantics of the Boolean connectives is given by the usual clauses. The preorder semantics of is obtained by skipping the clause for in the above definition.
Note that preorder models are just a special class of standard relational models for the extended language with atoms of the form and (as well as in the case of ). This means that we can apply to this semantics all the known concepts and results of Modal Logic [Blackburn et al., 2001], concerning -morphisms, bisimulations, filtrations, etc.
Proposition A.8.
Preorder models for (and respectively ) are the same as Alexandroff topo-models for (and respectively ). A map between two preorder models is a topo-morphism between the corresponding topo-models iff it is a relational p-morphism wrt to both relations and and all the atoms (, , , as well as in the case of ).
Equivalence between preorder models and Alexandroff topo-models As a consequence of Proposition A.8, we will identify Alexandroff topo-models with the corresponding preorder models (and later we will show that they correspond precisely to standard preorder models).
A.3 Special case 2: pseudo-metric models
We now introduce a special class of abstract topo-models that generalizes our intended metric dependence models for .
Definition A.9 (Pseudo-metric models for and ).
Let be a topo-model for . We say that is a pseudo-metric model for if the topologies are induced by pseudo-metrics272727Recall that a pseudo-metric on a set is a map satisfying three conditions, for all : ; ; . on , i.e. we have that
where . Pseudo-metric models for are again obtained by skipping the clauses involving (i.e. they are just topo-models for whose topologies are induced by pseudo-metrics). When we want to fix some specific pseudo-metrics, we exhibit them in a explicit manner, denoting the given pseudo-metric model by .
We now recover our metric dependence models as a special case of pseudo-metric topo-models.
Metric dependence models are pseudo-metric topo-models Every metric dependence model of the form , based on a typed metric model , gives rise to a pseudo-metric topo-model for , obtained by putting:
It should be obvious that the topological structure of this associated pseudo-metric model matches that of the associated topo-model (as introduced in the previous section), which explains our use of the same notation for both constructions. It should be equally obvious that the topo-model semantics for on the associated pseudo-metric model is the same as the semantics on the original metric dependence model . So, as in the case of general topo-models, from now on we will identify a metric dependence model with the associated pseudo-metric model, and thus include metric dependence models in the class of pseudo-metric models (and later show that they precisely correspond to standard pseudo-metric models.)
A.4 Standard models and their representation
Definition A.10 (Standard topo-models).
An topo-model is standard if we have, for all and :
- (St1)
-
is the topology generated by (where we skipped set brackets for singletons as usual, writing for );
- (St2)
-
is the topological indistinguishability relation, given by: iff ;
- (St3)
-
iff ;
- (St4)
-
iff .
Simplified presentation of standard topo-models It should be clear that a standard topo-model is uniquely determined by its set of points , its basic topologies and the valuation of the atoms of the form , so it can be identified with the structure
where the valuation ranges only over atoms ), while the topologies are defined using clause (St1) above, the relations are defined by the clause (St2) above (i.e., as topological indistinguishability relations for ), and the semantics of the atoms and is given by the clauses (St3) and (St4) above.
Proposition A.11.
For every topo-dependence model , the associated topo-model is standard.
The proof of this is immediate. The converse also holds:
Proposition A.12.
Each standard topo-model induces a topo-dependence model , based on the same set of states, where each empirical variable has as its range is given by
the map is given by
the topology on is given by
and finally, the interpretation of each predicate symbol is given by
Moreover, the abstract topo-semantics on agrees with the topo-dependence semantics on the associated abstract topo-dependence model.
Equivalence between standard topo-models and topo-dependence models Based on Facts A.11 and A.12, from now on we will identify topo-dependence models with the corresponding standard topo-models.
Special case: standard preorder models A standard preorder model is just a preorder model that is standard when considered as a topo-model (i.e. it satisfies conditions (St1)-(St5) in the definition of standard topo-models). It is useful to give a more direct characterization of the standard preorder models in purely relational terms:
Proposition A.13.
A structure , consisting of a set of states, equivalence relations and preorder relations on , as well as a valuation for the language of , is a standard preorder model iff it satisfies the following conditions, for all and :
- ()
-
if and , then we have iff ;
- ()
-
is the intersection of all relations with (where for singletons we again wrote for );
- ()
-
iff both and ;
- ()
-
iff ;
- ()
-
iff .
Simplified presentation of standard pre-models It should again be clear that a standard pre-model is uniquely determined by its set of points , its basic preorders and the valuation of the atoms of the form , so it can be identified with the structure
(where the valuation ranges only over atoms ), with the only requirement on these structures being condition () of Proposition A.13. In this simplified presentation, all the other components are definable by standardness: the relations are defined by clause () in Proposition A.13, the relations are defined by the clause () in the same Proposition, and the valuation of the atoms and is given by the clauses () and () in this Proposition.
Equivalence between standard preorder models and Alexandroff topo-dependence models As a special case of the above-mentioned equivalence between standard topo-models and topo-dependence models, we can now identify standard preorder models with the corresponding Alexandroff topo-dependence models.
Definition A.14 (Standard pseudo-metric models).
A pseudo-metric model of the form for is standard if it is standard as a topo-model (i.e. it satisfies all conditions (St1)-(St4) in the definition of standard topo-models), and in addition we have, for all and :
- (St5)
-
iff .
Note that, unlike in the case of preorder models, standard pseudo-metric models are not the same as pseudo-metric models whose underlying topo-model is standard: one needs the additional condition (Stg5). It is useful to have a direct characterization of standard pseudo-metric models in terms of the pseudo-metrics :
Proposition A.15.
A structure consisting of a set of states, equivalence relations and pseudo-distances on , as well as a valuation for the language of , is a standard pseudo-metric model iff it satisfies the following conditions, for all and :
- ()
-
if and , then we have iff ;
- ()
-
is the Chebyshev pseudo-metric induced by the basic pseudo-metrics :
with the convention that ;
- ()
-
pseudo-metric indistinguishability conincides with -equality: iff ;
- ()
-
iff ;
- ()
-
iff ;
- ()
-
iff .
Standard pseudo-metric models can be similarly characterized by restricting the valuation to the language of , and dropping the last clause.
Simplified presentation of standard pseudo-metric models Again, a standard pseudo-metric model is uniquely determined by its set of points , its basic pseudo-distances and the valuation of the atoms of the form , so it can be identified with the structure
where the valuation ranges only over atoms ), while the pseudo-distances are defined by clause () in Proposition A.15, the relations are defined by the clause () in the same Proposition, and the valuation of the atoms , and is given by the clauses (), () and () in this Proposition.
Proposition A.16.
For every metric dependence model , the associated pseudo-metric model is standard.
As in the case of topo-dependence models, the proof of this is immediate, and the converse also holds:
Proposition A.17.
Every standard pseudo-metric model (given in its simplified presentation) induces a metric dependence model , based on the same set of states, together with: each empirical variable has as its range is given by
the map is given by
(this map is obviously surjective); the metrics on are given by
and finally, the interpretation of each predicate symbol is given by
Moreover, the pseudo-metric semantics on agrees with the metric dependence semantics .
A.5 Completeness wrt finite preorder models
Proposition A.18.
The system LCD is complete for finite preorder models for , and similarly the system LUD is complete for finite preorder models for .
Proof.
We only give the proof for the harder case of , and specify which steps should be skipped to obtain the proof for . The proof uses a variation of the standard Modal Logic method of finite canonical models, based on combining the techniques of canonical models and filtration.
Let be our fixed consistent formula (where ‘consistent’ refers to the appropriate proof system, LCD and respectively LUD), and let be the finite set of variables that are actually occurring in . Take now to be the smallest set of formulas in , with the following closure properties:
-
;
-
is closed under subformulas and single negations ;
-
, , for all sets and all (where the closure clause for can be skipped in the case of );
-
if , then .
We can easily show that is finite.
We will build a finite preorder model for consisting of (some) maximally consistent subsets of (where again ‘consistent’ refers to the appropriate proof system, LCD and respectively LUD). First, we fix a maximally consistent subset of s.t. . (The existence of follows by the standard enumeration argument for the finite case of the Lindenbaum Lemma.) Second, for each set , we define two relations and between maximally consistent subsets of , by putting:
We define now a finite preorder model
-
;
-
the relations and are just the restrictions of the above-defined relations and to the set ;
-
is the canonical valuation for all atoms , , and , according to which by definition satisfies an atom iff the atom belongs to .292929More precisely, we put: ; ; ; and , i.e. iff , and otherwise). We skip the clause for in the case of .
Just by looking at the above definitions of and , it should be obvious that the relations (and so also their restrictions) are equivalence relations, and that the relations (and so also their restrictions ) are preorders. This can be further strengthened to:
Lemma A.19.
(Preorder Model Lemma) is a preorder model.
Proof.
We need to check that satisfies conditions (1)-(11) in the definition of preorder models.
For (1), let s.t. and , and assume that . By the definition of the canonical valuation, this means that . By the Determined Atoms axiom of and the closure conditions on (as well as the closure of maximally consistent subsets of under modus ponens in ), we have . Using the fact that and the Inclusion axiom (and again the closure conditions on ), we see that , and hence . By the definition of applied to , we obtain that , and using the Factivity of (axiom ) and the closure of under subformulas, we conclude that , which by the definition of canonical valuation gives us that , as desired.
For (2): By the definition of , is indeed the total relation on .303030As already remarked, the second part of condition (2) on preorder models is redundant, following from the first part together with condition (7).
For (3): Assume and , and so (by the canonical valuation), hence (by the definition of ), and thus (again by the canonical valuation). All that is left is to check that . For this, let , and we need to show that . We check the left-to-right implication (since the converse then follows by the symmetry of ): assume that . Since , we can use the -Transitivity axiom to obtain . So we have , which together with gives us that , hence . On the other hand, from we derive by the axiom of Determined Dependence, and so we have , which together with gives us that , hence , and thus by Factivity (axiom ) we have . Putting these all together, we conclude that , as desired.
Condition (4) follows from the definition of canonical valuation, together with the axioms of Inclusion, Additivity and Transitivity for , and .
For (5) and (6): The proof is completely similar to the above proof of the two conclusions of condition (3), using the definition of (instead of ) and the corresponding axioms for (-Veracity, -Transitivity and Knowable Dependence) instead of the axioms for (-Factivity, -Transitivity and Determined Dependence).
For (7): Assume . To show that , let s.t. , and we need to prove that . To show that , note that implies (by the LCD axioms of -Positive Introspection and Knowable Determination, as well as our closure conditions on ), and similarly implies (by the LCD axiom of Knowable Dependence), and so we obtain . From this and , we infer that , and thus in particular , which by the Factivity axiom gives us , as desired. Next, we also need to show that : for this, note that implies (by Knowability of Epistemic Dependence), hence we also have (by Knowable Dependence and the closure conditions on ), and thus (by -Inclusion). From this together with , we obtain that , so in particular , from which we infer (by Factivity). Putting all these together, we conclude that .
Conditions (8), (9) and (10) follow directly from the definition of canonical valuation, together with the Connecting Axioms of LCD. ∎
Lemma A.20.
(Diamond Lemma) For all states and formulas (where we recall that is single negation), we have:
-
1.
If , then iff there exists with and ;
-
2.
If , then iff there exists with and .
Proof.
The proof of this result goes along standard lines, cf. [Blackburn et al., 2001]: the non-trivial (left-to-right) implications are shown by constructing a consistent set of formulas in , that includes and that forces every -maximally consistent superset to be in the appropriate relation with .313131In fact, the proof of the first item was given in detail in [Baltag and van Benthem, 2021], while the proof of the second item is completely analogous (using the appropriate -axioms instead of the corresponding -axioms). ∎
As an immediate consequence, we obtain:
Lemma A.21.
(Truth Lemma) For every , we have that, for all formulas :
Proof.
The proof proceeds by induction on , as usual. The atomic case is simply enforced by our choice of the canonical valuation, and the Boolean connective cases are trivial, while the modal cases follow from the above Diamond Lemma. ∎
Putting these together, we obtain the desired conclusion, thus showing the completeness of our logics for finite preorder models. ∎
As a consequence, the set of theorems of LCD is recursive, and the same holds for the set of theorems of LUD
Proposition A.22.
The logics axiomatized by the proof systems LCD and LUD are decidable.
Of course, this does not yet prove the decidability of our intended logics and (but only of the given proof systems), but this will follow when we will prove the completeness of these systems with respect to our intended models (i.e., topo-dependence models for LCD, and metric dependence models for LUD).
A.6 Completeness wrt topo-dependence models: unravelling
In this section we show the decidability and completeness of the logic wrt topo-dependence models. By results in previous sections, it is enough to prove completeness wrt standard topo-models. For this, we will prove the following
Lemma A.23.
(Representation theorem for finite preorder models) Every finite preorder model for over a finite set of variables is a topo-morphic image of a standard topo-model for (more precisely a standard preorder model), and thus it is modally equivalent to a topo-dependence model.
The rest of this section is dedicated to the proof of this result.
The idea of the proof Throughout the section, we fix a finite preorder model of the form (for ), and a designated in this model.323232The specific choice of is irrelevant, as all the other states in will be accessible from via the total relation . To find a standard preorder model that is modally equivalent to , we use the well-known modal logic technique of unravelling. The proof goes along familiar lines, by unravelling into a tree of all possible “histories”, redefining the relations on this tree to ensure standardness, and defining a -morphism from the tree into our original model , by mapping each history to its last element. The proof is very similar to the corresponding proof for in [Baltag and van Benthem, 2021], which is itself a modification of the standard modal completeness proof for distributed knowledge (meant to deal with the new dependence atoms ).
Admittedly, our construction is slightly more complicated than necessary for the purposes of this section, since it will include some redundant numerical components that will play no role in this section, but will be useful later in dealing with the metric case. More precisely, instead of labeling the transitions in our unravelled tree by using simple sets of variables (‘agents’) as our labels (as in e.g. the standard proof for ), we label them by expressions of the form , for any set of variables and any real number . The expression is here just a more compact way of writing the ordered pair . The actual real numbers will play no role in this section, except for the distinction between (corresponding to -transitions) and (corresponding to -transitions). So in principle we could use only two values for in this section, and the reader can think of all the other real values in our construction as irrelevant ‘syntactic sugar’; but we do keep all these values for future use in the next section, where they will help us structure our tree of histories as a (standard) pseudo-metric model.333333Even for this purpose, not all real values in will actually be needed. If one prefers to keep the resulting model countable, we can restrict to rational values . In fact, we can restrict the numbers used in our completeness proofs to any set values , with the property that includes , as well as some countable sequence of numbers with and .
Histories Let be a finite preorder model for , and let be a designated state in this model. A history is any finite sequence (of any length ) of the form , where is the designated world, and for each we have: ; ; is a non-negative real number less than ; ; and finally whenever . We denote by the set of possible histories. The map , which sends every history to its last element , will play a key role in our construction.
One-step transition relations on histories There are three relevant one-step relations on histories: the immediate predecessor relation , as well as two labelled versions and of this relation, by putting (for all histories and sets ):
We denote by , and the converses of these one-step relations.
Order, -equality and -order on histories We can now define the order relation on histories, as well as analogues and of the relations and on histories in :
where we denote by the reflexive-transitive closure of relation .
Tree of histories, neighbors and (non-redundant) paths Two histories are neighbors if either one is the immediate predecessor of the other. A path from a history to another history is a chain of histories , having and as its endpoints, and s.t. for every , histories and are neighbors. A path is non-redundant if no history appears twice in the chain. The set of histories endowed with the partial order has an easily visualizable tree structure:
-
there is a unique history with no predecessor, namely ;
-
every other history has a unique immediate predecessor;
-
for every history , there are only finitely many histories ;
-
every pair of histories has a meet w.r.t. to the order ; moreover, by repeating this operation, we can see that triplets of histories also have meets ,343434More generally, every non-empty set of histories has a meet. However, the tree structure is not a meet semi-lattice, since the empty set of histories has no meet: that would be a top element, but the tree has no top.
-
there exists a unique non-redundant path between any two histories;
-
for all histories , we have , and thus we either have or .
Interval notation The interval between two histories is the set of all histories on the non-redundant path from to , i.e.:
It is easy to see that in general we have for all histories :
and this inclusion becomes equality whenever lies between and (i.e., in the interval between them):
Tree-distance and history length The tree-distance between histories and is defined by putting , where is the cardinality of the set (i.e., the length of the non-redundant path from to ). It is easy to see that is a metric on , and that moreover iff are neighbors. The length of a history is the tree-distance between and the root .
Path-characterizations of -equality and -order It is easy to see that, given histories , if is the non-redundant path from to where is the meet of the two histories, then the -equality and -order relations can be characterized as follows:
-
holds iff ;
-
holds iff .
To check this, it is enough to note that the definitions of and imply the existence of appropriate paths from to while that the tree structure implies that any such path must include the non-redundant path , then finally to check that this non-redundant path is “appropriate” for and respectively for only if it satisfies the corresponding clause in the above characterization.353535Technically speaking, proving this requires induction on the tree-distance .
Claim 1. The relations and have the following properties:
- 1.
are equivalence relations, and are preorders;
- 2.
if , then ;
- 3.
the intersection of with its converse is the relation ;
- 4.
the relations and are additive:
- 5.
if then ;
- 6.
if then ;
- 7.
if and , then and ;
- 8.
if and , then and ;
- 9.
if and , then ;
- 10.
if and , then .
Proof.
Items 1 and 2 follow immediately from the definitions of these relations on histories.
Item 3: The fact that implies is easily proved by induction on the tree-distance between the two histories, using the above characterizations of and in terms of the non-redundant path, as well as the fact that and are disjoint by definition.
For item 4, we first check the additivity of and , i.e. that: iff for all ; and iff for all . (These follow directly from the definitions of and and the Additivity axioms for and .) The desired additivity of and follows from these observations by induction of the tree distance (using the above characterizations of and in terms of the non-redundant path).
Items 5 and 6 similarly follow by easy induction (on the tree distance, using the above path characterization) from the corresponding statements for the one-step transitions, i.e.: implies ; and similarly implies . To prove the first of these one-step statements: from , we infer that for some with ; but in order for to be a well-formed history, we must have , which together with gives us , as desired. The second one-step statement is similar: from , we infer that for some with ; but in order for to be a well-formed history, we must have , which together with gives us , as desired.
Similarly, items 7 and 8 follow by easy induction (on the tree distance) from the corresponding statements for the one-step transitions. To check the first of these, assume with . By definition, the first of these means that we have for some with . Together with , this gives us (by the Transitivity axiom for ), and hence we have , as desired. The case of the relatiion (for item 8) is completely analogous.
Finally, items 9 and 10 follow by applying the above characterizations of and respectively in terms of the non-redundant path from to , and then noticing that implies that the same characterizing conditions apply to the subpaths from to , and respectively from to . ∎
The standard preorder model on histories To structure the set of histories as a standard preorder model (in simplified presentation)
we take as our preorders to be just the relations defined above, while the valuation for atoms of the form is inherited from our finite preorder model :
This is meant to be a standard preorder model, so technically speaking the relations and will be defined in this model by standardness (as intersections, in terms of the basic relations , using clauses (1) and (2) of Proposition A.13), rather than the way we defined them above on histories. But Claim 1 ensures that they match the above definitions, as made explicit in the following result:
Claim 2. The structure is indeed a standard preorder model, with its induced -equality and -preorder relations matching the relations and , as defined above on histories.
Proof.
The fact that the relations (as defined above on histories) coincide with the intersections follows from the additivity of (item 4 of Claim 1), while the fact that the relations coincide with the intersections follows from item 3 of Claim 1. So, to prove standardness (given the simplified presentation), it is enough to check condition () of Proposition A.13. For this, assume that we have and . By our choice of valuation on , this means that . By item 5 in Claim 1, implies that in . This, together with (and the fact that is a preorder model), give us (by clause 1 in the definition of preorder models), from which we can conclude that (again by our choice of valuation on ), as desired. ∎
We now finish the proof of our representation result (Lemma A.23 above), with the following:
Claim 3. The function , that maps every history to its last state , is a surjective -morphism from the standard preorder model to the given finite preorder model .
Proof.
The surjectivity of the map is immediate: given , if we take the history of length (which is a correct history, since by the definition of preorder models), then . So we just need to check the clauses in the definition of -morphisms on preorder models.
Atomic clause : holds by our choice of valuation in .
Atomic clause : We need to show that we have iff .
For the left-to-right implication, suppose that , and let ; we must prove that . For this, take the history . Then we have , which together with , gives (since is a preorder model). Since is the reflexive-transitive closure of while is an immediate predecessor of , can only hold in this case iff we have . By the definition of and the structure of , this means that we must have , as desired.
For the converse implication, suppose that ; we need to show that as well. For this, let be any history in with , and we need to prove that . Indeed, from and , we get (by item 7 of Claim 1), as desired.
Atomic clause : We need to show that we have iff .
The left-to-right implication is similar to the above proof for : suppose that , and let ; we need to prove that . For this, take again the history . Then we have (in fact ), which together with , gives us (since is a preorder model). Once again, since is the reflexive-transitive closure of and is an immediate predecessor of , can only hold in this case iff we have . By the definition of and the structure of , this means that we must have , as desired.
For the converse implication, let ; we need to show that as well. For this, let be any histories with , and we must prove that . From and , we get (by item 8 of Claim 1 above). Using this and , we obtain (by applying again item 8 of Claim 1), as desired.
The forth clauses for and are given by parts 5 and 6 of Claim 1 above.
The back clause for : Assuming , we take . This is a well-formed history in , satisfying and , as desired.
The back clause for : Assuming , we take for any number chosen in our construction. Once again, this is a well-defined history in , obviously satisfying the conditions and , as required. ∎
Putting together Proposition A.18 and Lemma A.23 with the well-known facts about the preservation of modal formulas under -morphisms (or more generally, under bisimulations), as well as the modal equivalence between standard preorder models and Alexandroff topo-dependence models, we immediately obtain the completeness of LCD wrt topo-dependence models (and as a consequence the decidability of the logic of topo-dependence models).
A.7 Completeness wrt metric dependence models: refinement
We now wrap up our completeness (and decidability) proofs for and wrt (pseudo-locally Lipschitz) metric dependence models. By previous results, it is enough to prove completeness wrt standard pseudo-metric models (whose pseudo-metrics satisfy the pseudo-locally Lipschitz condition). For this, we show the following:
Lemma A.24.
(Pseudo-metric representation theorem) Every finite preorder model for and respectively (over a finite set of variables ) is a topo-morphic image of a standard pseudo-metric model for , and respectively . Moreover, the metric dependence model associated to this standard pseudo-metric models is pseudo-local Lipschitz.
Plan of the proof. Essentially, the proof proceeds by (a) defining pseudo-distances between histories in the unravelled tree model introduced in the previous section; then (b) showing that, importantly, this pseudo-metric topology is a refinement of the Alexandroff topology associated to the preorders from the previous section, and (c) proving that the resulting structure is a standard pseudo-metric model; and finally (d) showing that the map (sending each history to its last element) is a (surjective) topo-morphism from the topo-model to (the topo-model associated) to our original preorder model for .
The proof in detail In the rest of this section, we present the details of our proof of Lemma A.24. We give the proof of this representation result for only; the proof for can be obtained by simply skipping all the steps and clauses involving the uniform dependence atoms . We start as in the previous section: let be a finite preorder model for . Since this is also in particular a finite preorder model for , we can apply the unravelling technique from the previous section to obtain the structure , as introduced in the previous section. All the notations and results in the previous section still apply, and we will make use of them, in particular of the fact that is a standard preorder model for , and that the map (sending each history to its last element) is a surjective -morphism between preorder models for , and hence a (surjective) interior map between the corresponding topo-models for . For , we will use the notations
to denote the corresponding -upsets in and respectively . Note that the fact that the surjective map is a -morphism is equivalent to saying that, for all histories , we have:
As announced in the Proof Plan, we will endow the set of histories with a pseudo-metric structure, obtained by defining ultra-pseudo-metric distances , and at the same time we will extend the valuation to cover atoms of the form , to obtain a pseudo-metric refinement of the topology of our unravelled preorder model . To do this, we need to introduce some preliminary notions.
The -root of a history When studying the Alexandroff topologies induced by the preorders on the set of all histories, the following notion is of special interest: the -root of a history is the shortest history s.t. .363636Here, “shortest” means that there is no proper sub-history with . It is easy to see that every history has a unique -root, which we will henceforth denote by ; moreover, we obviously have . In fact, if we denote by the -connected component373737A set of histories is -connected if for every two histories there exists some history with . The largest -connected subset of that contains a history is called the -connected component of , and denoted by . In fact, is the equivalence class of with respect to the equivalence relation given by putting iff there exists . that contains , it is easy to see that is a subtree of (wrt ), having as its root. Obviously, states that belong to the same -connected component have the same -root, i.e. we have that:
Density and -density of a history In addition to history length, we need another measure of the complexity of a history . The density of a history is defined as the minimum non-zero index occurring in the history (where we put when there are no such non-zero indices in ). More precisely, we put
with the convention that . Note that, in our setting, this convention is the natural analogue of the more standard convention that : since takes values in , the maximum possible distance is , playing the role of ‘infinity’. A distance will indicate that the two histories are so “far” from each other, that one cannot reach from by any number of “small” changes of -value. Also note that the infimum in the above definition is applied to a finite set of real values, so it can be replaced by minimum whenever the set is non-empty.
The density of a history is a measure of how “far” apart are its preceding histories. However, for defining our -topology on the tree , not all the past of a history is relevant, but only the past of its -root. The -density of history is simply the density of its -root, i.e., the quantity
Closeness To define our -distances, we need a notion of closeness between histories that differs from the tree distance: indeed, even a one-step transition may involve a large jump as far as the intended -distance is concerned. Two neighboring histories and are said to be -close if any of the following conditions holds:
either ; or and ; or and . |
For arbitrary histories, and are said to be -close if all the neighboring histories on the non-redundant path from to are -close. Two histories are said to be -far if they are not -close. Note that, since is a valid formula, every two histories are -close; in other words: if two histories are -far then . Finally, in the case that is a singleton, we can drop the set brackets, saying that two histories are -close (-far) if they are -close (-far).
Claim 1. For all histories and all sets , we have:
- 1.
;
- 2.
if , then ;
- 3.
;
- 4.
if , then ;
- 5.
if (and so also, in particular, if ), then ;
- 6.
;
- 7.
;
- 8.
-closeness is additive: two histories are -close iff they are both -close and -close;
- 9.
-closeness is an equivalence relation.
Proof.
: Parts 1 and 2 follow directly from the definitions of . Part 3 follows from part 1 and the fact that . Part 4 follows from the fact that implies .
Part 5 follows from the observation that implies that every history has also the property that , hence in particular we have that . By the definition of , this implies that .
For part 6: since , by the tree property we must have either or . Our claim is symmetric in and , so without loss of generality we can assume that , hence by part 2 we have , i.e. . On the other hand, since and , by Claim 1(10) in Section A.6 we must also have ; putting this together with and using the additivity of the relation , we obtain that ; moreover, by definition of , no strict predecessor of is , hence no such predecessor can be ; this, together with the fact that , shows that satisfies the defining property of , so we have . In conclusion, we obtain , as desired.
For part 7, we prove two inequalities separately. The fact that follows immediately from the fact that . To check the converse inequality , let be any history s.t. . Then by part 4 we have , and so by part 3 we have , as desired.
Part 8 follows directly from the definition of -closeness, using the Additivity Axioms for , and , as well as part 6.
For part 9, it is obvious that -closeness is reflexive and symmetric. For transitivity, let be s.t. is -close to , and is -close to . By definition, this means that all neighboring histories in are -close, and that the same holds for all neighboring histories in . Using the fact that , it follows that all neighboring histories in are also -close, and thus by definition and are -close, as desired. ∎
The pseudo-metric model on histories We proceed now to define our ultra-pseudo-metric model (in simplified presentation) . As the set of states, we take again the set of all histories, endowed with the same valuation on atoms of the form as on :
Since is meant to be a standard pseudo-metric model, the only thing left is to define the basic pseudo-metrics . Essentially, the pseudo-distance between two ‘close’ histories will be given by the maximum of the real numbers encountered on the non-redundant path between them; while the pseudo-distance between ‘far’ histories will be by definition. More precisely, for every we put:
where we assume the convention that , thus ensuring that .
For sets of variables , the pseudo-distances are defined like in any standard pseudo-metric model, using the Chebyshev distance
As usual, for every history , set and number , we use the notation
to denote the “open ball of radius centered at ”.
We now proceed to prove a number of useful results. First, using the additivity of -closeness (part 8 of Claim 1), we can immediately extend the above defining equations for to sets of variables (given the definition of in terms of Chebyshev distance):
Claim 2. For every set of variables , the functions satisfy the conditions:
As an immediate consequence of Claim 2, we have the following
Important Observations For all histories , we have:
-
1.
iff and are -close;
-
2.
if with , then .
Next, we look at distances between neighboring histories, spelling out a few immediate consequences of Claim 2:
Claim 3. For all neighboring histories , and , and all non-empty sets (with ), we have the following:
- 1.
if , then , , and (hence also );
- 2.
if , then ;
- 3.
if , then , and ;
Proof.
All parts follow from Claim 2 by simple case inspection. For part 1, we also use the constraints on histories and the fact that is the same as , as well as the fact that, by Claim 2, is consistent only with ). For part 2, we use the fact that implies , which implies . For part 3, we use the fact that both and imply , and the constraints on histories that imply that , as well as the fact that implies that and that we have either (which together with gives us ) or (in which case the constraints on histories give us that , hence also ). ∎
We now look at the key properties of our distances between arbitrary histories:
Claim 4. Each satisfies the following properties:
- 1.
;
- 2.
;
- 3.
holds iff ;
- 4.
if , then ;
- 5.
if , then ;
- 6.
(for arbitrary );
- 7.
if and , then (and hence );
- 8.
if , then (and hence );
- 9.
;
- 10.
for all ;
- 11.
if and , then and are -close;
- 12.
if and , then and are -close.
Proof.
Part 1 follows from Claim 2 and the convention that . Part 2 follows immediately from the symmetrical shape of the inductive definition of , and the in-built symmetry of in the case that .
For part 3: The special case in which and are neighboring histories, say should be obvious, using Claim 3(1), via the following sequence of equivalences: iff iff iff iff . The general case follows from this special case by induction on the length of the tree distance between and (using the general definition of for non-neighboring histories, as well as the transitivity of ).
Part 4 follows immediately from the definition of , together with the above-mentioned fact that:
Part 5 is another immediate consequence of the definition of , while part 6 follows from the same definition together with another fact mentioned above, namely that the inclusion
holds for arbitrary histories .
For part 7, assume and . Then, for all pairs satisfying , we have (by part 6), hence by part 3 of Claim 3 we have . Putting all these together along the non-redundant path from and and applying the transitivity of , we obtain the desired conclusion.
To prove part 8, assume and put . Since , by part 5 we have . This together with the fact that , gives by part 7 that , as desired.
For part 9, assume that . From this and the fact that , we infer that , so if we put , then by part 8 we have . It is clearly enough to prove that (hence , and thus , as desired), which by part 3 is equivalent to showing that . For this, we need to prove that holds for all pairs with . To prove this, assume towards a contradiction that we have for some such pair. Then, by the definition of and the fact (since and ), we have that . But on the other hand, from and we obtain by part 5 that , which contradicts .
For part 10, assume that and , i.e. . Choose some , and take the history . The fact that ensures that is a well-defined history with . By part 2 of Claim 3, we also have that , i.e. , and thus , as desired.
For part 11, suppose that , and let be histories with , hence by Claim 2 and are -close. To show that and are also -close, we need to check that all neighboring histories are -close. For this, let with and be such neighboring histories. By part 5, we have . By Claim 2, this implies that we are in one of the following three cases: either and , or and , or else and . Using the assumption that (which implies that and ) and the transitivity axioms for and , as well as the fact that (due to Claim 1.(5) and ) we can easily see that each of these cases yields the analogous case for : in other words, we have either and , or and , or else and . In all cases, and are -close, as desired.
For part 12, let and be histories with and , hence , and we can also assume that (otherwise the desired conclusion follows immediately by part 11). Applying again Claim 2, and are -close. To show that and are also -close, we need to check that all neighboring histories histories are -close. For this, let and be such neighboring histories. Since , by part 9 we have , i.e. . From this and the fact that , we obtain that , which together with , gives us that and (by Claim 1.(15) in Section A.6), and so by Claim 1.(4) above. Since are -close and , we have that are -close. By the definition of -closeness and the assumption that , it follows that we are in one of the following two cases: either and , or else and . In the first case, from and we obtain , which combined with (due to parts 3 and 4 of Claim 1 and the fact that ) gives us that are -close, as desired. In the second case, in which we have and , we combine these with the fact that implies and use additivity to conclude that we have and , thus are again -close, as desired. ∎
The facts in Claim 4 are the main ingredients ensuring that our construction will work as intended. We now proceed to show this, in Claims 5-8, that wrap up the proof of our representation result.
Claim 5. Each is an ultra-pseudo-metric whose topology is a refinement of the Alexandroff topology given by the corresponding preorder and whose metric-topological indistinguishability relation (relating states s.t. ) coincides with the -equality relation . Thus, is a refinement of the (standard) topo-model to a standard pseudo-metric model. Moreover, the metric dependence model associated to is pseudo-locally Lipschitz (with Lipschitz constant ), and so validates the ‘paradisiacal’ implication .
Proof.
The fact that is an ultra-pseudo-metric follows immediately by putting together items 1, 2 and 6 of Claim 4. By part 9 of Claim 4, we have that every upset includes an -open ball centered at (namely the ball ), which implies that the pseudo-metric topology induced by is a refinement of the preorder topology induced by the preorder . Part 3 of Claim 4 shows that the metric indistinguishability relation coincides with -equality . Standardness is by the definition of as the Chebyshev distance based on the ’s. Finally, the fact that the associated metric dependence model is pseudo-locally Lipschitz (with constant ) follows immediately from the (second part of the) Important Observations following Claim 2. ∎
Claim 6. iff .
Proof.
We can assume that , otherwise both sides hold by definition.
For the left-to-right direction, suppose that is a history with . We will only use a weaker consequence of this, namely the fact that (pointwise continuous dependence at ).393939But note that by the last part of Claim 5, this property is actually equivalent to on the ‘paradisiacal’ model . Choose any . Then, by the continuous dependence at point , there exists some s.t.
Take now the history , where and is any chosen number with . Since , we obtain by that . Given the definition of on neighboring histories and and the assumption that , we can infer from and that we have , as desired.
For the converse, let be a history with . We need to show that . For this, we choose , and have to prove that is continuously dependent on on the open neighborhood . In fact, we will prove a stronger statement, namely that is uniformly continuously dependent on on this neighborhood.404040Once again, note that by Claim 5 the apparently stronger condition is actually equivalent to on . Let be any arbitrary positive number. To show uniformly continuous dependence on our given neighborhood, we need to show that
For this, we choose , so we have . Let be s.t. ; so we have (since and ). From these, together with our assumption that , we infer (by part 12 of Claim 4) that is -close to both and . Since closeness is an equivalence relation, it follows that and are -close. By the Important Observation following Claim 2, we obtain that , as desired. ∎
Next, we prove the analogous assertion for uniform dependence:
Claim 7. iff .
Proof.
For the left-to-right direction, suppose that , and assume towards a contradiction that . Choose some number . Applying the definition of to , it follows that there exists some number with the property that
Fix now some , and consider the histories and . By Claim 3.(2), we have , so by we have , hence , and thus (by Claim 2) and are -close. From this, together with the assumption that and the fact that the history has , we obtain (using the definition of -closeness) that and . We consider now two cases: and . If , then in fact we must have (since and are neighboring histories), so by the definition of we infer that , and hence (by the axiom of the system ), thus contradicting our assumption that . In the alternative case when , it follows that is its own -root (since it contains no proper sub-history with ), i.e., , and thus we infer , obtaining the contradiction .
For the converse direction, suppose that . To prove that , let be any number with , and we need to show that there exists s.t.
For this, we take . To prove the desired conclusion, let be histories with . By part 11 of Claim 4 and the fact that , this implies that and are -close, and thus (by the Important Observation following Claim 2) we have , as desired. ∎
Claim 8. The map , mapping each history to its last element , is a uniform topo-morphism from to .
Proof.
In the proof of Lemma A.23 (our representation result for preorder models), we showed that the map is a surjective topo-morphism from to . In particular, using the atomic clauses for and in the definition of that topo-morphism, together with the fact that the models and agree on the semantics of these atoms (which, in the case of follows from the fact that both and are standard and that by Claim 5 the pseudo-metric indistinguishability coincides with -equality ), we obtain the corresponding atomic clauses for and in the definition of topo-morphism from to .
The atomic clauses for and follow from Claims 6 and 7.
The fact that the map is a -morphism wrt was already checked in the proof of Lemma A.23. Since Claim 5 tells us that the relation is the same as the pseudo-metric indistinguishability relation, it follows that is a topo-morphism with respect to this relation.
Finally, we need to prove that is an interior map, i.e. both open and continuous, when seen as a map from to . For this, we will make use of the fact that (by the proof of Lemma A.23), is an interior map (hence continuous) when seen as a map from to .
To show that is open, let be a open set in . We need to prove that is upward-closed in wrt . For this, let with , and we have to show that is included in . Since and is open in the pseudo-metric topology induced by , there must exist some s.t. . By part 10 of Claim 4, we obtain , as desired.
To show that is continuous, let be upward-closed in wrt . We need to prove that is open in the pseudo-metric topology . Since the map was shown in the previous section to be a -morphism from to (or equivalently, an interior map between the two preorder topologies), it follows that is upward-closed in wrt (i.e., open in the Alexandroff topology induced by ). But our pseudo-metric topology is a refinement of the Alexandroff topology induced by , and therefore is also open in the pseudo-metric topology. ∎
This finishes the proof of our representation theorem, hence also our completeness and decidability proof for with respect to metric dependence models. Since the model we constructed is pseudo-locally Lipschitz, this also proves completeness for pseudo-locally Lipschitz models.