-
Constructive S4 modal logics with the finite birelational frame property
Authors:
Philippe Balbiani,
Martín Diéguez,
David Fernández-Duque,
Brett McLean
Abstract:
The logics $\mathsf{CS4}$ and $\mathsf{IS4}$ are the two leading intuitionistic variants of the modal logic $\mathsf{S4}$. Whether the finite model property holds for each of these logics have been long-standing open problems. It was recently shown that $\mathsf{IS4}$ has the finite frame property and thus the finite model property. In this paper, we prove that $\mathsf{CS4}$ also enjoys the finit…
▽ More
The logics $\mathsf{CS4}$ and $\mathsf{IS4}$ are the two leading intuitionistic variants of the modal logic $\mathsf{S4}$. Whether the finite model property holds for each of these logics have been long-standing open problems. It was recently shown that $\mathsf{IS4}$ has the finite frame property and thus the finite model property. In this paper, we prove that $\mathsf{CS4}$ also enjoys the finite frame property.
Additionally, we investigate the following three logics closely related to $\mathsf{IS4}$. The logic $\mathsf{GS4}$ is obtained by adding the Gödel--Dummett axiom to $\mathsf{IS4}$; it is both a superintuitionistic and a fuzzy logic and has previously been given a real-valued semantics. We provide an alternative birelational semantics and prove strong completeness with respect to this semantics. The extension $\mathsf{GS4^c}$ of $\mathsf{GS4}$ corresponds to requiring a crisp accessibility relation on the real-valued semantics. We give a birelational semantics corresponding to an extra confluence condition on the $\mathsf{GS4}$ birelational semantics and prove strong completeness. Neither of these two logics have the finite model property with respect to their real-valued semantics, but we prove that they have the finite frame property for their birelational semantics. Establishing the finite birelational frame property immediately establishes decidability, which was previously open for these two logics. Our proofs yield NEXPTIME upper bounds. The logic $\mathsf{S4I}$ is obtained from $\mathsf{IS4}$ by reversing the roles of the modal and intuitionistic relations in the birelational semantics. We also prove the finite frame property, and thereby decidability, for $\mathsf{S4I}$
△ Less
Submitted 15 March, 2024; v1 submitted 29 February, 2024;
originally announced March 2024.
-
Specific versus General Principles for Constitutional AI
Authors:
Sandipan Kundu,
Yuntao Bai,
Saurav Kadavath,
Amanda Askell,
Andrew Callahan,
Anna Chen,
Anna Goldie,
Avital Balwit,
Azalia Mirhoseini,
Brayden McLean,
Catherine Olsson,
Cassie Evraets,
Eli Tran-Johnson,
Esin Durmus,
Ethan Perez,
Jackson Kernion,
Jamie Kerr,
Kamal Ndousse,
Karina Nguyen,
Nelson Elhage,
Newton Cheng,
Nicholas Schiefer,
Nova DasSarma,
Oliver Rausch,
Robin Larson
, et al. (11 additional authors not shown)
Abstract:
Human feedback can prevent overtly harmful utterances in conversational models, but may not automatically mitigate subtle problematic behaviors such as a stated desire for self-preservation or power. Constitutional AI offers an alternative, replacing human feedback with feedback from AI models conditioned only on a list of written principles. We find this approach effectively prevents the expressi…
▽ More
Human feedback can prevent overtly harmful utterances in conversational models, but may not automatically mitigate subtle problematic behaviors such as a stated desire for self-preservation or power. Constitutional AI offers an alternative, replacing human feedback with feedback from AI models conditioned only on a list of written principles. We find this approach effectively prevents the expression of such behaviors. The success of simple principles motivates us to ask: can models learn general ethical behaviors from only a single written principle? To test this, we run experiments using a principle roughly stated as "do what's best for humanity". We find that the largest dialogue models can generalize from this short constitution, resulting in harmless assistants with no stated interest in specific motivations like power. A general principle may thus partially avoid the need for a long list of constitutions targeting potentially harmful behaviors. However, more detailed constitutions still improve fine-grained control over specific types of harms. This suggests both general and specific principles have value for steering AI safely.
△ Less
Submitted 20 October, 2023;
originally announced October 2023.
-
Complete representation by partial functions for signatures containing antidomain restriction
Authors:
Brett McLean
Abstract:
We investigate notions of complete representation by partial functions, where the operations in the signature include antidomain restriction and may include composition, intersection, update, preferential union, domain, antidomain, and set difference. When the signature includes both antidomain restriction and intersection, the join-complete and the meet-complete representations coincide. Otherwis…
▽ More
We investigate notions of complete representation by partial functions, where the operations in the signature include antidomain restriction and may include composition, intersection, update, preferential union, domain, antidomain, and set difference. When the signature includes both antidomain restriction and intersection, the join-complete and the meet-complete representations coincide. Otherwise, for the signatures we consider, meet-complete is strictly stronger than join-complete. A necessary condition to be meet-completely representable is that the atoms are separating. For the signatures we consider, this condition is sufficient if and only if composition is not in the signature. For each of the signatures we consider, the class of (meet-)completely representable algebras is not axiomatisable by any existential-universal-existential first-order theory. For 14 expressively distinct signatures, we show, by giving an explicit representation, that the (meet-)completely representable algebras form a basic elementary class, axiomatisable by a universal-existential-universal first-order sentence. The signatures we axiomatise are those containing antidomain restriction and any of intersection, update, and preferential union and also those containing antidomain restriction, composition, and intersection and any of update, preferential union, domain, and antidomain.
△ Less
Submitted 18 July, 2023;
originally announced July 2023.
-
Gödel-Dummett linear temporal logic
Authors:
Juan Pablo Aguilera,
Martín Diéguez,
David Fernández-Duque,
Brett McLean
Abstract:
We investigate a version of linear temporal logic whose propositional fragment is Gödel-Dummett logic (which is well known both as a superintuitionistic logic and a t-norm fuzzy logic). We define the logic using two natural semantics: first a real-valued semantics, where statements have a degree of truth in the real unit interval and second a `bi-relational' semantics. We then show that these two…
▽ More
We investigate a version of linear temporal logic whose propositional fragment is Gödel-Dummett logic (which is well known both as a superintuitionistic logic and a t-norm fuzzy logic). We define the logic using two natural semantics: first a real-valued semantics, where statements have a degree of truth in the real unit interval and second a `bi-relational' semantics. We then show that these two semantics indeed define one and the same logic: the statements that are valid for the real-valued semantics are the same as those that are valid for the bi-relational semantics. This Gödel temporal logic does not have any form of the finite model property for these two semantics: there are non-valid statements that can only be falsified on an infinite model. However, by using the technical notion of a quasimodel, we show that every falsifiable statement is falsifiable on a finite quasimodel, yielding an algorithm for deciding if a statement is valid or not. Later, we strengthen this decidability result by giving an algorithm that uses only a polynomial amount of memory, proving that Gödel temporal logic is PSPACE-complete. We also provide a deductive calculus for Gödel temporal logic, and show this calculus to be sound and complete for the above-mentioned semantics, so that all (and only) the valid statements can be proved with this calculus.
△ Less
Submitted 27 June, 2023;
originally announced June 2023.
-
Preservation theorems for Tarski's relation algebra
Authors:
Bart Bogaerts,
Balder ten Cate,
Brett McLean,
Jan Van den Bussche
Abstract:
We investigate a number of semantically defined fragments of Tarski's algebra of binary relations, including the function-preserving fragment. We address the question whether they are generated by a finite set of operations. We obtain several positive and negative results along these lines. Specifically, the homomorphism-safe fragment is finitely generated (both over finite and over arbitrary stru…
▽ More
We investigate a number of semantically defined fragments of Tarski's algebra of binary relations, including the function-preserving fragment. We address the question whether they are generated by a finite set of operations. We obtain several positive and negative results along these lines. Specifically, the homomorphism-safe fragment is finitely generated (both over finite and over arbitrary structures). The function-preserving fragment is not finitely generated (and, in fact, not expressible by any finite set of guarded second-order definable function-preserving operations). Similarly, the total-function-preserving fragment is not finitely generated (and, in fact, not expressible by any finite set of guarded second-order definable total-function-preserving operations). In contrast, the forward-looking function-preserving fragment is finitely generated by composition, intersection, antidomain, and preferential union. Similarly, the forward-and-backward-looking injective-function-preserving fragment is finitely generated by composition, intersection, antidomain, inverse, and an `injective union' operation.
△ Less
Submitted 11 April, 2024; v1 submitted 8 May, 2023;
originally announced May 2023.
-
EXPTIME-hardness of higher-dimensional Minkowski spacetime
Authors:
Robin Hirsch,
Brett McLean
Abstract:
We prove the EXPTIME-hardness of the validity problem for the basic temporal logic on Minkowski spacetime with more than one space dimension. We prove this result for both the lightspeed-or-slower and the slower-than-light accessibility relations (and for both the irreflexive and the reflexive versions of these relations). As an auxiliary result, we prove the EXPTIME-hardness of validity on any fr…
▽ More
We prove the EXPTIME-hardness of the validity problem for the basic temporal logic on Minkowski spacetime with more than one space dimension. We prove this result for both the lightspeed-or-slower and the slower-than-light accessibility relations (and for both the irreflexive and the reflexive versions of these relations). As an auxiliary result, we prove the EXPTIME-hardness of validity on any frame for which there exists an embedding of the infinite complete binary tree satisfying certain conditions. The proof is by a reduction from the two-player corridor-tiling game.
△ Less
Submitted 14 June, 2022;
originally announced June 2022.
-
A Gödel Calculus for Linear Temporal Logic
Authors:
Juan Pablo Aguilera,
Martín Diéguez,
David Fernández-Duque,
Brett McLean
Abstract:
We consider Gödel temporal logic ($\sf GTL$), a variant of linear temporal logic based on Gödel--Dummett propositional logic. In recent work, we have shown this logic to enjoy natural semantics both as a fuzzy logic and as a superintuitionistic logic. Using semantical methods, the logic was shown to be {\sc pspace}-complete. In this paper we provide a deductive calculus for $\sf GTL$, and show thi…
▽ More
We consider Gödel temporal logic ($\sf GTL$), a variant of linear temporal logic based on Gödel--Dummett propositional logic. In recent work, we have shown this logic to enjoy natural semantics both as a fuzzy logic and as a superintuitionistic logic. Using semantical methods, the logic was shown to be {\sc pspace}-complete. In this paper we provide a deductive calculus for $\sf GTL$, and show this calculus to be sound and complete for the above-mentioned semantics.
△ Less
Submitted 10 May, 2022;
originally announced May 2022.
-
Time and Gödel: Fuzzy temporal reasoning in PSPACE
Authors:
Juan Pablo Aguilera,
Martín Diéguez,
David Fernández-Duque,
Brett McLean
Abstract:
We investigate a non-classical version of linear temporal logic whose propositional fragment is Gödel--Dummett logic (which is well known both as a superintuitionistic logic and a t-norm fuzzy logic). We define the logic using two natural semantics, a real-valued semantics and a bi-relational semantics, and show that these indeed define one and the same logic. Although this Gödel temporal logic do…
▽ More
We investigate a non-classical version of linear temporal logic whose propositional fragment is Gödel--Dummett logic (which is well known both as a superintuitionistic logic and a t-norm fuzzy logic). We define the logic using two natural semantics, a real-valued semantics and a bi-relational semantics, and show that these indeed define one and the same logic. Although this Gödel temporal logic does not have any form of the finite model property for these two semantics, we show that every falsifiable formula is falsifiable on a finite quasimodel, which yields decidability of the logic. We then strengthen this result by showing that this Gödel temporal logic is PSPACE-complete.
△ Less
Submitted 1 May, 2022;
originally announced May 2022.
-
Difference-restriction algebras of partial functions with operators: discrete duality and completion
Authors:
Célia Borlido,
Brett McLean
Abstract:
We exhibit an adjunction between a category of abstract algebras of partial functions and a category of set quotients. The algebras are those atomic algebras representable as a collection of partial functions closed under relative complement and domain restriction; the morphisms are the complete homomorphisms. This generalises the discrete adjunction between the atomic Boolean algebras and the cat…
▽ More
We exhibit an adjunction between a category of abstract algebras of partial functions and a category of set quotients. The algebras are those atomic algebras representable as a collection of partial functions closed under relative complement and domain restriction; the morphisms are the complete homomorphisms. This generalises the discrete adjunction between the atomic Boolean algebras and the category of sets. We define the compatible completion of a representable algebra, and show that the monad induced by our adjunction yields the compatible completion of any atomic representable algebra. As a corollary, the adjunction restricts to a duality on the compatibly complete atomic representable algebras, generalising the discrete duality between complete atomic Boolean algebras and sets. We then extend these adjunction, duality, and completion results to representable algebras equipped with arbitrary additional completely additive and compatibility preserving operators.
△ Less
Submitted 4 May, 2022; v1 submitted 30 November, 2020;
originally announced December 2020.
-
Difference-restriction algebras of partial functions: axiomatisations and representations
Authors:
Célia Borlido,
Brett McLean
Abstract:
We investigate the representation and complete representation classes for algebras of partial functions with the signature of relative complement and domain restriction. We provide and prove the correctness of a finite equational axiomatisation for the class of algebras representable by partial functions. As a corollary, the same equations axiomatise the algebras representable as injective partial…
▽ More
We investigate the representation and complete representation classes for algebras of partial functions with the signature of relative complement and domain restriction. We provide and prove the correctness of a finite equational axiomatisation for the class of algebras representable by partial functions. As a corollary, the same equations axiomatise the algebras representable as injective partial functions. For complete representations, we show that a representation is meet complete if and only if it is join complete. Then we show that the class of completely representable algebras is precisely the class of atomic and representable algebras. As a corollary, the same properties axiomatise the class of algebras completely representable by injective partial functions. The universal-existential-universal axiomatisation this yields for these complete representation classes is the simplest possible, in the sense that no existential-universal-existential axiomatisation exists.
△ Less
Submitted 4 May, 2022; v1 submitted 30 November, 2020;
originally announced November 2020.
-
A categorical duality for algebras of partial functions
Authors:
Brett McLean
Abstract:
We prove a categorical duality between a class of abstract algebras of partial functions and a class of (small) topological categories. The algebras are the isomorphs of collections of partial functions closed under the operations of composition, antidomain, range, and preferential union (or 'override'). The topological categories are those whose space of objects is a Stone space, source map is a…
▽ More
We prove a categorical duality between a class of abstract algebras of partial functions and a class of (small) topological categories. The algebras are the isomorphs of collections of partial functions closed under the operations of composition, antidomain, range, and preferential union (or 'override'). The topological categories are those whose space of objects is a Stone space, source map is a local homeomorphism, target map is open, and all of whose arrows are epimorphisms.
△ Less
Submitted 3 February, 2021; v1 submitted 16 September, 2020;
originally announced September 2020.
-
Free Kleene algebras with domain
Authors:
Brett McLean
Abstract:
First we identify the free algebras of the class of algebras of binary relations equipped with the composition and domain operations. Elements of the free algebras are pointed labelled finite rooted trees. Then we extend to the analogous case when the signature includes all the Kleene algebra with domain operations; that is, we add union and reflexive transitive closure to the signature. In this s…
▽ More
First we identify the free algebras of the class of algebras of binary relations equipped with the composition and domain operations. Elements of the free algebras are pointed labelled finite rooted trees. Then we extend to the analogous case when the signature includes all the Kleene algebra with domain operations; that is, we add union and reflexive transitive closure to the signature. In this second case, elements of the free algebras are 'regular' sets of the trees of the first case. As a corollary, the axioms of domain semirings provide a finite quasiequational axiomatisation of the equational theory of algebras of binary relations for the intermediate signature of composition, union, and domain. Next we note that our regular sets of trees are not closed under complement, but prove that they are closed under intersection. Finally, we prove that under relational semantics the equational validities of Kleene algebras with domain form a decidable set.
△ Less
Submitted 28 September, 2020; v1 submitted 24 July, 2019;
originally announced July 2019.
-
The temporal logic of two-dimensional Minkowski spacetime with slower-than-light accessibility is decidable
Authors:
Robin Hirsch,
Brett McLean
Abstract:
We work primarily with the Kripke frame consisting of two-dimensional Minkowski spacetime with the irreflexive accessibility relation 'can reach with a slower-than-light signal'. We show that in the basic temporal language, the set of validities over this frame is decidable. We then refine this to PSPACE-complete. In both cases the same result for the corresponding reflexive frame follows immediat…
▽ More
We work primarily with the Kripke frame consisting of two-dimensional Minkowski spacetime with the irreflexive accessibility relation 'can reach with a slower-than-light signal'. We show that in the basic temporal language, the set of validities over this frame is decidable. We then refine this to PSPACE-complete. In both cases the same result for the corresponding reflexive frame follows immediately. With a little more work we obtain PSPACE-completeness for the validities of the Halpern-Shoham logic of intervals on the real line with two different combinations of modalities.
△ Less
Submitted 25 June, 2018;
originally announced June 2018.
-
Disjoint-union partial algebras
Authors:
Robin Hirsch,
Brett McLean
Abstract:
Disjoint union is a partial binary operation returning the union of two sets if they are disjoint and undefined otherwise. A disjoint-union partial algebra of sets is a collection of sets closed under disjoint unions, whenever they are defined. We provide a recursive first-order axiomatisation of the class of partial algebras isomorphic to a disjoint-union partial algebra of sets but prove that no…
▽ More
Disjoint union is a partial binary operation returning the union of two sets if they are disjoint and undefined otherwise. A disjoint-union partial algebra of sets is a collection of sets closed under disjoint unions, whenever they are defined. We provide a recursive first-order axiomatisation of the class of partial algebras isomorphic to a disjoint-union partial algebra of sets but prove that no finite axiomatisation exists. We do the same for other signatures including one or both of disjoint union and subset complement, another partial binary operation we define.
Domain-disjoint union is a partial binary operation on partial functions, returning the union if the arguments have disjoint domains and undefined otherwise. For each signature including one or both of domain-disjoint union and subset complement and optionally including composition, we consider the class of partial algebras isomorphic to a collection of partial functions closed under the operations. Again the classes prove to be axiomatisable, but not finitely axiomatisable, in first-order logic.
We define the notion of pairwise combinability. For each of the previously considered signatures, we examine the class isomorphic to a partial algebra of sets/partial functions under an isomorphism map** arbitrary suprema of pairwise combinable sets to the corresponding disjoint unions. We prove that for each case the class is not closed under elementary equivalence.
However, when intersection is added to any of the signatures considered, the isomorphism class of the partial algebras of sets is finitely axiomatisable and in each case we give such an axiomatisation.
△ Less
Submitted 21 June, 2017; v1 submitted 1 December, 2016;
originally announced December 2016.
-
The finite representation property for composition, intersection, domain and range
Authors:
Brett McLean,
Szabolcs Mikulás
Abstract:
We prove that the finite representation property holds for representation by partial functions for the signature consisting of composition, intersection, domain and range and for any expansion of this signature by the antidomain, fixset, preferential union, maximum iterate and opposite operations. The proof shows that, for all these signatures, the size of base required is bounded by a double-expo…
▽ More
We prove that the finite representation property holds for representation by partial functions for the signature consisting of composition, intersection, domain and range and for any expansion of this signature by the antidomain, fixset, preferential union, maximum iterate and opposite operations. The proof shows that, for all these signatures, the size of base required is bounded by a double-exponential function of the size of the algebra. This establishes that representability of finite algebras is decidable for all these signatures. We also give an example of a signature for which the finite representation property fails to hold for representation by partial functions.
△ Less
Submitted 4 March, 2016; v1 submitted 9 March, 2015;
originally announced March 2015.
-
Moon Search Algorithms for NASA's Dawn Mission to Asteroid Vesta
Authors:
Nargess Memarsadeghi,
Lucy A. McFadden,
David Skillman,
Brian McLean,
Max Mutchler,
Uri Carsenty,
Eric E. Palmer,
the Dawn Mission's Satellite Working Group
Abstract:
A moon or natural satellite is a celestial body that orbits a planetary body such as a planet, dwarf planet, or an asteroid. Scientists seek understanding the origin and evolution of our solar system by studying moons of these bodies. Additionally, searches for satellites of planetary bodies can be important to protect the safety of a spacecraft as it approaches or orbits a planetary body. If a sa…
▽ More
A moon or natural satellite is a celestial body that orbits a planetary body such as a planet, dwarf planet, or an asteroid. Scientists seek understanding the origin and evolution of our solar system by studying moons of these bodies. Additionally, searches for satellites of planetary bodies can be important to protect the safety of a spacecraft as it approaches or orbits a planetary body. If a satellite of a celestial body is found, the mass of that body can also be calculated once its orbit is determined. Ensuring the Dawn spacecraft's safety on its mission to the asteroid (4) Vesta primarily motivated the work of Dawn's Satellite Working Group (SWG) in summer of 2011. Dawn mission scientists and engineers utilized various computational tools and techniques for Vesta's satellite search. The objectives of this paper are to 1) introduce the natural satellite search problem, 2) present the computational challenges, approaches, and tools used when addressing this problem, and 3) describe applications of various image processing and computational algorithms for performing satellite searches to the electronic imaging and computer science community. Furthermore, we hope that this communication would enable Dawn mission scientists to improve their satellite search algorithms and tools and be better prepared for performing the same investigation in 2015, when the spacecraft is scheduled to approach and orbit the dwarf planet (1) Ceres.
△ Less
Submitted 9 January, 2013;
originally announced January 2013.