Create accountLogin

Recent searches

No recent searches

Search options

Only available when logged in.
mastodon.world is one of the many independent Mastodon servers you can use to participate in the fediverse.
Generic Mastodon server for anyone to use.

Administered by:

Server stats:

10K
active users

mastodon.world: AboutStatusProfiles directoryPrivacy policy

Mastodon: AboutGet the appKeyboard shortcutsView source codev4.3.7

#modeltheory

0 posts0 participants0 posts today
Public
Alex Nelson

What 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

thmprover.wordpress.com/2024/1

Ariadne's Thread · What is a “structure” in Mizar?We saw how Mizar formalizes, e.g., Groups using structures. We also saw that Mizar’s set theoretic foundations includes an axiom asserting all objects are sets. So is a Group a set, or not? A…
Public *
Artem Chernikov

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"
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.

Abstract of the preprint on arXiv linked in the post.
#Mathematics#ModelTheory#TopologicalDynamics
Public
Greg Restall

After 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.

consequently.org/presentation/

consequently.orgExploring Three-Valued Models for Identity — consequently.org
#logic#ModelTheory#ProofTheory
Public *
Jon Awbrey

Survey of Animated Logical Graphs
• inquiryintoinquiry.com/2023/03

This is a Survey of blog and wiki posts on Logical Graphs, encompassing several families of graph-theoretic structures originally developed by Charles S. Peirce as graphical formal languages or visual styles of syntax amenable to interpretation for logical applications.

#Peirce #Logic #LogicalGraphs #EntitativeGraphs #ExistentialGraphs
#Boole #BooleanAlgebra #BooleanFunctions #ModelTheory #ProofTheory
#SpencerBrown #LawsOfForm #PropositionalCalculus #LogicAsSemiotics

Inquiry Into InquirySurvey of Animated Logical Graphs • 5By Jon Awbrey
Continued thread
Public *
Jon Awbrey

#LogicalGraphs • 16
• oeis.org/w/index.php?title=Log

#Duality • Logical and Topological

Turning to the #InitialEquation or #LogicalAxiom whose text expression is \(``\texttt{(}~\texttt{)(}~\texttt{)}=\texttt{(}~\texttt{)}",\) Figure 8 shows the planar maps and their corresponding #DualGraphs superimposed.

Figure 8
• oeis.org/w/images/0/09/Logical

#Logic #Peirce #SpencerBrown #LawsOfForm
#PropositionalCalculus #BooleanFunctions
#GraphTheory #ModelTheory #ProofTheory

Figure 8 is a composite picture for the Formal Equation in Figure 1. It illustrates the mapping of alpha graphs to dual graphs by overlaying the alpha graphs in Figure 1 with their corresponding dual graphs. We may think of the picture as composed of two layers. Layer 1 shows the alpha graphs for the First Initial Equation, previously shown in Figure 1 and again in Figure 7. Proceeding from left to right in Layer 1, there is a form on the left hand side, an equal sign, and a form on the right hand side. The form on the left consists of two circles drawn next to each other a space apart. The form on the right consists of a single circle. Layer 2 shows the dual graphs corresponding to the alpha graphs in Layer 1. Proceeding from left to right in Layer 2, there is a form on the left hand side, an equal sign, and a form on the right hand side. The form on the left is a graph-theoretic rooted tree, in this case consisting of two edges sharing a common root. The root is placed outside and below the two circles. The first edge extends to the interior of the circle on the left, where it meets its terminal node. The second edge extends to the interior of the circle on the right, where it meets its terminal node. The form on the right consists of a single rooted edge, or a rooted path of length one. It extends from its root outside the single circle to its terminal node inside the circle.
Continued thread
Public *
Jon Awbrey

#LogicalGraphs • 14
• oeis.org/w/index.php?title=Log

#Duality • Logical and Topological

The procedure just described is called “traversing” the tree and the string read off is called the “#TraversalString” of the tree. The reverse operation of going from the string to the tree is called “parsing” the string and the tree constructed is called the “#ParseGraph” of the string.

#Logic #Peirce #SpencerBrown #LawsOfForm
#PropositionalCalculus #BooleanFunctions
#GraphTheory #ModelTheory #ProofTheory

oeis.orgLogical Graphs - OeisWiki
Continued thread
Public
Jon Awbrey

#LogicalGraphs • 12
• oeis.org/w/index.php?title=Log

#Duality • Logical and Topological

Once we make the connection between one of #Peirce's #AlphaGraphs and its character string expression it's not too big a leap to see how the character string codes up the structure of the topological #DualGraph in the space of #RootedTrees.

#Logic #Peirce #SpencerBrown #LawsOfForm
#PropositionalCalculus #BooleanFunctions
#GraphTheory #ModelTheory #ProofTheory

oeis.orgLogical Graphs - OeisWiki
Continued thread
Public *
Jon Awbrey

#LogicalGraphs • 5
• oeis.org/w/index.php?title=Log

#AbstractPointOfView —

We may note in passing historical details like the fact Charles Sanders #Peirce used a #StreamerCross symbol where George #SpencerBrown used a #CarpentersSquare marker but the themes of primary interest at the abstract level of form are indifferent to variations of that order.

#Logic #PropositionalCalculus #BooleanFunctions
#Form #Idea #Isomorphism #MathematicalPerspective
#LawsOfForm #GraphTheory #ModelTheory #ProofTheory

oeis.orgLogical Graphs - OeisWiki
Continued thread
Public *
Jon Awbrey

#LogicalGraphs • 3
• oeis.org/w/index.php?title=Log

We begin on a low but expansive plateau of #FormalSystems #Peirce mapped out in his system of #AlphaGraphs \((\alpha),\) a platform so abstract in its mathematical forms as to support at least two interpretations for use in the conduct of logical reasoning. Along the way, we incorporate the later contributions of George #SpencerBrown, who revived and augmented Peirce's system in his book #LawsOfForm.

oeis.orgLogical Graphs - OeisWiki
#Logic#GraphTheory#ModelTheory
ExploreLive feeds
About