Login

Recent searches

No recent searches

Search options

Not available on mastodon.xyz.
mastodon.xyz is one of the many independent Mastodon servers you can use to participate in the fediverse.
A Mastodon instance, open to everyone, but mainly English and French speaking.

Administered by:

Server stats:

814
active users

mastodon.xyz: AboutProfiles directoryPrivacy policy

Mastodon: AboutGet the appKeyboard shortcutsView source codev4.3.4

#coq

3 posts3 participants1 post today
Public
Lénon
À Champagnac la rivière, comme dans beaucoup de villages, il y a des coqs et des poules. Ceux là ont l'air pas mal logés.
Comme par hasard le symbole de la résidence Super Rural qui nous amène là est un coq...

Bref je dessine des volailles pour ce projet depuis des mois et des fois c'est sur le motif.
En + on a appris que cette parcelle était une ancienne chenevière (parcelle de culture du chanvre).

#superrural
#poules
#coq
#habitabilite
Superrural.fr
Public
José A. Alonso

Bi-intuitionistic logics through the abstract algebraic logic lens. ~ Jonte Deakin, Ian Shillito. arxiv.org/abs/2503.17159 #ITP #Coq #Rocq #Logic

arXiv logo
arXiv.orgBi-intuitionistic logics through the abstract algebraic logic lensSince the discovery of critical mistakes in Rauszer's work on bi-intuitionistic logics, solid foundations for these have progressively been rebuilt. However, the algebraic treatment of these logics has not yet been tended to. We fill this gap by algebraically analysing the bi-intuitionistic logics wBIL and sBIL. Given that these logics are only distinguished as consequence relations, and not as sets of theorems (hence the conflation in Rauszer's work), the algebraic tools we use are tailored to the treatment of such relations. We mainly inspect these logics through the lens of abstract algebraic logic, but we also provide an alternative algebraic analysis of wBIL and sBIL as logic preserving degrees of truth and truth, respectively. Our results pertaining to wBIL and sBIL are formalised in the interactive theorem prover Rocq.
Public
José A. Alonso

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

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 #ITP #Coq #SetTheory

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.
ExploreLive feeds
About