| 1. |
- Aczel, Peter, et al.
(författare)
-
On the T1 axiom and other separation properties in constructive point-free and point-set topology
- 2010
-
Ingår i: Annals of Pure and Applied Logic. - : Elsevier BV. - 0168-0072 .- 1873-2461. ; 161:4, s. 560-569
-
Tidskriftsartikel (refereegranskat)abstract
- In this note a T1 formal space (T1 set-generated locale) is a formal space whose points are closed as subspaces. Any regular formal space is T1. We introduce the more general notion of a T1∗ formal space, and prove that the class of points of a weakly set-presentable T1∗ formal space is a set in the constructive set theory CZF. The same also holds in constructive type theory. We then formulate separation properties Ti∗ for constructive topological spaces (ct-spaces), strengthening separation properties discussed elsewhere. Finally we relate the Ti∗ properties for ct-spaces with corresponding properties of formal spaces.
|
|
| 2. |
- Ahlman, Ove, 1988-
(författare)
-
Simple structures axiomatized by almost sure theories
- 2016
-
Ingår i: Annals of Pure and Applied Logic. - : Elsevier BV. - 0168-0072 .- 1873-2461. ; 167:5, s. 435-456
-
Tidskriftsartikel (refereegranskat)abstract
- In this article we give a classification of the binary, simple, ω-categorical structures with SU-rank 1 and trivial algebraic closure. This is done both by showing that they satisfy certain extension properties, but also by noting that they may be approximated by the almost sure theory of some sets of finite structures equipped with a probability measure. This study give results about general almost sure theories, but also considers certain attributes which, if they are almost surely true, generate almost sure theories with very specific properties such as ω-stability or strong minimality.
|
|
| 3. |
- Berger, Josef, et al.
(författare)
-
A predicative completion of a uniform space
- 2012
-
Ingår i: Annals of Pure and Applied Logic. - : Elsevier BV. - 0168-0072 .- 1873-2461. ; 163:8, s. 975-980
-
Tidskriftsartikel (refereegranskat)abstract
- We give a predicative construction of a completion of a uniform space in the constructive Zermelo-Fraenkel set theory.
|
|
| 4. |
- Djordjevic, Marko
(författare)
-
The finite submodel property and ω-categorical expansions of pregeometries
- 2006
-
Ingår i: Annals of Pure and Applied Logic. - : Elsevier BV. - 0168-0072 .- 1873-2461. ; 139:1-3, s. 201-229
-
Tidskriftsartikel (refereegranskat)abstract
- We prove, by a probabilistic argument, that a class of ω-categorical structures, on which algebraic closure defines a pregeometry, has the finite submodel property. This class includes any expansion of a pure set or of a vector space, projective space or affine space over a finite field such that the new relations are sufficiently independent of each other and over the original structure. In particular, the random graph belongs to this class, since it is a sufficiently independent expansion of an infinite set, with no structure. The class also contains structures for which the pregeometry given by algebraic closure is non-trivial.
|
|
| 5. |
- Enqvist, Sebastian, et al.
(författare)
-
Completeness for mu-calculi : A coalgebraic approach
- 2019
-
Ingår i: Annals of Pure and Applied Logic. - : Elsevier BV. - 0168-0072 .- 1873-2461. ; 170:5, s. 578-641
-
Tidskriftsartikel (refereegranskat)abstract
- We set up a generic framework for proving completeness results for variants of the modal mu-calculus, using tools from coalgebraic modal logic. We illustrate the method by proving two new completeness results: for the graded mu-calculus (which is equivalent to monadic second-order logic on the class of unranked tree models), and for the monotone modal mu-calculus. Besides these main applications, our result covers the Kozen-Walukiewicz completeness theorem for the standard modal mu-calculus, as well as the linear-time mu-calculus and modal fixpoint logics on ranked trees. Completeness of the linear time mu-calculus is known, but the proof we obtain here is different and places the result under a common roof with Walukiewicz' result. Our approach combines insights from the theory of automata operating on potentially infinite objects, with methods from the categorical framework of coalgebra as a general theory of state-based evolving systems. At the interface of these theories lies the notion of a coalgebraic modal one-step language. One of our main contributions here is the introduction of the novel concept of a disjunctive basis for a modal one-step language. Generalizing earlier work, our main general result states that in case a coalgebraic modal logic admits such a disjunctive basis, then soundness and completeness at the one-step level transfer to the level of the full coalgebraic modal mu-calculus.
|
|
| 6. |
- Garner, Richard
(författare)
-
On the strength of dependent products in the type theory of Martin-Lof
- 2009
-
Ingår i: Annals of Pure and Applied Logic. - : Elsevier BV. - 0168-0072 .- 1873-2461. ; 160:1, s. 1-12
-
Tidskriftsartikel (refereegranskat)abstract
- One may formulate the dependent product types of Martin-Lof type theory either in terms of abstraction and application operators like those for the lambda-calculus; or in terms of introduction and elimination rules like those for the other constructors of type theory. It is known that the latter rules are at least as strong as the former: we show that they are in fact strictly stronger. We also show, in the presence of the identity types, that the elimination rule for dependent products - which is a "higher-order" inference rule ill the sense of Schroeder-Heister - can be reformulated in a first-order manner. Finally, we consider the principle of function extensionality in type theory, which asserts that two elements of a dependent product type which are pointwise propositionally equal, are themselves propositionally equal. We demonstrate that the usual formulation of this principle fails to verify a number of very natural propositional equalities; and suggest all alternative formulation which rectifies this deficiency. (C) 2009 Elsevier B.V. All rights reserved.
|
|
| 7. |
- Koponen, Vera
(författare)
-
Asymptotic probabilities of extension properties and random l-colourable structures
- 2012
-
Ingår i: Annals of Pure and Applied Logic. - : Elsevier. - 0168-0072 .- 1873-2461. ; 163:4, s. 391-438
-
Tidskriftsartikel (refereegranskat)abstract
- We consider a set of finite structures such that all members of have the same universe, the cardinality of which approaches ∞ as n→∞. Each structure in may have a nontrivial underlying pregeometry and on each we consider a probability measure, either the uniform measure, or what we call the dimension conditional measure. The main questions are: What conditions imply that for every extension axiom φ, compatible with the defining properties of , the probability that φ is true in a member of approaches 1 as n→∞? And what conditions imply that this is not the case, possibly in the strong sense that the mentioned probability approaches 0 for some φ? If each is the set of structures with universe {1,…,n}, in a fixed relational language, in which certain “forbidden” structures cannot be weakly embedded and has the disjoint amalgamation property, then there is a condition (concerning the set of forbidden structures) which, if we consider the uniform measure, gives a dichotomy; i.e., the condition holds if and only if the answer to the first question is ‘yes’. In general, we do not obtain a dichotomy, but we do obtain a condition guaranteeing that the answer is ‘yes’ for the first question, as well as condition guaranteeing that the answer is ‘no’; and we give examples showing that in the gap between these conditions the answer may be either ‘yes’ or ‘no’. This analysis is made for both the uniform measure and for the dimension conditional measure. The later measure has a closer relation to random generation of structures and is more “generous” with respect to satisfiability of extension axioms. Random l-coloured structures fall naturally into the framework discussed so far, but random l-colourable structures need further considerations. It is not the case that every extension axiom compatible with the class of l-colourable structures almost surely holds in an l-colourable structure. But a more restricted set of extension axioms turns out to hold almost surely, which allows us to prove a zero–one law for random l-colourable structures, using a probability measure which is derived from the dimension conditional measure, and, after further combinatorial considerations, also for the uniform probability measure.
|
|
| 8. |
- Koponen, Vera, 1968-
(författare)
-
Binary simple homogeneous structures
- 2018
-
Ingår i: Annals of Pure and Applied Logic. - : Elsevier BV. - 0168-0072 .- 1873-2461. ; 169:12, s. 1335-1368
-
Tidskriftsartikel (refereegranskat)abstract
- We describe all binary simple homogeneous structures M in terms of ∅-definable equivalence relations on M, which “coordinatize” M and control dividing, and extension properties that respect these equivalence relations.
|
|
| 9. |
- Koponen, Vera, 1968-
(författare)
-
Independence and the finite submodel property
- 2009
-
Ingår i: Annals of Pure and Applied Logic. - : Elsevier. - 0168-0072 .- 1873-2461. ; 158:1-2, s. 58-79
-
Tidskriftsartikel (refereegranskat)abstract
- We study a class c of aleph(0)-categorical simple structures such that every M in c has uncomplicated forking behavior and such that definable relations in M which do not cause forking are independent in a sense that is made precise; we call structures in c independent. The SU-rank of such M may be n for any natural number n > 0. The most well-known unstable member of c is the random graph, which has SU-rank one. The main result is that for every strongly independent structure M in e, if a sentence phi is true in M then phi is true in a finite substructure of M. The same conclusion holds for every structure in c with SU-rank one: so in this case the word 'strongly' can be removed. A probability theoretic argument is involved and it requires sufficient independence between relations which do not cause forking. A stable structure M belongs to c if and only if it is aleph(0)-categorical, aleph(0)-stable and every definable strictly minimal Subset of M-eq is indiscernible.
|
|
| 10. |
- Koponen, Vera, 1968-
(författare)
-
Supersimple omega-categorical theories and pregeometries
- 2019
-
Ingår i: Annals of Pure and Applied Logic. - : Elsevier. - 0168-0072 .- 1873-2461. ; 170:12
-
Tidskriftsartikel (refereegranskat)abstract
- We prove that if T is an omega-categorical supersimple theory with nontrivial dependence (given by forking), then there is a nontrivial regular 1-type over a finite set of reals which is realized by real elements; hence forking induces a nontrivial pregeometry on the solution set of this type and the pregeometry is definable (using only finitely many parameters). The assumption about omega-categoricity is necessary. This result is used to prove the following: If V is a finite relational vocabulary with maximal arity 3 and T is a supersimple V-theory with elimination of quantifiers, then T has trivial dependence and finite SU-rank. This immediately gives the following strengthening of [18, Theorem 4.1]: if M is a ternary simple homogeneous structure with only finitely many constraints, then Th(M) has trivial dependence and finite SU-rank. (C) 2019 Published by Elsevier B.V.
|
|
