Create accountLogin

Recent searches

No recent searches

Search options

Only available when logged in.
mathstodon.xyz is one of the many independent Mastodon servers you can use to participate in the fediverse.
A Mastodon instance for maths people. We have LaTeX rendering in the web interface!

Administered by:

Server stats:

2.8K
active users

mathstodon.xyz: AboutStatusProfiles directoryPrivacy policy

Mastodon: AboutGet the appKeyboard shortcutsView source codev4.3.7

#settheory

0 posts0 participants0 posts today
Public
2something

The set of all sets that are not big enough to trigger Russell's Paradox.


Okay that sounds like a joke, but I have a clear memory of my algebra professor in undergrad saying "If you have a large category, you can always shrink it to a small category that includes all the objects you care about."

Unless you're a foundations creature, in which case the objects you care about might include sets or categories which are big enough to cause trouble.

#SetTheory #CategoryTheory #Math

Public
José A. Alonso

Formalization of the filter extension principle (FEP) in Coq. ~ Guowei Dou, Wensheng Yu (2024). arxiv.org/abs/2407.06222

arXiv logo
arXiv.orgFormalization of the Filter Extension Principle (FEP) in CoqThe Filter Extension Principle (FEP) asserts that every filter can be extended to an ultrafilter, which plays a crucial role in the quest for non-principal ultrafilters. Non-principal ultrafilters find widespread applications in logic, set theory, topology, model theory, and especially non-standard extensions of algebraic structures. Since non-principal ultrafilters are challenging to construct directly, the Filter Extension Principle, stemming from the Axiom of Choice, holds significant value in obtaining them. This paper presents the formal verification of the Filter Extension Principle, implemented using the Coq proof assistant and grounded in axiomatic set theory. It offers formal descriptions for the concepts related to filter base, filter, ultrafilter and more. All relevant theorems, propositions, and the Filter Extension Principle itself are rigorously and formally verified. This work sets the stage for the formalization of non-standard analysis and a specific real number theory.
Public
José A. Alonso

Formalization of the axiom of choice and its equivalent theorems. ~ Tianyu Sun, Wensheng Yu (2019). arxiv.org/abs/1906.03930v1

arXiv logo
arXiv.orgFormalization of the Axiom of Choice and its Equivalent TheoremsIn this paper, we describe the formalization of the axiom of choice and several of its famous equivalent theorems in Morse-Kelley set theory. These theorems include Tukey's lemma, the Hausdorff maximal principle, the maximal principle, Zermelo's postulate, Zorn's lemma and the well-ordering theorem. We prove the above theorems by the axiom of choice in turn, and finally prove the axiom of choice by Zermelo's postulate and the well-ordering theorem, thus completing the cyclic proof of equivalence between them. The proofs are checked formally using the Coq proof assistant in which Morse-Kelley set theory is formalized. The whole process of formal proof demonstrates that the Coq-based machine proving of mathematics theorem is highly reliable and rigorous. The formal work of this paper is enough for most applications, especially in set theory, topology and algebra.
Public
Ur Ya'ar

TIL: "The use of the symbol ∈ (a stylized form of the Greek epsilon) to denote membership was initiated by the Italian mathematician Giuseppe Peano in 1889. It abbreviates the Greek word ἐστί, which means "is". The underlying rationale is illustrated by the fact that if 𝐵 is the set of all blue objects, then we write "𝑥∈𝐵" in order to assert that 𝑥 is blue."
- Enderton, Elements of set theory

#TIL#SetTheory#notation
Public
Rowan Brad Quni

The sets of all math (M), communication (C), and physical matter (P) are subsets of information (I):

M ⊆ I (M is a subset of I)
C ⊆ I (C is a subset of I)
P ⊆ I (P is a subset of I)

Alternatively, we can express this as the union of the sets:
(M ∪ C ∪ P) ⊆ I (The union of M, C, and P is a subset of I)

#InformationalUniverse #IUH #InformationTheory #Epistemology #DataScience
#Mathematics #Proof #Physics #SetTheory #Ontology #Reality #DigitalAge #AI #QuantumInformation #QNFO #StickyNote

Public *
Ur Ya'ar

"We have been studying mice in the abstract, but we have yet to produce any! In this section we shall describe a certain family of mouse constructions which we call, for obscure reasons, 𝐾ᶜ-constructions."

− Steel, An outline of inner model theory

#MathQuote#SetTheory#mice
SearchLive feeds
About