Artículos con la etiqueta ‘teoría de las categorías’

Topos Semantics for Higher-Order Modal Logic

Por • 6 mar, 2014 • Category: Educacion

We define the notion of a model of higher-order modal logic in an arbitrary elementary topos E . In contrast to the well-known interpretation of (non-modal) higher-order logic, the type of propositions is not interpreted by the subobject classifier ΩE , but rather by a suitable complete Heyting algebra H . The canonical map relating H and ΩE both serves to interpret equality and provides a modal operator on H in the form of a comonad. Examples of such structures arise from surjective geometric morphisms f:F→E , where H=f∗ΩF . The logic differs from non-modal higher-order logic in that the principles of functional and propositional extensionality are no longer valid but may be replaced by modalized versions. The usual Kripke, neighborhood, and sheaf semantics for propositional and first-order modal logic are subsumed by this notion.

Scheme representation for first-order logic

Por • 13 feb, 2014 • Category: Educacion

Although contemporary model theory has been called “algebraic geometry minus fields”, the formal methods of the two fields are radically different. This dissertation aims to shrink that gap by presenting a theory of logical schemes, geometric entities which relate to first-order logical theories in much the same way that algebraic schemes relate to commutative rings. The construction relies on a Grothendieck-style representation theorem which associates every coherent or classical first-order theory with an affine scheme: a topological groupoid (the spectrum of the theory) together with a sheaf of (local) syntactic categories.

Chasing diagrams in cryptography

Por • 1 feb, 2014 • Category: Opinion

Cryptography is a theory of secret functions. Category theory is a general theory of functions. Cryptography has reached a stage where its structures often take several pages to define, and its formulas sometimes run from page to page. Category theory has some complicated definitions as well, but one of its specialties is taming the flood of structure. Cryptography seems to be in need of high level methods, whereas category theory always needs concrete applications. So why is there no categorical cryptography? One reason may be that the foundations of modern cryptography are built from probabilistic polynomial-time Turing machines, and category theory does not have a good handle on such things. On the other hand, such foundational problems might be the very reason why cryptographic constructions often resemble low level machine programming. I present some preliminary explorations towards categorical cryptography. It turns out that some of the main security concepts are easily characterized through the categorical technique of *diagram chasing*, which was first used Lambek’s seminal `Lecture Notes on Rings and Modules’.

Category theory, logic and formal linguistics: some connections, old and new

Por • 30 ene, 2014 • Category: Crítica

We seize the opportunity of the publication of selected papers from the \emph{Logic, categories, semantics} workshop in the \emph{Journal of Applied Logic} to survey some current trends in logic, namely intuitionistic and linear type theories, that interweave categorical, geometrical and computational considerations. We thereafter present how these rich logical frameworks can model the way language conveys meaning.

Category Theory Using String Diagrams

Por • 30 ene, 2014 • Category: Ciencia y tecnología

In work of Fokkinga and Meertens a calculational approach to category theory is developed. The scheme has many merits, but sacrifices useful type information in the move to an equational style of reasoning. By contrast, traditional proofs by diagram pasting retain the vital type information, but poorly express the reasoning and development of categorical proofs. In order to combine the strengths of these two perspectives, we propose the use of string diagrams, common folklore in the category theory community, allowing us to retain the type information whilst pursuing a calculational form of proof. These graphical representations provide a topological perspective on categorical proofs, and silently handle functoriality and naturality conditions that require awkward bookkeeping in more traditional notation.

Arrow’s Theorem by Arrow Theory

Por • 21 ene, 2014 • Category: Filosofía

We give a categorical account of Arrow’s theorem, a seminal result in social choice theory.

Logical systems II: Free semantics

Por • 15 ene, 2014 • Category: Crítica

This paper is a sequel to “Logical systems I: Lambda calculi through discreteness”. It provides a general 2-categorical setting for extensional calculi and shows how intensional and extensional calculi can be related in logical systems. We focus on transporting the notion of Day convolution to a 2-categorical framework, and as a complementary result we prove the convolution theorem for internal categories. We define the concept of Yoneda triangle, and show how objects in a Yoneda bitriangle get extensional semantics “for free”. This includes the usual semantics for propositional calculi, Kripke semantics for intuitionistic calculi and ternary frame semantics for substructural calculi including Lambek’s lambda calculi, relevance and linear logics. We show how in this setting, one may use a model-theoretic logic to induce a structure of a proof-theoretic logic.

Arithmetical Foundations – Excerpt

Por • 31 dic, 2013 • Category: Crítica

Recursive maps, nowadays called primitive recursive maps, PR maps, have been introduced by G\”odel in his 1931 article for the arithmetisation, g\”odelisation, of metamathematics. For construction of his undecidable formula he introduces a non-constructive, non-recursive predicate beweisbar, provable. Staying within the area of categorical free-variables theory PR of primitive recursion or appropriate extensions opens the chance to avoid the two (original) G\”odel’s incompleteness theorems: these are stated for Principia Mathematica und verwandte Systeme, “related systems” such as in particular Zermelo-Fraenkel set theory ZF and v. Neumann G\”odel Bernays set theory NGB. On the basis of primitive recursion we consider \mu-recursive maps as partial pr maps. Special terminating general recursive maps considered are complexity controlled iterations. Map code evaluation is then given in terms of such an iteration. We discuss iterative pr map code evaluation versus termination conditioned soundness and based on this decidability of primitive recursive predicates.

Categories within the Foundation of Mathematics

Por • 27 dic, 2013 • Category: Educacion

The recent trend in mathematics is towards a framework of abstract mathematical objects, rather than the more concrete approach of explicitly defining elements which objects were thought to consist of. A natural question to raise is whether this sort of abstract approach advocated for by Lawvere, among others, is foundational in the sense that it provides a unified, universal, system of first order axioms in which we can define the usual mathematical objects and prove their usual properties. In this way, we view the “foundation” as something without any necessary justification or starting point. Some of the main arguments for categories as such a structure are laid out by MacLane as he argues that the set-theoretic constructions are inappropriate for current mathematics as practices, and that they are inadequate to properly encompass category theory itself and therefore cannot properly encompass all of mathematics, while category theory can be used to describe set theory and all the natural consequences of a given primitive system.
arXiv:1312.6198v1 [math.LO]

On ground model definability

Por • 6 dic, 2013 • Category: Opinion

Laver, and Woodin independently, showed that models of ZFC are uniformly definable in their set-forcing extensions, using a ground model parameter. We investigate ground model definability for models of fragments of ZFC , particularly of ZF+DC δ and of ZFC − , and we obtain both positive and negative results. Generalizing the results of Laver and Woodin, we show that models of ZF+DC δ are uniformly definable in their set-forcing extensions by posets admitting a gap at δ , using a ground model parameter. In particular, this means that models of ZF+DC δ are uniformly definable in their forcing extensions by posets of size less than δ . We also show that it is consistent for ground model definability to fail for models of ZFC − of the form H κ + . Using forcing, we produce a ZFC universe in which there is a cardinal κ>>ω such that H κ + is not definable in its Cohen forcing extension. As a corollary, we show that there is always a countable transitive model of ZFC − violating ground model definability. These results turn out to have a bearing on ground model definability for models of ZFC . It follows from our proof methods that the hereditary size of the parameter that Woodin used to define a ZFC model in its set-forcing extension is best possible.