terrorist :: FelineToday I learned
Löwenheim–Skolem theorem
Any 1st order theory with an infinite model has arbitrary large models
https://en.wikipedia.org/wiki/L%C3%B6wenheim%E2%80%93Skolem_theorem
HoldMyTypeThe role of axioms and proofs
"refutation of A in T, is a proof of ¬A. If one exists (T ⊢ ¬A), the statement A is called refutable (in T).
A statement is called decidable (in T) if it is provable or refutable.
A contradiction of a theory T is a proof of 0 in T. If one exists (T ⊢ 0), the theory T is called contradictory or inconsistent ; otherwise it is called consistent.
A refutation of A in T amounts to a contradiction of the theory T∧A obtained by adding A to the axioms of T.
If a statement is both provable and refutable in T then all are, because it means that T is inconsistent, independently of the chosen statement"
Question : can order of evaluation in #haskell relate to #modeltheory
https://settheory.net/foundations/metamathematics#:~:text=refutation%20of%20A,the%20chosen%20statement
The role of axioms and proofs
"refutation of A in T, is a proof of ¬A. If one exists (T ⊢ ¬A), the statement A is called refutable (in T).
A statement is called decidable (in T) if it is provable or refutable.
A contradiction of a theory T is a proof of 0 in T. If one exists (T ⊢ 0), the theory T is called contradictory or inconsistent ; otherwise it is called consistent.
A refutation of A in T amounts to a contradiction of the theory T∧A obtained by adding A to the axioms of T.
If a statement is both provable and refutable in T then all are, because it means that T is inconsistent, independently of the chosen statement"
Question : can order of evaluation in #haskelk relate to #modeltheory
https://settheory.net/foundations/metamathematics#:~:text=refutation%20of%20A,the%20chosen%20statement
Markus Redeker 🐘@LeoTsai14 While they do not actually call it so, set theoreticians do a lot of work in a category in which the objects are the models of set theory and the arrows are the elementary embeddings (https://en.wikipedia.org/wiki/Elementary_equivalence#Elementary_embeddings) between them.
Models of (ZFC-like) set theories have the interesting property that the maps between them are to some amount determined by the mappings between their classes of ordinals: If this map is an isomorphism, the whole map is one (https://en.wikipedia.org/wiki/Critical_point_(set_theory)).
You may also have a look at inner model theory (https://en.wikipedia.org/wiki/Inner_model_theory), I think.
Wilhelm_Grafe[ this is a follow on to my former account [email protected]. and hence repeat here my ... ]
#intro to my way in #philosophy -
I do believe in a relatively slowly [and in a Collingwoodstyle] transforming philosophia perennis.
my papers center around the tradeoff of knowledge and reality, most important in this respect - in my own opinion - is my paper on a formal analogy (in basic #modeltheory) to elements of Spinoza’s #metaphysics in ‘de deo’ [ethics, part I ].
I share my philosophical views broadly construed as a public respondent of the
Philsurvey_2020
[https://philpeople.org/profiles/friedrich-wilhelm-grafe/views],
and I draw and share with discussions (somewhat elaborated chat discussions, as
well as online discussions) at many occasions.
Artem ChernikovA new Ph.D thesis prize is being established in honor of Zoé Chatzidakis, by Fondation Sciences Mathématiques de Paris.
This yearly award for an outstanding thesis in model theory will honor her scientific legacy and her commitment to the younger generation.
https://www.helloasso.com/associations/fondation-sciences-mathematiques-de-paris/formulaires/7
Alex NelsonWhat is a "structure" in Mizar?
This was always one of the most confusing things to me when I first got started with #Mizar since the answer requires a little bit of Model Theory, which isn't adequately taught in the US to "generic Mathematicians".
The answer is surprisingly deep yet simple: it's "just" a finite partial map in the Metatheory. This can be made precise using something like #Isabelle as the Metatheory (as done in the Isabelle/Mizar project).
We can also use a finite set of "attribute"-value pairs, which is called "first-class aggregates" (or "first-class structures") since they're defined like any other notion in Mizar, without special metatheoretic considerations. And they're useful for doing graph theory!
#Mizar #ProofAssistant #ModelTheory #Model_Theory #Logic #Mathematics
https://thmprover.wordpress.com/2024/10/04/what-is-a-structure-in-mizar/
Very excited about this new preprint, with Kyle Gannon and Krzysztof Krupinski!
"Definable convolution and idempotent Keisler measures III. Generic stability, generic transitivity, and revised Newelski's conjecture"
https://arxiv.org/abs/2406.00912
Classical work by Wendel, Rudin, Cohen (before inventing forcing) and others classifies idempotent Borel measures on locally compact abelian groups, showing that they are precisely the Haar measures of compact subgroups.
We are interested in a counterpart of this phenomenon in the definable category. In the same way as e.g. algebraic or Lie groups are important in algebraic or differential geometry, the understanding of groups definable in a given first-order structure (or in certain classes of first-order structures) is important for model theory and its applications. The class of stable groups is at the core of model theory, and the corresponding theory was developed in the 1970s-1980s borrowing many ideas from the study of algebraic groups over algebraically closed fields. More recently, many of the ideas of stable group theory were extended to the class of NIP groups, which contains both stable groups and groups definable in o-minimal structures or over the p-adics. This led to multiple applications, e.g. a resolution of Pillay’s conjecture for compact o-minimal groups, or Hrushovski’s work on approximate subgroups. This brought to light the importance of the study of invariant measures on definable subsets of the group, as well as the methods of topological dynamics. In particular, deep connections with tame dynamical systems as studied by Glasner, Megrelishvili and others have emerged.
Definable convolution and idempotent Keisler measures III. Generic stability, generic transitivity, and revised Newelski's conjecture
We study idempotent measures and the structure of the convolution semigroups of measures over definable groups. We isolate the property of generic transitivity and demonstrate that it is sufficient (and necessary) to develop stable group theory localizing on a generically stable type, including invariant stratified ranks and connected components. We establish generic transitivity of generically stable idempotent types in important new cases, including abelian groups in arbitrary theories and arbitrary groups in rosy theories, and characterize them as generics of connected type-definable subgroups. Using tools from Keisler's randomization theory, we generalize some of these results from types to generically stable Keisler measures, and classify idempotent generically stable measures in abelian groups as (unique) translation-invariant measures on type-definable fsg subgroups. This provides a partial definable counterpart to the classical work of Rudin, Cohen and Pym for locally compact topological groups. Finally, we provide an explicit construction of a minimal left ideal in the convolution semigroup of measures for an arbitrary countable NIP group, from a minimal left ideal in the corresponding semigroup on types and a canonical measure constructed on its ideal subgroup. In order to achieve it, we in particular prove the revised Ellis group conjecture of Newelski for countable NIP groups.
Greg RestallAfter a short summer break exploring Scotland, it’s time to slowly get back into the saddle, giving a few talks, and preparing for the new academic year’s teaching.
First up, a short visit to Bochum for a PhD exam, and an impromptu talk on non-classical models for the identity predicate.
https://consequently.org/presentation/2023/exploring-three-valued-models-for-identity/
Hi! I am a philosopher and logician, and if you would like to understand the kind of work I do, the easiest way to get up to speed is to start with my little slip of a book “Proofs and Models in Philosophical Logic”. https://consequently.org/writing/pmpl-elements/