All Questions
1,459 questions with no upvoted or accepted answers
3
votes
0
answers
137
views
A question regarding forcing in $NGBC^{-f}$+$BAFA$
Suppose one has a model $M$$\vDash$$NGBC^{-f}$+BAFA. Does there exist a (class) forcing extension $M[G]$$\vDash$$NGBC^{-f}$+$BAFA$ that has a submodel $N$$\vDash$$NGB^{-f}$+$BAFA$+$\lnot$$AC$? Can ...
3
votes
0
answers
115
views
Cardinality based results in Topological Vector Spaces?
Given a topological vector space $V$, let its density be the smallest cardinal $A$ such that a set of cardinality $A$ is dense in $V$. Naively, it seems one of two things happen:
TVS's $V$ of larger ...
3
votes
0
answers
238
views
Is there a $\Sigma^0_3$-complete ideal on $\omega$?
In Kechris's book "Classical Descriputive set theory" Chapter 23 (Exercise 23.4), it claim that there is a $\Sigma^0_\xi$-complete ideal on $\omega$ for each $\xi\geq 3$.
There is a candidate ...
3
votes
0
answers
172
views
Logical framework for type theories like ML and CIC
I'm looking for a logical framework in which it is possible to easily present both intensional and extensional theories of dependent types with a partially ordered set of universes à la Russell ...
3
votes
0
answers
314
views
Certain conditions on cancellative semigroups
This is extracted from this question following Benjamin Steinberg's suggestion.
For a semigroup $S,$ let $P(S)$ denote the power semigroup of $S,$ which is made up of all non-empty subsets of $S$ ...
3
votes
0
answers
126
views
dual composition of binary relations
I'm not sure if this is of any interest at all, but I spent some time looking at it a couple of years ago so I'd like to ask for input on this.
Given two binary relations $\rho,\,\sigma$ on a set $X,$...
3
votes
0
answers
141
views
Non-finitely based varieties and pseudovarieties
The variety of semigroups defined by $B=\Big\{(x^py^p)^2=(y^px^p)^2:p \text{ is prime}\Big\}$ is non-finitely based (Isbell, 1970). Is the pseudovariety defined by $B$ also non-finitely based?
More ...
3
votes
0
answers
303
views
Pseudomodules, "general coherence theorem"
A pseudomonoid is defined within a monoidal bicategory. It is like a monoid in a monoidal category except that the usual axioms hold up to coherent invertible 2-cells. Pseudomonoid is like a monoidal ...
3
votes
0
answers
174
views
Number of k-generated semigroups
Given some $k>1$, I am interested in the number of $k$-generated semigroups of order $n$ (either up to isomorphism or all associative binary operations on an n-element set). At first I thought $3$-...
3
votes
0
answers
138
views
Is every union-closed family of set the set of solutions of some co-HORNSAT formula?
Related to the Union-closed sets conjecture.
Let $\phi$ be a co-HORNSAT
on variables $x_1 \ldots x_n$ in CNF format.
This means in every close at most one literal is negative.
The solutions of $\phi$...
3
votes
0
answers
125
views
Algorithmic quantifier elimination over p-adic fields
It is known that the first-order theory of p-adic fields is decidable, and that the p-adics admit elimination of quantifiers. What is the state of the art in algorithmic aspects of quantifier ...
3
votes
0
answers
190
views
Preimages of accessible full subcategories
My question is ultimately about the model theory of $L_{\infty, \omega}$, but it is more convenient to phrase it in terms of category theory. Suppose I have finitely accessible categories $\mathcal{C},...
3
votes
0
answers
87
views
A question on the incompleteness of quantified K.2 and S4.2 with the Barcan formula
I have been attempting to come to grips with Max Cresswell's account of this in Journal of Philosophical Logic 24 (4):379 - 403 (1995) where he presents proofs of the incompleteness of QK.2BF as well ...
3
votes
0
answers
343
views
Peano (Dedekind) categoricity
What is the smallest fragment of second order logic such that $Th(\mathbb{N})$ in that logic is categorical (only one model, namely natural numbers, up to isomorphism). For example, can we do this in ...
3
votes
0
answers
853
views
What is the role of the (formalized) omega rule in Ramified Analysis?
In the 1960's, Feferman and Schutte did groundbreaking proof-theoretic work to find out the strength of predicative systems of second-order arithmetic. They used the ramified theory of types, a ...
3
votes
0
answers
360
views
Binary search with maximum consecutive lies about "is X in subset S?"
Here's the original problem:
Alice tells Bob "I have thought of an integer between 1 and 2000. Tell
me 1000 numbers. If your set contains my number, I'll give you this
prize." Bob really wants ...
3
votes
0
answers
474
views
Deducing Skolem's nonstandard integers from downward Lowenheim-Skolem?
If one has a nonstandard model $\mathcal{N}$ of PA and adjoins to the first-order theory the countable list of axioms $1<H,\, 2<H,\, 3<H, \ldots$ (satisfied in $\mathcal{N}$) for all the "...
3
votes
0
answers
743
views
The substitution theorem in first order logic (finitely many variables)
We consider the language ${\cal L}=\{\in\}$ with an arbitrary set of variables $V$. Specifically we define ${\bf P}(V)$ as the free algebra of type $\{\bot,\to\}\cup\{\forall x:x\in V\}$ (with the ...
3
votes
0
answers
107
views
Hindman's theorem variant for noncommutative semigroups
The well set proof of Hindman's finite sums theorem applied to noncommutative semigroups yields a sequence of elements such that finite products ordered coherently with this sequence are in one set. ...
3
votes
0
answers
160
views
Self-modelling structures
Consider - for the sake of simplicity - only graphs as structures.
For undirected graphs $(V, E\subseteq \binom{V}{2})$ let
$E(v)$ be the set of edges $e\in E$ incident with $v$, i.e. $\lbrace e \ ...
3
votes
0
answers
199
views
Is there a useful Galois connection between Languages and Grammars?
I've just beginning to learn logic and proof theory - and the following rather vague and perhaps ill-formed question occurred to me.
Given an alphabet it's straightforward to construct the Language, ...
3
votes
0
answers
191
views
What are the enforceable models of local artinian rings?
I was reading Hodges' "Model Theory" Chapter 8 a propos existentially closed models of $\forall_2$ theories in a countable first order language $L$. He extends the proof of the omitting type theorem ...
3
votes
0
answers
166
views
A question of terminology - Unitizations of semigroups
There are at least two standard ways of unitizing a (small) semigroup $\mathbb A$:
(i) We add an identity regardless that $\mathbb A$ is already unital.
(ii) We add an identity only if none is ...
3
votes
0
answers
278
views
Can we prove the completeness of FOL based on forcing?
I asked this question at http://math.stackexchange.com but I didn't get any answer there.
In David Marker's Model Theory, there is a exercise said " we can view a countable Henkin construction as a ...
3
votes
0
answers
241
views
is there any connection between the consistent histories interpretation of quantum mechanics and kripke semantics?
Kripke semantics interpret intuitionistic logic by a partially ordered set of worlds/situations. Consistent histories interpretation of QM elaborates the copenhagen interpretation where a consistent ...
3
votes
0
answers
516
views
Groupoid interpretation of type theory
Hello,
I read the paper on groupoid interpretation of type theory by Hofmann and Streicher and I have a question. According to the authors $Tm([[\text{Set}\:[\Gamma]\: ]])$ is the same as $\text{Se}([...
3
votes
0
answers
185
views
Unbounded Class of Orbit Equivalence Relations
In their paper titled "The Classification of Hypersmooth Borel Equivalence Relations" Alexander Kechris and Alain Louveau quote the following (Theorem 5.2 in the article) as "Harrington, unpublished": ...
3
votes
0
answers
241
views
Non-Computational classical subterms
Assume we have a proof term of the form $(a^{A\rightarrow^c B\rightarrow^{nc} C}b^Ac^B)^C$, where $c$ is classical (that is, contains free instances of duplex negatio affirmat). The extracted term ...
3
votes
0
answers
175
views
Intersecting the algebraic closure of independent elements
$G$ is a group with a simple first order theory $T$ as defined by Shelah, hence equiped with a "nice" notion of independence. $G$ also has generic elements. I write $acl^n(A)$ for the set of elements ...
3
votes
0
answers
257
views
Oracle separating FIP for bounded-depth Frege from FIP for Frege (and hardness conditions on DDH)
Is there an oracle such that in the relativized world, bd-Frege (bounded depth Frege propositional proof system) has FIP (feasible interpolation property) but Frege does not have FIP?
Such an oracle ...
3
votes
0
answers
559
views
Unprovability of the Steiner-Lehmus theorem
Conway postulated that the Steiner-Lehmus theorem is unprovable using direct methods of proof. Can this be proven directly, that the Steiner-Lehmus theorem cannot be proven directly over Euclidean ...
3
votes
1
answer
961
views
Extensions of fast-growing hierarchy
In recent weeks, I have been fascinated by the possible extensions of the fast-growing hierarchy. But is there a way to define it for all recursive ordinals? I saw a statement of this sort on ...
2
votes
0
answers
63
views
Consistency of Sigma-V-2 uniformization with AD
Is ZF + AD consistent with: For every real $r$, every true $Σ^V_2(r)$ statement has a $Δ^V_2(r)$ example?
DC is provable in ZF + every true $Σ^V_2$ statement has a $Δ^V_2$ example (i.e. witness). ...
2
votes
0
answers
102
views
Is this theory synonymous with ZF + Global Choice?
$\textbf{Logic:}$ Mono-sorted first order logic with equality.
$\textbf{Extralogical Primitives: } <, \in$
Define: $x > y \iff y < x \\ x \leq y \iff x < y \lor x=y \\ x \not > y \iff \...
2
votes
0
answers
84
views
Is it a property when a cohesive type is a manifold?
Let $X : Type$ in a type theory $T$ interpreting synthetic differential geometry - I don't believe it should matter too much if we have smooth stuff on hand except maybe at the end of this line, but ...
2
votes
0
answers
92
views
Geometric interpretation of flags and the role of the rook monoid and Kazhdan–Lusztig theory in $M_n(\mathbb{C})$
Let $G = GL_n(\mathbb{C})$, $B$ be its Borel subgroup, and $P$ a parabolic subgroup. The space $G/B$ corresponds to complete flags in $ \mathbb{C}^n$, and $G/P$ corresponds to partial flags. The ...
2
votes
0
answers
187
views
Semantic equivalence between mathematical proofs
Sometimes, we recognize two proofs of the same claim to be the "same" proof. In some cases, this sameness is obvious -- for example, the proofs that $\sqrt{2}$ and $\sqrt{3}$ are irrational ...
2
votes
0
answers
117
views
Can we have the set world obeying Quine's New Foundations with its well-founded realm obeying $\sf ZFC$?
Is this theory consistent?
Language: first order language of set theory,
Extra-logical axioms:
1. Extensionality: as in $\sf NF$.
2. Stratified Comprehension: as in $\sf NF$.
Define: a set is said ...
2
votes
0
answers
102
views
Direct construction of an arithmetically high degree below $0^{(\omega)}$
The existence of a high arithmetic degree (meaning the degrees induced by the notion of relative arithmetic definability) below $0^\omega$ can be established by using Harrington/Simpson's ...
2
votes
0
answers
232
views
Is the poset in the following construction stationary $\aleph_{\alpha + 2}$-linked?
Definition: A poset P is $\mathbf{stationary}$ $\kappa^{+}$-$\mathbf{linked}$ if for every sequence of conditions $(p_{\gamma} | \gamma < \kappa^{+})$, there is a regerssive function $f: \kappa^{+} ...
2
votes
0
answers
88
views
Intuitionistic countermodels in which $u \leq v \implies M_u \leq M_v$
In Fitting's Intuitionistic Logic Model Theory and Forcing, the following theorem is proven:
If $X$ is a formula with no universal quantifiers and $\not\vdash_I X$, then there is a countermodel $(\...
2
votes
0
answers
142
views
Can a path in Kleene's $\mathcal{O}$ enumerate all of the computable reals via uniform diagonalization?
It's a well-known fact that there are computable diagonalization functions on Baire space $\mathbb{B} = \mathbb{N}^\mathbb{N}$ (i.e., functions which take a sequence $(r_i)_{i\in \mathbb{N}}$ of ...
2
votes
0
answers
100
views
Realizing arithmetic hierarchy in algebraic number theory
Is it possible to realize arithmetic hierarchy in algebraic number theory?
For example, consider a $\Pi^0_4$ statement of the form $\forall x \exists y \forall z \exists w \phi(x,y,z,w)=0$ where $\phi$...
2
votes
0
answers
132
views
A property of < in Primitive recursive arithmetic
In Primitive recursive arithmetic (PRA), we can introduce $\lt$ by introducing its representing function $K_{\lt}$, where $K_{\lt}(x,y) =sg(x+1-y)$. Here "sg" and "-" are the ...
2
votes
0
answers
196
views
On "necessary connectives" in a structure
Given a clone $\mathcal{C}$ over $\{\top,\perp\}$, let $\mathsf{FOL}^\mathcal{C}$ be the version of first-order logic with connectives from $\mathcal{C}$ in place of the usual Booleans. Given a clone $...
2
votes
0
answers
76
views
Defining fields of characteristic zero in existential second-order logic
Is it possible to define in existential second-order logic (ESO) the class of fields of characteristic zero? An easy compactness argument shows that the class of fields of positive characteristic is ...
2
votes
0
answers
143
views
Constructively, when do functions that agree on $[a, b] \cup [b, c]$ also agree on $[a,c]$?
Let $a, b, c \in \mathbb R$ such that $a \le b \le c$. Let $S$ be some set and $f, g : [a, c] \to S$ be functions. As a follow up to When can a function defined on $[a, b] \cup [b, c]$ be ...
2
votes
0
answers
48
views
Is the class of strongly Kripke complete normal modal logics closed under sums?
Given an arbitrary set of normal modal logics $\mathcal{L}$, one can define their sum $\bigoplus \mathcal{L}$ (or $\bigoplus_{L \in \mathcal{L}} L$ if you prefer) to be the least normal modal logic ...
2
votes
0
answers
235
views
Is there a computable model of HoTT?
Among the various models of homotopy type theory (simplicial sets, cubical sets, etc.), is there a computable one?
Can the negative follow from the Gödel-Rosser incompleteness theorem?
If there is no ...
2
votes
0
answers
434
views
Showing that every satisfiable sentence with at most two variables has a finite model
I have tried to prove, in first order logic, that every satisfiable sentence (without function symbols) with at most two variables has a finite model. My attempts were unsuccessful.
This is an ...