{'fraction_non_alphanumeric': 0.04698903425104304, 'fraction_numerical': 0.004910587916753843, 'mean_word_length': 4.147545137789041, 'pattern_counts': {'":': 1, '<': 0, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 23, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
A Topos Foundation for Theories of Physics: I. Formal Languages for Physics

This paper is the first in a series whose goal is to develop a fundamentally new way of constructing theories of physics. The motivation comes from a desire to address certain deep issues that arise when contemplating quantum theories of space and time. Our basic contention is that constructing a theory of physics is equivalent to finding a representation in a topos of a certain formal language that is attached to the system. Classical physics arises when the topos is the category of sets. Other types of theory employ a different topos. In this paper we discuss two different types of language that can be attached to a system, S. The first is a propositional language, PL(S); the second is a higher-order, typed language L(S). Both languages provide deductive systems with an intuitionistic logic. The reason for introducing PL(S) is that, as shown in paper II of the series, it is the easiest way of understanding, and expanding on, the earlier work on topos theory and quantum physics. However, the main thrust of our programme utilises the more powerful language L(S) and its representation in an appropriate topos.


Introduction
This paper is the first in a series whose goal is to develop a fundamentally new way of constructing theories of physics. The motivation comes from a desire to address certain deep issues that arise when contemplating quantum theories of space and time.
A striking feature of the various current programmes for quantising gravityincluding superstring theory and loop quantum gravity-is that, notwithstanding their disparate views on the nature of space and time, they almost all use more-or-less standard quantum theory. Although understandable from a pragmatic viewpoint (since all we have is more-or-less standard quantum theory) this situation is nevertheless questionable when viewed from a wider perspective. Indeed, there has always been a school of thought asserting that quantum theory itself needs to be radically changed/developed before it can be used in a fully coherent quantum theory of gravity.
This iconoclastic stance has several roots, of which, for us, the most important is the use in the standard quantum formalism of certain critical mathematical ingredients that are taken for granted and yet which, we claim, implicitly assume certain properties of space and time. Such an a priori imposition of spatio-temporal concepts would be a major error if they turn out to be fundamentally incompatible with what is needed for a theory of quantum gravity.
A prime example is the use of the continuum which, in this context, means the real and/or complex numbers. These are a central ingredient in all the various mathematical frameworks in which quantum theory is commonly discussed. For example, this is clearly so with the use of (i) Hilbert spaces and operators; (ii) geometric quantisation; (iii) probability functions on a non-distributive quantum logic; (iv) deformation quantisation; and (v) formal (i.e., mathematically ill-defined) path integrals and the like. The a priori imposition of such continuum concepts could be radically incompatible with a quantum gravity formalism in which, say, space-time is fundamentally discrete: as, for example, in the causal set programme.
A secondary motivation for changing the quantum formalism is the peristalithic problem of deciding how a 'quantum theory of cosmology' could be interpreted if one was lucky enough to find one. Most people who worry about foundational issues in quantum gravity would probably place the quantum cosmology/closed system problem at, or near, the top of their list of reasons for re-envisioning quantum theory. However, although we are certainly interested in such conceptual issues, the main motivation for our research programme is not to find a new interpretation of quantum theory. Rather, the goal is to find a novel structural framework within which new types of theory can be constructed, and in which continuum quantities play no fundamental role.
Having said that, it is certainly true that the lack of any external 'observer' of the universe 'as a whole' renders inappropriate the standard Copenhagen interpretation with its instrumentalist use of counterfactual statements about what would happen if a certain measurement was performed. Indeed, the Copenhagen interpretation is inapplicable for any 3 system that is truly 'closed' (or 'self-contained') and for which, therefore, there is no 'external' domain in which an observer can lurk. This problem has motivated much research over the years and continues to be of wide interest. Clearly, the problem is particularly severe in a quantum theory of cosmology.
When dealing with a closed system, what is needed is a realist interpretation of the theory, not one that is instrumentalist. The exact meaning of 'realist' is infinitely debatable but, when used by physicists, it typically means the following: 1. The idea of 'a property of the system' (i.e., 'the value of a physical quantity') is meaningful, and representable in the theory.
2. Propositions about the system are handled using Boolean logic. This requirement is compelling in so far as we humans think in a Boolean way.
3. There is a space of 'microstates' such that specifying a microstate 4 leads to unequivocal truth values for all propositions about the system. The existence of such a state space is a natural way of ensuring that the first two requirements are satisfied.
The standard interpretation of classical physics satisfies these requirements, and provides the paradigmatic example of a realist philosophy in science. On the other hand, the existence of such an interpretation in quantum theory is foiled by the famous Kochen-Specker theorem [4].
What is needed is a formalism that is (i) free of prima facie prejudices about the nature of the values of physical quantities-in particular, there should be no fundamental use of the real or complex numbers; and (ii) 'realist', in at least the minimal sense that propositions are meaningful, and are assigned 'truth values', not just instrumentalist probabilities.
However, finding such a formalism is not easy: it is notoriously difficult to modify the mathematical framework of quantum theory without destroying the entire edifice. In particular, the Hilbert space structure is very rigid and cannot easily be changed. And the formal path-integral techniques do not fare much better.
Our approach includes finding a new way of formulating quantum theory which, unlike the existing approaches, does admit radical generalisations and changes. A recent example of such an attempt is the work of Abramsky and Coecke who construct a categorical analogue of some of the critical parts of the Hilbert space formalism [5]; see also the work by Vicary [6]. Here, we adopt a different strategy based on the intrinsic logical structure that is associated with any topos. 5 3 Of course, the existence of the long-range, and all penetrating, gravitational force means that, at a fundamental level, there is really only one truly closed system, and that is the universe itself. 4 In simple non-relativistic systems, the state is specified at any given moment of time. Relativistic systems (particularly quantum gravity!) require a more sophisticated understanding of 'state', but the general idea is the same. 5 Topos theory is a sophisticated subject and, for theoretical physicists, not always that easy to Our contention is that theories of a physical system should be formulated in a topos that depends on both the theory-type and the system. More precisely, if a theorytype (such as classical physics, or quantum physics) is applicable to a certain class of systems, then, for each system in this class, there is a topos in which the theory is to be formulated. For some theory-types the topos is system-independent: for example, conventional classical physics always uses the topos of sets. For other theory-types, the topos varies from system to system: for example, this is the case in quantum theory.
In regard to the three conditions listed above for a 'realist' interpretation, our scheme has the following ingredients: 1. The concept of the 'value of a physical quantity' is meaningful, although this 'value' is associated with an object in the topos that may not be the real-number object. With that caveat, the concept of a 'property of the system' is also meaningful.
2. Propositions about a system are representable by a Heyting algebra associated with the topos. A Heyting algebra is a distributive lattice that differs from a Boolean algebra only in so far as the law of excluded middle need not hold, i.e., α ∨ ¬α 1. A Boolean algebra is a Heyting algebra with strict equality: α ∨ ¬α = 1.
3. There is a 'state object' in the topos. However, generally speaking, there will not be enough 'microstates' to determine this. Nevertheless, truth values can be assigned to propositions with the aid of a 'truth object'. These truth values lie in another Heyting algebra.
This new approach affords a way in which it becomes feasible to generalise quantum theory without any fundamental reference to Hilbert spaces, path integrals, etc.; in particular, there is no prima facie reason for introducing continuum quantities. As we have emphasised, this is our main motivation for developing the topos approach. We shall say more about this later. From a conceptual perspective, a central feature of our scheme is the 'neo-realist 6 ' structure reflected in the three statements above. This neo-realism is the conceptual fruit of the mathematical fact that a physical theory expressed in a topos 'looks' very much like classical physics.
This fundamental feature stems from (and, indeed, is defined by) the existence of two special objects in the topos: the 'state object' 7 , Σ φ , mentioned above, and the 'quantity-value object', R φ . Then: (i) any physical quantity, A, is represented by an arrow A φ : Σ φ → R φ in the topos; and (ii) propositions about the system are represented by sub-objects of the state object Σ φ . These form a Heyting algebra, as is the case for the set of sub-objects of any object in a topos.
The fact that physical quantities are represented by arrows whose domain is the object Σ φ , and propositions are represented by sub-objects of Σ φ , suggests strongly that Σ φ should be regarded as the topos-analogue of a classical state space. Indeed, for any classical system the topos is just the category of sets, Sets, and then the ideas above reduce to the familiar picture in which (i) there is a state space S which is a set; (ii) any physical quantity, A, is represented by a real-valued functionsȂ : S → IR; and (iii) propositions are represented by subsets of S, and with the associated Boolean algebra.
The present work is the first of a series of papers devoted to exploring in depth the idea that theories of physics should be expressed in a topos that depends on both the theory-type and the system; and that physical quantities and propositions are represented in the ways indicated above. Papers II and III in the series are concerned with quantum theory [1,2] which serves as a paradigmatic example for the general theory. These ideas are motivated by earlier work by one of us (CJI) and Butterfield on interpreting quantum theory in a topos [21,22,23,24,26,25]; see also [20,27].
In the present paper, we will make precise the sense in which propositions about a system can be represented by sub-objects of an object in a topos. To this end, we introduce a formal language for each system with the key idea that the construction of a theory of the system involves finding a representation of the associated language in an appropriate topos. These languages are deductive systems employing intuitionistic logic; as such, they can be used to make, and manipulate, statements about the world as it is revealed in the system under study.
In paper IV ( [3]) we return once more to the overall formalism and consider what happens to the languages and their representations when the system ranges over the objects in a 'category of systems'. This category incorporates the ideas of forming composites of systems, and finding sub-systems of a system.
The plan of the present paper is as follows. Section 2 is written in a rather discursive style and deals with various topics with a significant conceptual content. In particular, we discuss in more detail some of the issues concerning the status of continuum quantities in physics.
Then, in Section 3 we introduce a simple propositional language, PL(S), that can be used to assert statements about the world as it is reflected in the system S. The propositional logic used in this language is intuitionistic and, therefore, it is mathematically consistent to seek representations of PL(S) in a Heyting algebra; in particular in the collection of sub-objects of the state object of a topos.
Simple propositional languages are limited in scope and, therefore, in Section 4 a higher-order, typed language, L(S), is developed. Languages of this sort lie at the heart of topos theory and are of great power. We discuss in detail an example of such a language which, although simple, can be used for many physical systems. This language has just two 'ground type' symbols, Σ and R, that are the linguistic precursors of the state object, and quantity-value object, respectively. In addition, there are 'function symbols' A : Σ → R that represent physical quantities in the theory. We show how representations of L(S) in a topos correspond to concrete physical theories, and work out the scheme in detail for classical physics. (The application to quantum theory is discussed in the next two papers [1,2].) Finally, in Section 5 we draw some conclusions about this first chapter of our endeavour to construct a topos framework within which to construct theories of physics.
The paper concludes with an Appendix which contains some of the central ideas of topos theory. Many important topics are left out for reasons of space, but we have tried to include the key ideas used in this series of papers. To gain a proper understanding of topos theory, we recommend the standard text books [7,8,10,9,11,12] 2 The Conceptual Background of our Scheme

The Problem of Using Real Numbers a Priori
As mentioned in the Introduction, one of the main goals of our work is to find new tools with which to develop theories that are significant extensions of, or developments from, quantum theory but without being tied a priori to the use of the real or complex numbers.
In this context we note that real numbers arise in theories of physics in three different (but related) ways: (i) as the values of physical quantities; (ii) as the values of probabilities; and (iii) as a fundamental ingredient in models of space and time (especially in those based on differential geometry). The first two are of direct concern in our worries about making unjustified, a priori assumptions in quantum theory, and we shall now examine them in detail.
Why are physical quantities assumed to be real-valued? One reason for assuming physical quantities to be real-valued is undoubtedly that, traditionally (i.e., in the pre-digital age), they are measured with rulers and pointers (or they are defined operationally in terms of such measurements), and rulers and pointers are taken to be classical objects that exist in the continuum physical space of classical physics. In this sense there is a direct link between the space in which physical quantities take their values (what we shall call the 'quantity-value space') and the nature of physical space or space-time [19].
If conceded, this claim means that the assumption that physical quantities are real-valued is problematic in a theory in which space, or space-time, is not modelled by a smooth manifold. Admittedly, if the theory employs a background space, or space-time-and if this background is a manifold-then the use of real-valued physical quantities is justified in so far as their value-space can be related to this background. Such a stance is particularly appropriate in situations where the background plays a central role in giving meaning to concepts like 'observers' and 'measuring devices', and thereby provides a basis for an instrumentalist interpretation of the theory.
However, caution is needed with this argument since the background structure may arise only in some 'sector' of the theory; or it may exist only in some limiting, or approximate, sense. The associated instrumentalist interpretation would then be similarly limited in scope. For this reason, if no other, a 'realist' interpretation is more attractive than an instrumentalist one.
In fact, in such circumstances, the phrase 'realist interpretation' does not really do justice to the situation since it tends to imply that there are other interpretations of the theory, particularly instrumentalism, with which the realist one can contend on a more-or-less equal footing. But, as we just argued, the instrumentalist interpretation may be severely limited in scope as compared to the realist one. To flag this point, we will sometimes refer to a 'realist formalism', rather than a 'realist interpretation'. 8 Why are probabilities required to lie in the interval [0, 1]? The motivation for using the subset [0, 1] of the real numbers as the value space for probabilities comes from the relative-frequency interpretation of probability. Thus, in principle, an experiment is to be repeated a large number, N, times, and the probability associated with a particular result is defined to be the ratio N i /N, where N i is the number of experiments in which that result was obtained. The rational numbers N i /N necessarily lie between 0 and 1, and if the limit N → ∞ is taken-as is appropriate for a hypothetical 'infinite ensemble'-real numbers in the closed interval [0, 1] are obtained.
The relative-frequency interpretation of probability is natural in instrumentalist theories of physics, but it is not meaningful if there is no classical spatio-temporal background in which the necessary measurements could be made; or, if there is a background, it is one to which the relative-frequency interpretation cannot be adapted.
In the absence of a relativity-frequency interpretation, the concept of 'probability' must be understood in a different way. In the physical sciences, one of the most discussed approaches involves the concept of 'potentiality', or 'latency', as favoured by Heisenberg, Margenau, and Popper [15][16] [17] (and, for good measure, Aristotle). In this case there is no compelling reason why the probability-value space should be a subset of the real numbers. The minimal requirement is that this value-space is an ordered set-so that one proposition can be said to be more or less probable than another. However, there is no prima facie reason why this set should be totally ordered: i.e., there may be pairs of propositions whose potentialities cannot be compared-something that seems eminently plausible in the context of non-commensurable quantities in quantum theory.
By invoking the idea of 'potentiality', it becomes feasible to imagine a quantumgravity theory with no spatio-temporal background but where probability is still a fundamental concept. However, it could also be that the concept of probability plays no fundamental role in such circumstances, and can be given a meaning only in the context of a sector, or limit, of the theory where a background does exist. This background could then support a limited instrumentalist interpretation which would include a (limited) relative-frequency understanding of probability.
In fact, most modern approaches to quantum gravity aspire to a formalism that is background independent [28,29,30,31]. So, if a background space does arise, it will be in one of the restricted senses mentioned above. Indeed, it is often asserted that a proper theory of quantum gravity will not involve any direct spatio-temporal concepts, and that what we commonly call 'space' and 'time' will 'emerge' from the formalism only in some appropriate limit [18]. In this case, any instrumentalist interpretation could only 'emerge' in the same limit, as would the associated relative-frequency interpretation of probability.
In a theory of this type, there will be no prima facie link between the values of physical quantities and the nature of space or space-time although, of course, this cannot be totally ruled out. In any event, part of the fundamental specification of the theory will involve deciding what the 'quantity-value space' should be.
These considerations suggest that quantum theory must be radically changed in order to accommodate situations where there is no background space, or space-time, manifold within which an instrumentalist interpretation can be formulated, and where, therefore, some sort of 'realist' formalism is essential.
These reflections also suggest that the quantity-value space employed in an instrumentalist realisation of a theory-or a 'sector', or 'limit', of the theory-need not be the same as the quantity-value space in a neo-realist formulation. At first sight this may seem strange but, as is shown in the third paper of this series, this is precisely what happens in the topos reformulation of standard quantum theory [2].

A Possible Role for Heyting Algebras
To motivate topos theory as the source of neo-realism let us first consider classical physics, where everything is defined in the category, Sets, of sets and functions between sets. Then (i) any physical quantity, A, is represented by a real-valued functionȂ : S → IR, where S is the space of microstates; and (ii) a proposition of the form "A ε ∆" (which asserts that the value of the physical quantity A lies in the subset ∆ of the real line IR) 9 is represented by the subset 10Ȃ−1 (∆) ⊆ S. In fact any proposition P about the system is represented by an associated subset, S P , of S: namely, the set of states for which P is true. Conversely, every subset of S represents a proposition. 11 It is easy to see how the logical calculus of propositions arises in this picture. For let P and Q be propositions, represented by the subsets S P and S Q respectively, and consider the proposition "P and Q". This is true if, and only if, both P and Q are true, and hence the subset of states that represents this logical conjunction consists of those states that lie in both S P and S Q -i.e., the set-theoretic intersection S P ∩ S Q . Thus "P and Q" is represented by S P ∩ S Q . Similarly, the proposition "P or Q" is true if either P or Q (or both) are true, and hence this logical disjunction is represented by those states that lie in S P plus those states that lie in S Q -i.e., the set-theoretic union S P ∪ S Q . Finally, the logical negation "not P " is represented by all those points in S that do not lie in S P -i.e., the set-theoretic complement S/S P .
In this way, a fundamental relation is established between the logical calculus of propositions about a physical system, and the Boolean algebra of subsets of the state space. Thus the mathematical structure of classical physics is such that, of necessity, it reflects a 'realist' philosophy, in the sense in which we are using the word.
One way to escape from the tyranny of Boolean algebras and classical realism is via topos theory. Broadly speaking, a topos is a category that behaves very much like the category of sets (see Appendix); in particular, the collection of sub-objects of an object forms a Heyting algebra, just as the collection of subsets of a set form a Boolean algebra. Our intention, therefore, is to explore the possibility of associating physical propositions with sub-objects of some object Σ (the analogue of a classical state space) in some topos.
A Heyting algebra, h, is a distributive lattice with a zero element, 0, and a unit element, 1, and with the property that to each pair α, β ∈ h there is an implication α ⇒ β, characterized by The negation is defined as ¬α := (α ⇒ 0) and has the property that the law of excluded middle need not hold, i.e., there may exist α ∈ h, such that α ∨ ¬α ≺ 1 or, equivalently, ¬¬α ≻ α. This is the characteristic property of an intuitionistic logic. A Boolean algebra is the special case of a Heyting algebra in which there is the strict equality α ∨ ¬α = 1. 9 In the rigorous theory of classical physics, the set S is a symplectic manifold, and ∆ is a Borel subset of IR. Also, the functionȂ : S → IR may be required to be measurable, or continuous, or smooth, depending on the quantity, A, under consideration. 10 Throughout this series of papers we will adopt the notation in which A ⊆ B means that A is a subset of B that could equal B; while A ⊂ B means that A is a proper subset of B; i.e., A does not equal B. Similar remarks apply to other pairs of ordering symbols like ≺, ; or ≻, , etc. 11 More precisely, every Borel subset of S represents many propositions about the values of physical quantities. Two propositions are said to be 'physically equivalent' if they are represented by the same subset of S.
The elements of a Heyting algebra can be manipulated in a very similar way to those in a Boolean algebra. One of our claims is that, as far as theories of physics are concerned, Heyting logic is a viable 12 alternative to Boolean logic.
To give some idea of the difference between a Boolean algebra and a Heyting algebra, we note that the paradigmatic example of the former is the collection of all measurable subsets of a measure space X. Here, if α ⊆ X represents a proposition, the logical negation, ¬α, is just the set-theoretic complement X/α.
On the other hand, the paradigmatic example of a Heyting algebra is the collection of all open sets in a topological space X. Here, if α ⊆ X is open, the logical negation ¬α is defined to be the interior of the set-theoretical complement X/α. Therefore, the difference between ¬α in the topological space X, and ¬α in the measurable space generated by the topology of X, is just the 'thin' boundary of X/α.

Our Main Contention about Topos Theory and Physics
We contend that, for a given theory-type (for example, classical physics, or quantum physics), each system S to which the theory is applicable is associated with a particular topos τ φ (S) within whose framework the theory, as applied to S, is to be formulated and interpreted. In this context, the 'φ'-subscript is a label that changes as the theorytype changes. It signifies the representation of a system-language in the topos τ φ (S): we will come to this later.
The conceptual interpretation of this formalism is 'neo-realist' in the following sense: and R φ,S are two special objects in the topos τ φ (S). These are the analogues of, respectively, (i) the classical state space, S; and (ii) the real numbers, IR, in which classical physical quantities take their values.
In what follows, Σ φ,S and R φ,S are called the 'state object', and the 'quantityvalue object', respectively.
2. Propositions about the system S are represented by sub-objects of Σ φ,S . These sub-objects form a Heyting algebra.
3. Once the topos analogue of a state (a 'truth object') has been specified, these propositions are assigned truth values in the Heyting logic associated with the global elements of the sub-object classifier, Ω τ φ (S) , in the topos τ φ (S).
Thus a theory expressed in this way looks very much like classical physics except that whereas classical physics always employs the topos of sets, other theoriesincluding quantum theory and, we conjecture, quantum gravity-use a different topos.
One deep result in topos theory is that there is an internal language associated with each topos. In fact, not only does each topos generate an internal language, but, conversely, a language satisfying appropriate conditions generates a topos. Topoi constructed in this way are called 'linguistic topoi', and every topos can be regarded as a linguistic topos. In many respects, this is one of the profoundest ways of understanding what a topos really 'is'. This aspect of topos theory is discussed at length in the books by Bell [9], and Lambek and Scott [10].
These results are exploited in Section 4 where we introduce the idea that, for any applicable theory-type, each physical system S is associated with a 'local' language, L(S). The application of the theory-type to S is then equivalent to finding a representation of L(S) in a topos.
Closely related to the existence of this linguistic structure is the striking fact that a topos can be used as a foundation for mathematics itself, just as set theory is used in the foundations of 'normal' (or 'classical') mathematics. In this context, the key remark is that the internal language of a topos has a form that is similar in many ways to the formal language on which normal set theory is based. It is this internal, topos language that is used to interpret the theory in a 'neo-realist' way.
The main difference with classical logic is that the logic of the topos language does not satisfy the principle of excluded middle, and hence proofs by contradiction are not permitted. This has many intriguing consequences. For example, there are topoi with genuine infinitesimals that can be used to construct a rival to normal calculus. The possibility of such quantities stems from the fact that the normal proof that they do not exist is a proof by contradiction.
Thus each topos carries its own world of mathematics: a world which, generally speaking, is not the same as that of classical mathematics.
Consequently, by postulating that, for a given theory-type, each physical system carries its own topos, we are also saying that to each physical system plus theorytype there is associated a framework for mathematics itself! Thus classical physics uses classical mathematics; and quantum theory uses 'quantum mathematics'-the mathematics formulated in the topoi of quantum theory. To this we might add the conjecture: "Quantum gravity uses 'quantum gravity' mathematics"!

Two Opposing Interpretations of Propositions
Attempts to construct a naïve realist interpretation of quantum theory founder on the Kochen-Specker theorem. However, if, despite this theorem, some degree of realism is still sought, there are not that many options.
One approach is to 'reify' only a subset of physical variables, as, for example, in the pilot-wave approach and other 'modal interpretations'. A topos-theoretic extension of this idea of 'partial reification' was proposed in [21,22,23,24] with a technique in which all possible reifyable sets of physical variables are included on an equal footing. This involves constructing a category, C, whose objects are collections of quantum observables that can be simultaneously reified because the corresponding self-adjoint operators commute. Of course, the concept of 'measurement' plays no fundamental role in our neo-realist, topos approach.
In this earlier work, it was postulated that the logic for handling quantum propositions from this perspective is that associated with the topos of presheaves 13 , Sets C op . The idea is that a single presheaf will encode any quantum proposition from the perspective of all contexts at once. However, in the original papers, the crucial 'daseinisation' operation (see paper II) was not known and, consequently, the discussion became convoluted in places. In addition, the generality and power of the underlying procedure was not fully appreciated.
For this reason, in the present paper we return to the basic questions and reconsider them in the light of the overall topos structure that has now become clear.
We start by considering the way in which propositions arise, and are manipulated, in physics. For simplicity, we will concentrate on systems that are associated with 'standard' physics. Then, to each such system S there is associated a set of physical quantities-such as energy, momentum, position, angular momentum etc. 14 -all of which are real-valued. The associated propositions are of the form "A ε ∆", where A is a physical quantity, and ∆ is a subset 15 of IR.
From a conceptual perspective, the proposition "A ε ∆" can be read in two, very different, ways: (i) The (naïve) realist interpretation: "The physical quantity A has a value, and that value lies in ∆." (ii) The instrumentalist interpretation: "If a measurement is made of A, the result will be found to lie in ∆." The former is the familiar, 'commonsense' understanding of propositions in both classical physics and daily life. The latter underpins the Copenhagen interpretation of quantum theory. The instrumentalist interpretation can, of course, be applied to classical physics too, but it does not lead to anything new. For, in classical physics, what is measured is what is the case: "Epistemology models ontology".
We will now study the role of propositions in physics more carefully, particularly in the context of 'realist' interpretations.

Intuitionistic Logic and the Definition of PL(S)
We are going to construct a formal language, PL(S), with which to express propositions about a physical system, S, and to make deductions concerning them. Our intention is to interpret these propositions in a 'realist' way: an endeavour whose mathematical underpinning lies in constructing a representation of PL(S) in a Heyting algebra, H, that is part of the mathematical framework involved in the application of a particular theory-type to S.
The first step is to construct the set, PL(S) 0 , of all strings of the form "A ε ∆" where A is a physical quantity of the system S, and ∆ is a (Borel) subset of the real line, IR. Note that what has here been called a 'physical quantity' could better (but more clumsily) be termed the 'name' of the physical quantity. For example, when we talk about the 'energy' of a system, the word 'energy' is the same, and functions in the same way in the formal language, irrespective of the details of the actual Hamiltonian of the system.
The strings "A ε ∆" are taken to be the primitive propositions about the system, and are used to define 'sentences'. More precisely, a new set of symbols {¬, ∧, ∨, ⇒} is added to the language, and then a sentence is defined inductively by the following rules (see Ch. 6 in [8]): 1. Each primitive proposition "A ε ∆" in PL(S) 0 is a sentence.
2. If α is a sentence, then so is ¬α.
The collection of all sentences, PL(S), is an elementary formal language that can be used to express and manipulate propositions about the system S. Note that the symbols ¬, ∧, ∨, and ⇒ have no explicit meaning, although of course the implicit intention is that they should stand for 'not', 'and', 'or' and 'implies', respectively. This implicit meaning becomes explicit when a representation of PL(S) is constructed as part of the application of a theory-type to S (see below). Note also that PL(S) is a propositional language only: it does not contain the quantifiers '∀' or '∃'. To include them requires a higher-order language. We shall return to this in our discussion of the local language L(S).
The next step arises because PL(S) is not only a vehicle for expressing propositions about the system S: we also want to reason with it about the system. To achieve this, a series of axioms for a deductive logic must be added to PL(S). This could be either classical logic or intuitionistic logic, but we select the latter since it allows a larger class of representations/models, including representations in topoi in which the law of excluded middle fails.
The axioms for intuitionistic logic consist of a finite collection of sentences in PL(S) (for example, α ∧ β ⇒ β ∧ α), plus a single rule of inference, modus ponens (the 'rule of detachment') which says that from α and α ⇒ β the sentence β may be derived.
Others axioms might be added to PL(S) to reflect the implicit meaning of the primitive proposition "A ε ∆": i.e., "A has a value, and that value lies in ∆ ⊆ IR". For example, the sentence "A ε ∆ 1 ∧ A ε ∆ 2 " ('A belongs to ∆ 1 ' and 'A belongs to ∆ 2 ') might seem to be equivalent to " Thus, along with the axioms of intuitionistic logic and detachment, we might be tempted to add the following axioms: These axioms are consistent with the intuitionistic logical structure of PL(S).
We shall see later the extent to which the axioms (3.1-3.2) are compatible with the topos representations of classical physics, and of quantum physics. However, the other obvious proposition to consider in this way-"It is not the case that A belongs to ∆"-is clearly problematical.
In classical logic, this proposition 16 , "¬(A ε ∆)", is equivalent to "A belongs to IR\∆", where IR\∆ denotes the set-theoretic complement of ∆ in IR. This suggests augmenting (3.1-3.2) with a third axiom However, applying '¬' to both sides of (3.3) gives because of the set-theoretic result IR\(IR\∆) = ∆. But in an intuitionistic logic we do not have α ⇔ ¬¬α but only α ⇒ ¬¬α, and so (3.3) could be false in a Heyting-algebra representation of PL(S) that was not Boolean. Therefore, adding (3.3) as an axiom in PL(S) is not indicated if representations are to be sought in non-Boolean topoi.

Representations of PL(S).
To use the language PL(S) 'for real' it must be represented in the concrete mathematical structure that arises when a theory-type is applied to S. Such a representation, π, maps each of the primitive propositions, α, in PL(S) 0 to an element, π(α), of some Heyting algebra (which could be Boolean), H, whose specification is, of course, part of the theory. For example, in classical mechanics, the propositions are represented in the Boolean algebra of all (Borel) subsets of the classical state space.
The representation of the primitive propositions can be extended recursively to all of PL(S) with the aid of the following rules [8]: Note that, on the left hand side of (3.5-3.8), the symbols {¬, ∧, ∨, ⇒} are elements of the language PL(S), whereas on the right hand side they are the logical connectives in the Heyting algebra, H, in which the representation takes place.
This extension of π from PL(S) 0 to PL(S) is consistent with the axioms for the intuitionistic, propositional logic of the language PL(S). More precisely, these axioms become tautologies: i.e., they are all represented by the maximum element, 1, in the Heyting algebra. By construction, the map π : PL(S) → H is then a representation of PL(S) in the Heyting algebra H. A logician would say that π : PL(S) → H is an H-valuation, or H-model, of the language PL(S).
Note that different systems, S, can have the same language. For example, consider a point-particle moving in one dimension, with a Hamiltonian H = p 2 2m + V (x). Different potentials V (x) correspond to different systems (in the sense in which we are using the word 'system'), but the physical quantities for these systems-or, more precisely, the 'names' of these quantities, for example, 'energy', 'position', 'momentum'-are the same for them all. Consequently, the language PL(S) is independent of V (x). However, the representation of, say, the proposition "Hε∆", with a specific subset of the state space will depend on the details of the Hamiltonian.
Clearly, a major consideration in using the language PL(S) is choosing the Heyting algebra in which the representation takes place. A fundamental result in topos theory is that the set of all sub-objects of any object in a topos is a Heyting algebra: these are the Heyting algebras with which we will be concerned.
Of course, beyond the language, S, and its representation π, lies the question of whether or not a proposition is true. This requires the concept of a 'state' which, when specified, yields 'truth values' for the primitive propositions in PL(S). These are then extended recursively to the rest of PL(S). In classical physics, the possible truth values are just 'true' or 'false'. However, the situation in topos theory is more complex, and discussion is deferred to paper II of the present series [1].
Introducing time dependence. There is also the question of 'how things change in time'. In the form presented above, the language PL(S) may seem geared towards a 'canonical' perspective in so far as the propositions concerned are, presumably, to be asserted at a particular moment of time, and, as such, deal with the values of physical quantities at that time. In other words, the underlying spatio-temporal perspective seems thoroughly 'Newtonian'. This is partly true; but only partly, since the phrase 'physical quantity' can have meanings other than the canonical one. For example, one could talk about the 'time average of momentum', and call that a physical quantity. In this case, the propositions would be about histories of the system, not just 'the way things are' at a particular moment in time.
We will return to these extended versions of the formalism in our discussion of the higher-order language, L(S), in Section 4.4. However, for the moment let us focus on the canonical perspective, and the associated question of how time dependence is to be incorporated. This can be addressed in various ways.
One possibility is to attach a time label, t, to the physical quantities, so that the primitive propositions become of the form "A t ε ∆". In this case, the language itself becomes time-dependent, so that we should write PL(S) t . One might not like the idea of adding external labels in the language and, indeed, in our discussion of the higherorder language L(S) we will strive to eliminate such things. However, in the present case, in so far as ∆ ⊆ IR is already an 'external' (to the language) entity, there seems no particular objection to adding another one.
If we adopt this approach, the representation π will map "A t ε ∆" to a timedependent element, π(A t ε ∆), of the Heyting algebra, H; one could say that this is a type of 'Heisenberg picture'. However, this suggests another option, which is to keep the language time-independent, but allow the representation to be time-dependent. In that case, π t (A ε ∆) will again be a time-dependent member of H.
Another approach is to let the 'truth object' in the theory be time-dependent: this corresponds to a type of Schrödinger picture. We will return to this subject in paper II where the concept of a truth object is discussed in detail [1].

The Representation of PL(S) in Classical Physics
Let us now look at the representation of PL(S) that corresponds to classical physics. In this case, the topos involved is just the category, Sets, of sets and functions between sets.
We will denote by π cl the representation of PL(S) that describes the classical, Hamiltonian mechanics of a system, S, whose state-space is a symplectic (or Poisson) manifold S. We denote byȂ : S → IR the real-valued function 17 on S that represents the physical quantity A.
Then the representation π cl maps the primitive proposition "A ε ∆" to the subset of S given by This representation can be extended to all the sentences in PL(S) with the aid of (3.5-3.8). Note that, since ∆ is a Borel subset of IR,Ȃ −1 (∆) is a Borel subset of the state-space S. Hence, in this case, H is equal to the Boolean algebra of all Borel subsets of S.
We note that, for all (Borel) subsets ∆ 1 , ∆ 2 of IR we havȇ and hence all three conditions (3.1-3.3) that we discussed earlier can be added consistently to the language PL(S) .
Consider now the assignment of truth values to the propositions in this theory. This involves the idea of a 'state' which, in classical physics, is simply an element s of the state space S. Each state s assigns to each primitive proposition "A ε ∆", a truth value, ν A ε ∆; s , which lies in the set {false, true} (which we identify with {0, 1}) and is defined as for all s ∈ S.

The Failure to Represent PL(S) in Standard Quantum Theory.
The procedure above that works so easily for classical physics fails completely if one tries to apply it to standard quantum theory.
In quantum physics, a physical quantity A is represented by a self-adjoint operator A on a Hilbert space H, and the proposition "A ε ∆" is represented by the projection operatorÊ[A ∈ ∆] which projects onto the subset ∆ of the spectrum ofÂ; i.e., (3.14) Of course, the set of all projection operators, P(H), in H has a 'logic' of its own-the 'quantum logic' 18 of the Hilbert space H-but this is incompatible with the intuitionistic logic of the language PL(S), and the representation (3.14).
Indeed, since the 'logic' P(H) is non-distributive, there will exist non-commuting operatorsÂ,B,Ĉ, and Borel subsets ∆ A , ∆ B , ∆ C of IR such that 19 18 For an excellent survey of quantum logic see [14]. This includes a discussion of a first-order axiomatisation of quantum logic, and with an associated sequent calculus. It is interesting to compare our work with what the authors of this paper have done. We hope to return to this at some time in the future. 19 There is a well-known example that uses three rays in IR 2 , so this phenomenon is not particularly exotic.
while, on the other hand, the logical bi-implication can be deduced from the axioms of the language PL(S).
This failure of distributivity bars any naïve realist interpretation of quantum logic.

If an instrumentalist interpretation is used instead, the spectral projectorsÊ[A ∈ ∆] now represent propositions about what would happen if a measurement is made, not
propositions about what is 'actually the case'. And, of course, when a state is specified, this does not yield actual truth values but only the Born-rule probabilities of getting certain results.

The Basics of the Language L(S)
We want now to consider the possibility of representing the physical quantities of a system by arrows in a topos other than Sets.
The physical meaning of such a quantity is not clear, a priori. Nor is it clear what it is that is being represented in this way. However, what is clear is that in such a situation it is no longer correct to work with a fixed value-space IR. Rather, the targetobject, R S , is potentially topos-dependent, and therefore part of the 'representation'.
A powerful technique for allowing the quantity-value object to be system-dependent is to add a symbol 'R' to the language. Developing this line of thinking suggests that 'Σ', too, should be added, as should a symbol 'A : Σ → R', to be construed as 'what it is' that is represented by the arrow in a topos. Similarly, there should be a symbol 'Ω', to act as the linguistic precursor to the sub-object classifier in the topos; in the topos Sets, this is just the set {0, 1}.
The clean way of doing all this is to construct, what Bell [9] calls, a 'local language'. Our basic assumption is that a unique local language, L(S), is associated with each system S. Physical theories of S then correspond to representations of L(S) in appropriate topoi.
The symbols of L(S). We first consider the minimal set of symbols needed to handle elementary physics. For more sophisticated theories in physics, it will be necessary to change, or enlarge, the set of 'ground type' symbols.
The symbols for the local language, L(S), are defined recursively as follows: 1. (a) The basic type symbols are 1, Ω, Σ, R. The last two, Σ and R, are known as ground-type symbols. They are the linguistic precursors of the state object, and quantity-value object, respectively.
(b) If T is a type symbol, then so is P T .

(a)
For each type symbol, T , there is associated a countable set of variables of type T .
(b) There is a special symbol * .

(a)
To each pair (T 1 , T 2 ) of type symbols there is associated a set, F L(S) (T 1 , T 2 ), of function symbols. Such a symbol, A, is said to have signature T 1 → T 2 ; this is indicated by writing A : T 1 → T 2 .
(b) Some of these sets of function symbols may be empty. However, particular importance is attached to the set, F L(S) (Σ, R), of function symbols A : Σ → R, and we assume this set is non-empty.
The function symbols A : Σ → R represent the 'physical quantities' of the system, and hence F L(S) (Σ, R) will depend on the system. In fact, the only parts of the language that are system-dependent are these function symbols.
For example, if S 1 is a point particle moving in one dimension, the set of physical quantities could be chosen to be F L(S 1 ) (Σ, R) = {x, p, H} which represent the position, momentum, and energy of the system. On the other hand, if S 2 is a particle moving in three dimensions, we could have F L(S 2 ) (Σ, R) = {x, y, z, p x , p y , p z , H} to allow for threedimensional position and momentum. Or, we could decide to add angular momentum too, to give the set F L(S 2 ) (Σ, R) = {x, y, z, p x , p y , p z , J x , J y , J z , H}.
Note that, as with the propositional language PL(S), the fact that a given system has a specific Hamiltonian 21 -expressed as a particular function of position and momentum coordinates-is not something that is to be coded into the language: instead, such system dependence arises in the choice of representation of the language. This means that many different systems can have the same local language.
Finally, it should be emphasised that this list of symbols is minimal and one may want to add more. One obvious, general, example is a type symbol IN, to be interpreted as the linguistic analogue of the natural numbers. The language could then be augmented with the axioms of Peano arithmetic.
The terms of L. The next step is to enumerate the 'terms' in the language, together with their associated types [9, 10]: 1. (a) For each type symbol T , the variables of type T are terms of type T . 20 By definition, if n = 0 then T 1 × T 2 × · · · × T n := 1. 21 It must be emphasised once more that the use of a local language is not restricted to standard, canonical systems in which the concept of a 'Hamiltonian' is meaningful. The scope of the linguistic ideas is much wider than that: the canonical systems are only an example. Indeed, our long-term interest is in the application of these ideas to quantum gravity, where the local language is likely to be very different from that used here. However, the basic ideas are the same.
(b) The symbol * is a term of type 1.
(c) A term of type Ω is called a formula; a formula with no free variables is called a sentence.

If
A is function symbol with signature T 1 → T 2 , and t is a term of type T 1 , then In particular, if A : Σ → R is a physical quantity, and t is a term of type Σ, then A(t) is a term of type R.
(b) If t is a term of type T 1 × T 2 × · · · × T n , and if 1 ≤ i ≤ n, then (t) i is a term of type T i .

(a)
If ω is a term of type Ω, andx is a variable of type T , then {x | ω} is a term of type P T .
(b) If t 1 , t 2 are terms of the same type, then t 1 = t 2 is a term of type Ω.
(c) If t 1 , t 2 are terms of type T, P T respectively, then t 1 ∈ t 2 is a term of type Ω.
Note that the logical operations are not included in the set of symbols. Instead, they can all be defined using what is already given. and so on.
Terms of particular interest to us. Let A be a physical quantity in the set F L(S) Σ, R , and therefore a function symbol of signature Σ → R. In addition, let ∆ be a variable (and therefore a term) of type P R; and lets be a variable (and therefore a term) of type Σ. Then some terms of particular interest to us are the following: 1. A(s) is a term of type R with a free variable,s, of type Σ.
2. 'A(s) ∈∆' is a term of type Ω with free variables (i)s of type Σ; and (ii)∆ of type P R.

{s | A(s)
∈∆} is a term of type P Σ with a free variable∆ of type P R.
As we shall see, {s | A(s) ∈∆} and 'A(s) ∈∆' are (closely related) analogues of the primitive propositions "A ε ∆" in the propositional language PL(S). However, there is a crucial difference. In PL(S), the '∆' in "A ε ∆" is a specific subset of the external (to the language) real line IR. On the other hand, in the local language L(S), the '∆' in 'A(s) ∈∆' is an internal variable within the language.
Adding axioms to the language. To make the language L(S) into a deductive system we need to add a set of appropriate axioms and rules of inference. The former are expressed using sequents: defined as expressions of the form Γ : α where α is a formula (a term of type Ω) and Γ is a set of such formula. The intention is that 'Γ : α' is to be read intuitively as "the collection of formula in Γ 'imply' α". If Γ is empty we just write : α.
The basic axioms include things like 'α : α' (tautology), and ':t ∈ {t | α} ⇔ α' (comprehension) wheret is a variable of type T . These axioms 23 and the rules of inference (sophisticated analogues of modus ponens) give rise to a deductive system using intuitionistic logic. For the details see [9,10].
However, for applications in physics we could add extra axioms (in the form of sequents). For example, perhaps the quantity-value object should always be an abeliangroup object 24 ? This can be coded into the language by adding the axioms for an abelian group structure for R. This involves the following steps: 1. Add the following symbols: (a) A 'unit' function symbol 0 : 1 → R; this will be the linguistic analogue of the unit element in an abelian group.
Equality: x = y, α(z/x) : α(z/y). Here, α(z/x) is the term α withz replaced by the term x for each free occurrence of the variablez. The terms x and y must be of the same type asz. Products: Comprehension: :t ∈ {t | α} ⇔ α 2. Then add axioms like ': ∀r + r, 0( * ) =r ' wherer is a variable of type R, and so on.
For another example, consider a point particle moving in three dimensions, with the function symbols F L(S) (Σ, R) = {x, y, z, p x , p y , p z , J x , J y , J z , H}. As L(S) stands, there is no way to specify, for example, that 'J x = yp z − zp y '. Such relations can only be implemented in a representation of the language. However, if this relation is felt to be 'universal' (i.e., it holds in all physically-relevant representations) then it could be added to the language with the use of extra axioms.
One of the delicate decisions that has to be made about L(S) is what extra axioms to add to the base language. Too few, and the language lacks content; too many, and representations of potential physical significance are excluded. This is one of the places in the formalism where a degree of physical insight is necessary!

Representing L(S) in a Topos
The construction of a theory of the system S involves choosing a representation 25 /model, φ, of the language L(S) in a topos 26 τ φ . The choice of both topos and representation depend on the theory-type being used.
For example, consider a system, S, that can be treated using both classical physics and quantum physics, such as a point particle moving in three dimensions. Then, for the application of the theory-type 'classical physics', in a representation denoted σ, the topos τ σ is Sets, and Σ is represented by the symplectic manifold Σ σ := T * IR 3 .
On the other hand, for the application of the theory-type 'quantum physics', τ φ is the topos, Sets V(H) op , of presheaves over the category 27 is the Hilbert space of the system S. In this case, Σ is represented by Σ φ := Σ, where Σ is the spectral presheaf; this representation is discussed at length in papers II and III [1,2]. For both theory types, the details of, for example, the Hamiltonian, are coded in the representation.
We now list the τ φ -representation of the most significant symbols and terms in our language, L(S) (we have only picked out the parts that are immediately relevant to our programme: for full details see [9,10]).

(a)
The ground type symbols Σ and R are represented by objects Σ φ and R φ in τ φ . These are identified physically as the state object, and quantity-value 25 The word 'interpretation' is often used in the mathematical literature, but we want to reserve that for use in discussions of interpretations of quantum theory, and the like. 26 A more comprehensive notation is τ φ (S), which draws attention to the system S under discussion; similarly, the state object could be written as Σ φ,S , and so on. This extended notation is used in paper IV where we are concerned with the relations between different systems, and then it is essential to indicate which system is meant. However, in the present paper, only one system at a time is being considered, and so the truncated notation is fine. 27 We recall that the objects in V(H) are the unital, commutative von Neumann subalgebras of the algebra, B(H), of all bounded operators on H. object, respectively.
2. For each type symbol P T , we have (P T ) φ := P T φ , the power object of the object T φ in τ φ .

each physical quantity) is represented by an arrow
We will generally require the representation to be faithful : i.e., the map A → A φ is one-to-one.

A term of type Ω of the form 'A(s) ∈∆' (which has free variabless,∆ of type Σ and P R respectively) is represented by an arrow [[
In detail, this arrow is Thus [[ A(s) ∈∆ ]] φ is the chain of arrows: We see that the analogue of the '∆' used in the PL(S)-propositions "A ε ∆" is played by sub-objects of R φ (i.e., global elements of P R φ ) in the domain of the arrow in (4.3). These objects are, of course, representation-dependent (i.e., they depend on φ).

A term of type P Σ of the form {s | A(s) ∈∆} (which has a free variable∆ of type P R) is represented by an arrow [[ {s |
6. A term, ω, of type Ω with no free variables is represented by a global element [[ ω ]] φ : 1 τ φ → Ω τ φ . These will typically act as 'truth values' for propositions about the system. 7. Any axioms that have been added to the language are required to be represented by the arrow true : 1 τ φ → Ω τ φ . 28 One of the basic properties of a topos is that there is a one-to-one correspondence between arrows The local set theory of a topos. We should emphasise that the decision to focus on the particular type of language that we have, is not an arbitrary one. Indeed, there is a deep connection between such languages and topos theory.
In this context, we first note that to any local language, L, there is associated a 'local set theory'. This involves defining an 'L-set' to be a term X of power type (so that expressions of the form x ∈ X are meaningful) and with no free variables. Analogues of all the usual set operations can be defined on L-sets. For example, if X, Y are L-sets of type P T , one can define X ∩ Y := {x |x ∈ X ∧x ∈ Y } wherex is a variable of type T .
Furthermore, each local set theory, L, gives rise to an associated topos, C(L), whose objects are equivalence classes of L-sets, where X ≡ Y is defined to mean that the equation X = Y (i.e., a term of type Ω with no free variables) can be proved using the sequent calculus of the language with its axioms. From this perspective, a representation of L(S) in a topos τ is equivalent to a functor from the topos C(L(S)) to τ .
Conversely, for each topos τ there is a local language, L(τ ), whose ground-type symbols are the objects of τ , and whose function symbols are the arrows in τ . It then follows that a representation of a local language, L, in τ is equivalent to a 'translation' of L in L(τ ).
Thus, a rather elegant way of summarising what is involved in constructing a theory of physics is that we are translating the language, L(S), of the system in another local language, L(τ ). As we will see in paper IV, the idea of translating one local language into another plays a central role in the discussion of composite systems and sub-systems [3].

Classical Physics in the Local Language L(S)
The quantum theory representation of L(S) is studied in papers II and III [1,2] of the present series. Here we will look at the concrete form of the expressions in the previous Section for the example of classical physics. In this case, for all systems S, and all classical representations, σ, the topos τ σ is Sets. This representation of L(S) has the following ingredients: 1. (a) The ground-type symbol Σ is represented by a symplectic manifold, Σ σ , that is the state-space for the system S.
(b) The ground-type symbol R is represented by the real line, i.e., R σ := IR.
(c) The type symbol P Σ is represented by the set, P Σ σ , of all subsets of the state space Σ σ . The type symbol P R is represented by the set, P IR, of all subsets of IR.

The term {s | A(s) ∈∆} of type P Σ (where∆ is a free variable of type P R) is represented by the function [[ {s |
for all ∆ ∈ P IR.

Adapting the Language L(S) to Other Types of Physical System
Our central contention in this series of papers is that (i) each physical system, S, can be equipped with a local language, L(S); and (ii) constructing an explicit theory of S in a particular theory-type is equivalent to finding a representation of L(S) in a topos which may well be other than the topos of sets.
There are many situations in which the language is independent of the theory-type, and then, for a given system S, the different topos representations of L(S), correspond to the application of the different theory-types to the same system S. We gave an example earlier of a point particle moving in three dimensions: the classical physics representation is in the topos Sets; and, as shown in papers II and III, the quantum theory representation is in the presheaf topos Sets V(L 2 (IR 3 , d 3 x)) .
However, there are other situations where the relationship between the language and its representations is more complicated than this. In particular, there is the critical question about what features of the theory should go into the language, and what into the representation. Adding new features would begin by adding to, or changing, the set of ground-type symbols which generally represent the entities that are going to be of generic interest (such as a state object or quantity-value object). In doing this, extra axioms may also be introduced to encode the properties that the new objects are expected to possess in all the representations that are of physical interest.
For example, suppose we want to use our formalism to discuss space-time physics: where does the information about the space-time go? If the subject is classical field theory in a curved space-time, then the topos τ is Sets, and the space-time manifold is part of the background structure. This makes it natural to have the manifold assumed in the representation; i.e., the information about the space-time is in the representation.
However, alternatively one can add a new ground type symbol, 'M', to the language, to serve as the linguistic progenitor of 'space-time'; thus M would have the same theoretical status as the symbols Σ and R. A function symbol ψ : M → R is then the progenitor of a physical field. In a representation φ, the object M φ plays the role of 'space-time' in the topos τ φ , and ψ φ : M φ → R φ is the representation of a field in this theory.
Of course, the language L(S) says nothing about what sort of entity M φ is, except in so far as such information is encoded in extra axioms. For example, if the subject is classical field theory, then τ φ = Sets, and M φ would be a standard differentiable manifold. On the other hand, if the topos τ φ admits 'infinitesimals', then M φ could be a manifold according to the language of synthetic differential geometry [13].
A fortiori, the same type of argument applies to the status of 'time' in a canonical theory. In particular, it is possible to add a ground type symbol, T , so that, in any representation, φ, the object T φ in the topos τ φ is the analogue of the 'time-line' for that theory. For standard physics in Sets we have T φ = IR, but the form of T φ in a more general topos, τ φ , would be a rich subject for speculation.
The addition of a 'time-type' symbol, T , to the language L(S) is a prime example of a situation where one might want to add extra axioms. These could involve ordering properties, or algebraic properties like those of an abelian group, and so on. These properties would be realised in any representation as the corresponding type of object in the topos τ φ . Thus abelian group axioms mean that T φ is an abelian-group object in τ φ ; total-ordering axioms for the time-type T mean that T φ is a totally-ordered object in τ φ , and so on.
As a rather interesting extension of this idea, one could have a space-time ground type symbol M, but then add the axioms for a partial ordering. In that case, M φ would be a poset-object in τ φ , which could be interpreted physically as the τ φ -analogue of a causal set [32].
Yet another possibility is to develop a language for history theories, and use it study the topos version of the consistent-histories approach to quantum theory.
We will return to some of these ideas in future publications.

Conclusion
In this paper, the first in a series, we have introduced the idea that a formal language can be attached to each physical system, and that constructing a theory of that system is equivalent to finding a representation of this language in an appropriate topos.
The long-term goal of this research programme is to provide a novel framework for constructing theories of physics in general; in particular, to construct theories that go 'beyond' standard quantum theory, and especially in the direction of quantum cosmology. In doing so, we have constructed a formalism that is not tied to the familiar use of Hilbert spaces, or formal path integrals, and which, therefore, need not assume a priori the use of continuum quantities in physics.
We have introduced two different types of language that can apply to a given system S. The first is the propositional language, PL(S), that deals only with propositions of the form "A ε ∆". The intention is represent these propositions in a Heyting algebra of sub-objects of some object in a topos that is identified as the analogue of a 'state space'. The simplest example is classical physics, where propositions are represented by the Boolean algebra of (Borel) subsets of the classical state space. The example of quantum theory is considerably more interesting and is discussed in detail in paper II [1].
The second type of language that we discussed is considerably more powerful. This is the 'local' language L(S) which includes symbols for the state object and quantityvalue object (and/or whatever theoretical entities are felt to be of representationindependent importance), as well as symbols for the physical quantities in the system. The key idea is that constructing a theory of S is equivalent is to finding a representation of this entire language (not just the propositional part) in a topos. As with PL(S), the language L(S) forms a deductive system that is based on intuitionistic logic: something that is naturally adapted to finding a representation in a topos.
Any theory of this type is necessarily 'neo-realist' in the sense that physical quantities are represented by arrows A φ : Σ φ → R φ ; and propositions are represented by sub-objects of Σ φ , the set of which is a Heyting algebra. In this sense, these toposbased theories all 'look' like classical physics, except of course that, generally speaking, the topos concerned is not Sets.

A.1 Presheaves on a Poset
Topos theory is a remarkably rich branch of mathematics which can be approached from a variety of different viewpoints. The basic area of mathematics is category theory; where, we recall, a category consists of a collection of objects and a collection of morphisms (or arrows).
In the special case of the category of sets, the objects are sets, and a morphism is a function between a pair of sets. In general, each morphism f in a category is associated with a pair of objects, known as its 'domain' and 'codomain', and is written as f : B → A where B and A are the domain and codomain respectively. Note that this arrow notation is used even if f is not a function in the normal set-theoretic sense.
A key ingredient in the definition of a category is that if f : B → A and g : C → B (i.e., the codomain of g is equal to the domain of f ) then f and g can be 'composed' to give an arrow f • g : C → A; in the case of the category of sets, this is just the usual composition of functions.
A simple example of a category is given by any partially-ordered set ('poset') C: (i) the objects are defined to be the elements of C; and (ii) if p, q ∈ C, a morphism from p to q is defined to exist if, and only if, p q in the poset structure. Thus, in a poset regarded as a category, there is at most one morphism between any pair of objects p, q ∈ C; if it exists, we shall write this morphism as i pq : p → q. This example is important for us in form of the 'category of contexts', V(H), in quantum theory (see papers II-IV). The objects in V(H) are the commutative, unital von Neumann subalgebras of the algebra, B(H), of all bounded operators on the Hilbert space H. (Unital means that all these algebras contain the identity operator1 ∈ B(H).) The definition of a topos. From our perspective, the most relevant feature of a topos, τ , is that it is a category which behaves in many ways like the category of sets [8,11]. Most of the precise details are not necessary for the present series of papers, but here we will list some of the most important ones for our purposes: 1. There is a terminal object 1 τ in τ ; this means that given any object A in the topos, there is a unique arrow A → 1 τ .
For any object A in the topos, an arrow 1 τ → A is called a global element 29 of A. The set of all global elements of A is denoted ΓA.
Given A, B ∈ Ob(τ ), there is a product A × B in τ . In fact, a topos always has pull-backs, and the product is just a special case of this. 30 29 In the category of sets, Sets, the terminal object 1 Sets is a singleton set { * }. It follows that the elements of ΓA are in one-to-one correspondence with the elements of A. 30 The conditions in 1. above are equivalent to saying that τ is finitely complete.
2. There is an initial object 0 τ in τ . This means that given any object A in the topos, there is a unique arrow 0 τ → A.
Given A, B ∈ Ob(τ ), there is a co-product A ⊔ B in τ . In fact, a topos always has push-outs, and the co-product is just a special case of this. 31 3. There is exponentiation: i.e., given objects A, B in τ we can form the object A B , which is the topos analogue of the set of functions from B to A in set theory. The definitive property of exponentiation is that, given any object C, there is an isomorphism that is natural in A and C.
The last item is of particular importance to us as it is the source of the Heyting algebras that we use so much. To explain what is meant, let us first consider the familiar topos, Sets, of sets. There, the subsets K ⊆ X of a set X are in one-to-one correspondence with functions χ K : X → {0, 1}, where χ K (x) = 1 if x ∈ K, and χ K (x) = 0 otherwise. Thus the target space {0, 1} can be regarded as the simplest 'false-true' Boolean algebra, and the mathematical proposition "x ∈ K" is true if χ K (x) = 1, and false otherwise.
In the case of a topos, τ , the sub-objects 32 K of an object X in the topos are in one-to-one correspondence with arrows χ K : X → Ω τ , where the special object Ω τcalled the 'sub-object classifier', or 'object of truth values'-plays an analogous role to that of {0, 1} in the category of sets.
An important property for us is that, in any topos τ , the collection, Sub(A), of subobjects of an object A forms a Heyting algebra. The reader is referred to the standard texts for proofs (for example, see [8], p151).
The idea of a presheaf. To illustrate the main ideas, we will first give a few definitions from the theory of presheaves on a partially ordered set (or 'poset'); in the case of quantum theory, this poset is the space of 'contexts' in which propositions are asserted. We shall then use these ideas to motivate the definition of a presheaf on a general category. Only the briefest of treatments is given here, and the reader is referred to the standard literature for more information [8,11].
A presheaf (also known as a varying set) X on a poset C is a function that assigns to each p ∈ C, a set X p ; and to each pair p q (i.e., i pq : p → q), a map X qp : X q → X p such that (i) X pp : X p → X p is the identity map id X p on X p , and (ii) whenever p q r, the composite map X r (A. 2) The notation X qp is shorthand for the more cumbersome X(i pq ); see below in the definition of a functor.
An arrow, or natural transformation η : X → Y between two presheaves X, Y on C is a family of maps η p : X p → Y p , p ∈ C, that satisfy the intertwining conditions whenever p q. This is equivalent to the commutative diagram A sub-object of a presheaf X is a presheaf K, with an arrow i : K → X such that (i) K p ⊆ X p for all p ∈ C; and (ii) for all p q, the map K qp : K q → K p is the restriction of X qp : X q → X p to the subset K q ⊆ X q . This is shown in the commutative diagram where the vertical arrows are subset inclusions.
The collection of all presheaves on a poset C forms a category, denoted Sets C op . The arrows/morphisms between presheaves in this category are defined as the arrows above.

A.2 Presheaves on a General Category
The ideas sketched above admit an immediate generalization to the theory of presheaves on an arbitrary 'small' category C (the qualification 'small' means that the collection of objects is a genuine set, as is the collection of all arrows/morphisms between any pair of objects). To make the necessary definition we first need the idea of a 'functor': 1. The idea of a functor: A central concept is that of a 'functor' between a pair of categories C and D. Broadly speaking, this is an arrow-preserving function from one category to the other. The precise definition is as follows.
Definition A.1 1. A covariant functor F from a category C to a category D is a function that assigns (a) to each C-object A, a D-object F A ; 2. A contravariant functor X from a category C to a category D is a function that assigns (a) to each C-object A, a D-object X A ; The connection with the idea of a presheaf on a poset is straightforward. As mentioned above, a poset C can be regarded as a category in its own right, and it is clear that a presheaf on the poset C is the same thing as a contravariant functor X from the category C to the category Sets of normal sets. Equivalently, it is a covariant functor from the 'opposite' category 33 C op to Sets. Clearly, (A.2) corresponds to the contravariant condition (A.7). Note that mathematicians usually call the objects in C 'stages of truth', or just 'stages'. For us they are 'contexts'.
2. Presheaves on an arbitrary category C: These remarks motivate the definition of a presheaf on an arbitrary small category C: namely, a presheaf on C is a covariant functor 34 X : C op → Sets from C op to the category of sets. Equivalently, a presheaf is a contravariant functor from C to the category of sets.
We want to make the collection of presheaves on C into a category, and therefore we need to define what is meant by a 'morphism' between two presheaves X and Y . The intuitive idea is that such a morphism from X to Y must give a 'picture' of X within Y . Formally, such a morphism is defined to be a natural transformation N : X → Y , by which is meant a family of maps (called the components of N) N A : X A → Y A , A ∈ Ob(C), such that if f : B → A is a morphism in C, then the composite map In other words, we have the 33 The 'opposite' of a category C is a category, denoted C op , whose objects are the same as those of C, and whose morphisms are defined to be the opposite of those of C; i.e., a morphism f : A → B in C op is said to exist if, and only if, there is a morphism f : B → A in C.
34 Throughout this series of papers, a presheaf is indicated by a letter that is underlined.
of which (A.4) is clearly a special case. The category of presheaves on C equipped with these morphisms is denoted Sets C op .
The idea of a sub-object generalizes in an obvious way. Thus we say that K is a sub-object of X if there is a morphism in the category of presheaves (i.e., a natural transformation) ι : K → X with the property that, for each A, the component map ι A : K A → X A is a subset embedding, i.e., K A ⊆ X A . Thus, if f : B → A is any morphism in C, we get the analogue of the commutative diagram (A.5): where, once again, the vertical arrows are subset inclusions.
The category of presheaves on C, Sets C op , forms a topos. We do not need the full definition of a topos; but we do need the idea, mentioned in Section A.1, that a topos has a sub-object classifier Ω, to which we now turn.
3. Sieves and the sub-object classifier Ω. Among the key concepts in presheaf theory is that of a 'sieve', which plays a central role in the construction of the sub-object classifier in the topos of presheaves on a category C.
A sieve on an object A in C is defined to be a collection S of morphisms f : B → A in C with the property that if f : B → A belongs to S, and if g : C → B is any morphism with co-domain B, then f • g : C → A also belongs to S. In the simple case where C is a poset, a sieve on p ∈ C is any subset S of C such that if r ∈ S then (i) r p, and (ii) r ′ ∈ S for all r ′ r; in other words, a sieve is nothing but a lower set in the poset.
The presheaf Ω : C → Sets is now defined as follows. If A is an object in C, then Ω A is defined to be the set of all sieves on A; and if f : where ↓B denotes the principal sieve on B, defined to be the set of all morphisms in C whose codomain is B. In words: the pull-back of any sieve on A by a morphism from B to A that belongs to the sieve, is the principal sieve on B.
If C is a poset, the pull-back operation corresponds to a family of maps Ω qp : Ω q → Ω p (where Ω p denotes the set of all sieves/lower sets on p in the poset) defined by Ω qp = Ω(i pq ) if i pq : p → q (i.e., p q). It is straightforward to check that if S ∈ Ω q , then Ω qp (S) :=↓ p ∩ S (A.12) where ↓ p := {r ∈ C | r p}.
A crucial property of sieves is that the set Ω A of sieves on A has the structure of a Heyting algebra. Specifically, Ω A is a Heyting algebra where the unit element 1 Ω A in Ω A is the principal sieve ↓A, and the null element 0 Ω A is the empty sieve ∅. The partial ordering in Ω A is defined by S 1 S 2 if, and only if, S 1 ⊆ S 2 ; and the logical connectives are defined as: S 1 ∧ S 2 := S 1 ∩ S 2 (A.13) S 1 ∨ S 2 := S 1 ∪ S 2 (A.14) S 1 ⇒ S 2 := {f : B → A | ∀ g : C → B if f • g ∈ S 1 then f • g ∈ S 2 }(A. 15) As in any Heyting algebra, the negation of an element S (called the pseudo-complement of S) is defined as ¬S := S ⇒ 0; so that ¬S := {f : B → A | for all g : C → B, f • g ∈ S}.
(A. 16) It can be shown that the presheaf Ω is a sub-object classifier for the topos Sets C op . That is to say, sub-objects of any object X in this topos (i.e., any presheaf on C) are in one-to-one correspondence with morphisms χ : X → Ω. This works as follows. First, let K be a sub-object of X. Then there is an associated characteristic morphism χ K : X → Ω, whose 'component' χ KA : X A → Ω A at each stage/context A in C is defined as for all x ∈ X A . That the right hand side of (A.17) actually is a sieve on A follows from the defining properties of a sub-object.
Thus, in each 'branch' of the category C going 'down' from the stage A, χ K A (x) picks out the first member B in that branch for which X(f )(x) lies in the subset K B , and the commutative diagram (A.9) then guarantees that X(h• f )(x) will lie in K C for all h : C → B. Thus each stage A in C serves as a possible context for an assignment to each x ∈ X A of a generalised truth value-a sieve belonging to the Heyting algebra Ω A . This is the sense in which contextual, generalised truth values arise naturally in a topos of presheaves.
There is a converse to (A.17): namely, each morphism χ : X → Ω (i.e., a natural transformation between the presheaves X and Ω) defines a sub-object K χ of X via at each stage A.

Global elements of a presheaf:
We recall that, in any topos, τ , a terminal object is defined to be an object 1 τ with the property that, for any object X in the category, there is a unique morphism X → 1 τ ; it is easy to show that terminal objects are unique up to isomorphism. A global element of an object X is then defined to be any morphism s : 1 τ → X. The motivation for this nomenclature is that, in the case of the category of sets, a terminal object is any singleton set { * }; and then it is true that there is a one-to-one correspondence between the elements of a set X and functions from { * } to X.
For the category of presheaves on C, a terminal object 1 : C → Sets can be defined by 1 A := { * } at all stages A in C; if f : B → A is a morphism in C then 1(f ) : { * } → { * } is defined to be the map * → * . This is indeed a terminal object since, for any presheaf X, we can define a unique natural transformation N : X → 1 whose components N A : X(A) → 1 A = { * } are the constant maps x → * for all x ∈ X A .
A global element of a presheaf X is also called a global section. As a morphism γ : 1 → X in the topos Sets C op , a global element corresponds to a choice of an element γ A ∈ X A for each stage A in C, such that, if f : B → A, the 'matching condition' is satisfied.