The Logic and Computation Group is composed of faculty and graduate students from the Computer and Information Science, Mathematics, and Philosophy departments, and participates in the Institute for Research in the Cognitive Sciences. The Logic and Computation group runs a weekly seminar. The seminar is open to the public and all are welcome.
The seminar meets regularly during the school year on Mondays at 4:30 p.m. in room DRL 4C8 on the fourth (top) floor of the David Rittenhouse Laboratory (DRL), on the Southeast corner of 33-rd and Walnut Streets at the University of Pennsylvania. Directions may be found here. Any changes to this venue or schedule will be specifically noted.
Girard's linear logic, Lukasiewicz logic (and several modal logics) have an intriguing simultaneous interpretation. It uses the co-universal characterization of closed intervals that arises from the search for a co-inductive approach to infinite precision real analysis.
The Axiom of Determinacy is associated with a game of perfect information, in which two players take turns choosing natural numbers. Associated with the game is a rule defining the conditions under which each player wins. If one player has a winning strategy, the game is said to be determined; the Axiom of Determinacy states that all such games are determined.
The axiom has important consequences for the real numbers: it implies that every set of real numbers is Lebesgue measurable and has the Baire property. The axiom is also intimately related to large cardinals. For example, it implies the existence of an inner model of L(R) with infinitely many Woodin cardinals.
The talk will begin with a rigorous definition of the Axiom of Determinacy. Some elementary consequences of the axiom will then be discussed. The talk should be interesting to both logicians and non-logicians.
In 1961 Robert Vaught published a ground breaking paper on countable model theory entitled "Denumerable Models of Complete Theories". In this paper he set out many of the fundamental results concerning countable model theory. At the end of the this paper he made a conjecture that every countable first order theory in every model of set theory had either countably or continuum many countable models. This conjecture is what is now called "Vaught's Conjecture" and is one of the oldest open problems in model theory.
Over the years there have been several variants of Vaught's Conjecture which have been shown to be equivalent to it or to be implied by it. In the first part of this series of talks we will show that Vaught's Conjecture is equivalent to the following statement: "If a countable first order theory T does not have a perfect kernel of countable models, then every model of T is isomorphic to a model in L[T]." In other words, if there isn't a natural relationship between the countable models of T and the real numbers (as in for example the theory (Z, Succ, O, P) where P is some subset of Z) then the countable models of T are independent of the set theory you are working in (for example the theory of algebraically closed fields of characteristic 0). We call a sentence of L_{omega_1, omega} which does not have a perfect kernel of models "scattered". So Vaught's Conjecture, whether true or false, has important implications for the connections between set theory and countable model theory. We will show that these two statements of Vaught's Conjecture are equivalent by constructing what is known as the Vaught tree for any sentence of L_{omega_1, omega} and discussing properties of this tree.
The second part of this series of talks will then focus on presenting the ideas behind the central result of my dissertation, that for every countable ordinal alpha there is a scattered sentence of L_{omega_1, omega} of quantifier rank omega which has a Vaught tree of at least height alpha.
In 1961 Robert Vaught published a ground breaking paper on countable model theory entitled "Denumerable Models of Complete Theories". In this paper he set out many of the fundamental results concerning countable model theory. At the end of the this paper he made a conjecture that every countable first order theory in every model of set theory had either countably or continuum many countable models. This conjecture is what is now called "Vaught's Conjecture" and is one of the oldest open problems in model theory.
Over the years there have been several variants of Vaught's Conjecture which have been shown to be equivalent to it or to be implied by it. In the first part of this series of talks we will show that Vaught's Conjecture is equivalent to the following statement: "If a countable first order theory T does not have a perfect kernel of countable models, then every model of T is isomorphic to a model in L[T]." In other words, if there isn't a natural relationship between the countable models of T and the real numbers (as in for example the theory (Z, Succ, O, P) where P is some subset of Z) then the countable models of T are independent of the set theory you are working in (for example the theory of algebraically closed fields of characteristic 0). We call a sentence of L_{omega_1, omega} which does not have a perfect kernel of models "scattered". So Vaught's Conjecture, whether true or false, has important implications for the connections between set theory and countable model theory. We will show that these two statements of Vaught's Conjecture are equivalent by constructing what is known as the Vaught tree for any sentence of L_{omega_1, omega} and discussing properties of this tree.
The second part of this series of talks will then focus on presenting the ideas behind the central result of my dissertation, that for every countable ordinal alpha there is a scattered sentence of L_{omega_1, omega} of quantifier rank omega which has a Vaught tree of at least height alpha.
In 1961 Robert Vaught published a ground breaking paper on countable model theory entitled "Denumerable Models of Complete Theories". In this paper he set out many of the fundamental results concerning countable model theory. At the end of the this paper he made a conjecture that every countable first order theory in every model of set theory had either countably or continuum many countable models. This conjecture is what is now called "Vaught's Conjecture" and is one of the oldest open problems in model theory.
Over the years there have been several variants of Vaught's Conjecture which have been shown to be equivalent to it or to be implied by it. In the first part of this series of talks we will show that Vaught's Conjecture is equivalent to the following statement: "If a countable first order theory T does not have a perfect kernel of countable models, then every model of T is isomorphic to a model in L[T]." In other words, if there isn't a natural relationship between the countable models of T and the real numbers (as in for example the theory (Z, Succ, O, P) where P is some subset of Z) then the countable models of T are independent of the set theory you are working in (for example the theory of algebraically closed fields of characteristic 0). We call a sentence of L_{omega_1, omega} which does not have a perfect kernel of models "scattered". So Vaught's Conjecture, whether true or false, has important implications for the connections between set theory and countable model theory. We will show that these two statements of Vaught's Conjecture are equivalent by constructing what is known as the Vaught tree for any sentence of L_{omega_1, omega} and discussing properties of this tree.
The second part of this series of talks will then focus on presenting the ideas behind the central result of my dissertation, that for every countable ordinal alpha there is a scattered sentence of L_{omega_1, omega} of quantifier rank omega which has a Vaught tree of at least height alpha.
In this talk we will show, using the method of forcing, that the axiom of choice is independent of the other axioms of set theory. We will then also consider other results using the method of forcing.
The Continuum Hypothesis says that "Any uncountable subset of the real numbers is equinumerous with all of the real numbers". This statement was first proposed by Cantor in the late 1890's and was considered so fundamentally important that it was listed as the first among Hilbert's famous twenty-three open problems.
In 1940 Kurt Goedel showed, via his construction of the inner model L, that that the Continuum Hypothesis was consistent with the other axiom of ZFC. However, in 1963, Cohen proved that the Continuum Hypothesis was not just consistent with the axioms of ZFC but was in fact independent of them. His proof made the Continuum Hypothesis the first example of a mathematically important statement which couldn't be decided by the standard axioms of set theory.
The methods used in showing the independence of the continuum hypothesis gave rise to several of the most important ideas in modern set theory. In this series of talks we will introduce these important ideas and prove the independence of the Continuum Hypothesis from ZFC.
In the fifth part of this series we will complete the proof that the Continuum Hypothesis can't be proved from the other axioms of set theory.
Although there is an abundance of known properties independent of the usual axioms of set theory ZFC, only relatively few of them concern the objects taught in calculus courses. In this talk we discuss two such examples. The first concerns multivariable calculus and is related to Fubini theorem: When the existence of iterated integrals of a function f(x,y) implies that the resulting value is independent of the order of integration? The second concerns continuously differentiable functions from the interval I=[0,1] to itself: Is it possible that a set of such functions that cover the unit square has fewer elements than the set of real numbers? The talk will be fairly elementary.
Although there is an abundance of known properties independent of the usual axioms of set theory ZFC, only relatively few of them concern the objects taught in calculus courses. In this talk we discuss two such examples. The first concerns multivariable calculus and is related to Fubini theorem: When the existence of iterated integrals of a function f(x,y) implies that the resulting value is independent of the order of integration? The second concerns continuously differentiable functions from the interval I=[0,1] to itself: Is it possible that a set of such functions that cover the unit square has fewer elements than the set of real numbers? The talk will be fairly elementary.
We present a revisited semantics for multiset rewriting founded on the left sequent rules of linear logic in its DILL presentation. The resulting interpretation is extended with a majority of linear connectives into the language of omega-multisets. It drops the distinction between multiset elements and rewrite rules, and considerably enriches the expressive power of standard multiset rewriting with embedded rules, choice, replication and more. The cut rules introduce finite auxiliary rewriting chains and are admissible. Derivations are now primarily viewed as open objects, and are closed only to examine intermediate rewriting states. The resulting language can also be interpreted as a process algebra. A simple translation maps process constructors of the asynchronous pi-calculus to rewrite operators, while the structural equivalence correspond directly to logically-motivated structural properties of omega-multisets (with one exception). The language of omega-multisets forms the basis for the security protocol specification language MSR 3. With relations to both multiset rewriting and process algebra, it supports specifications that are process-based, state-based, or of a mixed nature. Additionally, its deep logical underpinning makes it an ideal common ground for systematically comparing protocol specification languages, a task currently done in an ad-hoc manner.
Modal logics of knowledge have been proposed as a formalism for the study of information flow in distributed and multi-agent systems. In particular, the notion of knowledge-based programs, in which agents condition their actions on formulas expressing what they know, has been argued to provide a level of abstraction that leads to simple correctness proofs, an ability to capture commonalities between protocols that operate under different environmental assumptions, and the ability to specify that information accesible to the agents is used in an optimal way.
Knowledge-based programs cannot be directly executed, however, but are better understood as specifications that can be said to be satisfied by concrete implementations. This leads to the problems of verification and synthesis for knowledge-based programs. The talk will survey work on the algorithmic solution of these problems, their implementation in the model checker MCK, which uses symbolic techniques (BDD's) to mmodel check specifications in the logic of knwoeldge and time. An application of this system to the analysis of cache coherency will be discussed which has automatically identified a non-optimal behavior of the Synapse protocol.
The Continuum Hypothesis says that "Any uncountable subset of the real numbers is equinumerous with all of the real numbers". This statement was first proposed by Cantor in the late 1890's and was considered so fundamentally important that it was listed as the first among Hilbert's famous twenty-three open problems.
In 1940 Kurt Goedel showed, via his construction of the inner model L, that that the Continuum Hypothesis was consistent with the other axiom of ZFC. However, in 1963, Cohen proved that the Continuum Hypothesis was not just consistent with the axioms of ZFC but was in fact independent of them. His proof made the Continuum Hypothesis the first example of a mathematically important statement which couldn't be decided by the standard axioms of set theory.
The methods used in showing the independence of the continuum hypothesis gave rise to several of the most important ideas in modern set theory. In this series of talks we will introduce these important ideas and prove the independence of the Continuum Hypothesis from ZFC.
In the fourth part of this series we will complete the proof that the Continuum Hypothesis can't be proved from the other axioms of set theory.
The Continuum Hypothesis says that "Any uncountable subset of the real numbers is equinumerous with all of the real numbers". This statement was first proposed by Cantor in the late 1890's and was considered so fundamentally important that it was listed as the first among Hilbert's famous twenty-three open problems.
In 1940 Kurt Goedel showed, via his construction of the inner model L, that that the Continuum Hypothesis was consistent with the other axiom of ZFC. However, in 1963, Cohen proved that the Continuum Hypothesis was not just consistent with the axioms of ZFC but was in fact independent of them. His proof made the Continuum Hypothesis the first example of a mathematically important statement which couldn't be decided by the standard axioms of set theory.
The methods used in showing the independence of the continuum hypothesis gave rise to several of the most important ideas in modern set theory. In this series of talks we will introduce these important ideas and prove the independence of the Continuum Hypothesis from ZFC.
In the third part of this series we will continue use Cohen's method of forcing to show that the Continuum Hypothesis can't be proved from the other axioms of set theory.
The Continuum Hypothesis says that "Any uncountable subset of the real numbers is equinumerous with all of the real numbers". This statement was first proposed by Cantor in the late 1890's and was considered so fundamentally important that it was listed as the first among Hilbert's famous twenty-three open problems.
In 1940 Kurt Goedel showed, via his construction of the inner model L, that that the Continuum Hypothesis was consistent with the other axiom of ZFC. However, in 1963, Cohen proved that the Continuum Hypothesis was not just consistent with the axioms of ZFC but was in fact independent of them. His proof made the Continuum Hypothesis the first example of a mathematically important statement which couldn't be decided by the standard axioms of set theory.
The methods used in showing the independence of the continuum hypothesis gave rise to several of the most important ideas in modern set theory. In this series of talks we will introduce these important ideas and prove the independence of the Continuum Hypothesis from ZFC.
In the second part of this series we will use Cohen's method of forcing to show that the Continuum Hypothesis can't be proved from the other axioms of set theory.
We present a novel approach for proving secrecy properties of security protocols by mechanized flow analysis. In contrast to existing tools for proving secrecy by abstract interpretation, our tool enjoys cryptographic soundness in the strong sense of blackbox reactive simulatability/UC which entails that secrecy properties proven by our tool are automatically guaranteed to hold for secure cryptographic implementations of the analyzed protocol, with respect to the more fine-grained cryptographic secrecy definitions and adversary models.
Our tool is capable of reasoning about a comprehensive language for expressing protocols, in particular handling symmetric encryption and asymmetric encryption, and it produces proofs for an unbounded number of sessions in the presence of an active adversary. We have implemented the tool and applied it to a number of common protocols from the literature.
The Continuum Hypothesis says that "Any uncountable subset of the real numbers is equinumerous with all of the real numbers". This statement was first proposed by Cantor in the late 1890's and was considered so fundamentally important that it was listed as the first among Hilbert's famous twenty-three open problems.
In 1940 Kurt Goedel showed, via his construction of the inner model L, that that the Continuum Hypothesis was consistent with the other axiom of ZFC. However, in 1963, Cohen proved that the Continuum Hypothesis was not just consistent with the axioms of ZFC but was in fact independent of them. His proof made the Continuum Hypothesis the first example of a mathematically important statement which couldn't be decided by the standard axioms of set theory.
The methods used in showing the independence of the continuum hypothesis gave rise to several of the most important ideas in modern set theory. In this series of talks we will introduce these important ideas and prove the independence of the Continuum Hypothesis from ZFC.
In the first half of this series we will introduce Cohen's method of forcing and use this method to show that the Continuum Hypothesis can't be proved from the other axioms of set theory.
Continuing our exposition from last week, today we prove Lindstrom's Theorem.
Two of the properties satisfied by first-order logic which make it so useful for describing mathematical structures are the Lowenheim-Skolem property and Compactness. These properties allow us to use first-order logic to study infinite structures without concern for the underlying universe in which these structures occur.
As these two properties are so important, we might ask what other abstract logics satisfy these properties? And is it possible to find a logic with more expressive power than first-order logic which also has these properties? In one of the most significant results in the study of abstract logics, Lindstrom showed that among all abstract logics which satisfy Compactness, the Lowenheim-Skolem property, and are closed under negation and conjugation, first-order logic is maximal.
In this expository talk we will introduce the notions of abstract logic, compactness, and the Lowenheim-Skolem property, and then we will prove Lindstrom's Theorem.