**18**

votes

**2**answers

996 views

### Is the Invariant Subspace Problem arithmetic?

Invariant Subspace Conjecture: A bounded operator on a separable Hilbert space has a non-trivial closed invariant subspace.
Can this conjecture be reformulated as an arithmetic statement, that is, ...

**1**

vote

**0**answers

76 views

### Interesting fragments of first-order logic induced by sorting?

In first approximation, modal logic (I'm using the term loosely)
can be understood as an interesting fragment of first-order logic
(for simplicity I ignore e.g. how modal logic relates to
...

**5**

votes

**2**answers

151 views

### Models of PRA/EFA with induction on $X$ but not $\omega^X$

As I currently understand it, induction on formulas containing $N+1$ first-order quantifiers is required to prove the well-ordering of the ordinal $(\omega \uparrow\uparrow N) < \epsilon_0$, that ...

**6**

votes

**0**answers

172 views

### Co-Heyting Valued Models of Paraconsistent Set Theory

I've been trying to do some forcing arguments in intuitionistic ZF using Heyting valued models where the Heyting algebra I'm using is actually a bi-Heyting algebra (both a Heyting algebra and a ...

**12**

votes

**2**answers

311 views

### Producing no non-constructible reals

The following is stated without proof in Shelah's book "Cardinal arithmetic" (page 276), and is attributed to Uri Abraham:
Suppose that $L[A], L[B]$ have no non-constructible reals and that ...

**2**

votes

**2**answers

180 views

### What do we call functions that behave like predicate symbols?

Assume a metatheory that supports lambda-abstraction, and an object language that is merely first-order. Now let $\varphi$ denote a formula in the object language with one free variable $x$. Then we ...

**2**

votes

**1**answer

212 views

### Partial interpretation of an iteration

Suppose that $\langle\mathbb{P_\alpha,\dot Q_\beta}\mid \beta<\delta,\alpha\leq\delta\rangle$ is a system of iterated forcing.
Let $\dot a$ be a name in $\mathbb P_\delta$, and let $G_\alpha$ be a ...

**1**

vote

**1**answer

116 views

### Free monoids and full transformation monoids

I asked this question on math stack exchange, but I didn't get any responses. So, now I am motivated to ask it here. Is the class of free monoids first order axiomatizable? And what about the class of ...

**4**

votes

**1**answer

275 views

### Essential incompleteness via diophantine formulas?

Work in the first order language of number theory, consisting of the symbols $\mathbf{0}$, $\mathbf{S}$, $\boldsymbol{+}$, and $\boldsymbol{\cdot}$, and let $Q$ denote Robinson's arithmetic.
By a ...

**2**

votes

**3**answers

740 views

### An established proof in Wang Tile which I doubt

When I was reading the paper:
Wang, Hao. "Notes on a class of tiling problems." Fundamenta Mathematicae 82.4 (1975): 295-305.
from http://matwbn.icm.edu.pl/ksiazki/fm/fm82/fm82119.pdf
I could not ...

**6**

votes

**1**answer

223 views

### Characterization of intermediate submodels of generic extensions

Question 1: Suppose that $V[G]$ is a set generic extension of $V$ by some forcing notion $P\in V,$ and suppose that $W$ is a model of $ZFC, V \subset W \subset V[G].$ Can we find a forcing notion ...

**2**

votes

**0**answers

317 views

### Topological proof of a result in Logic

I proved the result below using logic. My questions:
Can this theorem be proved by purely topological means?
Do you know any theorems that either can be used to prove the same result, or which give ...

**9**

votes

**2**answers

809 views

### Is there any research on set theory without extensionality axiom?

In practice (say, in computer science), collections with many "labels" ("identities"), or collections which occur in many copies, are more frequently used than sets. Such collections do not satisfy ...

**2**

votes

**1**answer

401 views

### Is this system incomplete?

Let $\mathbf{SBM}$ be the normal modal logic system defined as $\mathbf{T}$ plus the following two axioms:
$$\mathrm{SB}: \Box(\Diamond p \rightarrow p)\rightarrow (p \rightarrow \Box p)$$
...

**4**

votes

**1**answer

82 views

### Counterexample for closedness under union of $\prec_{\infty,\kappa}$ chains

Assume $\kappa$ is uncountable and $\phi$ is an $L_{\infty,\kappa}$ sentence. Let $K$ be the collection of models of $\phi$ partially ordered by $\prec_{\infty,\kappa}$. It is well-known that $K$ is ...

**5**

votes

**2**answers

815 views

### Why can't mathematics be formalised in terms of classes rather than sets? [closed]

I've always been curious about the seeming compulsion to found mathematics upon sets, be it ZF(C) or some other system. Of course, there are other approaches these days like category theory and type ...

**21**

votes

**1**answer

589 views

### Is there a model of ZF set theory with a set that does not inject into the cardinals?

Question. Is there is a model of ZF set theory with a set $X$ that does not inject into the cardinals?
I use the term "cardinal" here in the ZF sense, so they are not necessarily well-orderable.
To ...

**7**

votes

**1**answer

287 views

### Is there a name for infinite words containing every finite words?

Apparently, the closest thing I've found would be normal number http://mathworld.wolfram.com/NormalNumber.html
But requiring that every finite words occurs is weaker than this property. So I'm ...

**4**

votes

**1**answer

177 views

### Necessity of omega-models in second order arithmetic

Are there examples of independence results over subsystems of true second order arithmetic that cannot be established using omega-models? To rule out trivial examples, let us assume that the base ...

**7**

votes

**2**answers

295 views

### Proof complexity of two directions of equivalency?

This question is not precise, but I believe has a precise formulation.
Consider a mathematical theorem which gives an equivalency between two conditions. As an extreme example:
\begin{theorem}
A ...

**7**

votes

**2**answers

341 views

### Are there “non-constructive” sets in second-order arithmetic?

Consider $\phi(A)$ a formula of second-order arithmetic with one free variable $A$ of type "set". Suppose $\exists A : \phi(A)$ is a true sentence. Does it follow (not in second order arithmetic ...

**10**

votes

**4**answers

1k views

### Does formalizing math require search and creativity, or is it near-mechanical?

I remember reading somewhere that it takes about a week to convert a page of math into something a proof-assistant like Isabelle or HOL Light would accept.
Is this type of conversion something that ...

**1**

vote

**0**answers

51 views

### Is it possible to classify all the inequivalent classes of first order sentence with quantifier rank fixed

It is known that for symbols with finite many relations, the number of inequivalent class of first order sentence with quantifier rank $m$ is finite. But is it possible to list (classify) them? At ...

**2**

votes

**1**answer

221 views

### Absolutness of $\Pi_1^1$ statements

Shoenfield absoluteness is well known for $\Pi_2^1$-statements, but it does not hold between a countable transitive model of ZFC and the universe.
But it is also known that $\Pi_1^1$ statements are ...

**12**

votes

**3**answers

455 views

### Formal/rigorous treatment of (im)predicativity/predicativism

There are several places on the web where one may find quite intuitively understandable accounts of (im)predicativity; here on MO I found two questions with very good detailed answers (Predicative ...

**5**

votes

**0**answers

350 views

### Last Status of Feferman's Conjecture on Indefinite Value of Continuum

The "true" value of $2^{\aleph_0}$ is one of the most fundamental open questions of mathematics and its philosophy. Hundreds of set theoretic results during the last century don't say anything more ...

**4**

votes

**2**answers

296 views

### Overspill in models of arithmetic

Assume that $M$ is a non-standard model of complete arithmetic, i.e. of the theory $Th(\mathbb{N})$. Suppose that $R$ and $S$ are proper cuts of $M$. (With a cut, I mean a subset of the universe of ...

**19**

votes

**1**answer

630 views

### Why isn't this a computable description of the ordinal of ZF?

In a previous MO question, I was told by several commenters that
(a) it's known that there exists a computable ordinal $\alpha_{ZF}$ that "encodes the strength of ZF set theory" (i.e., a least ...

**2**

votes

**1**answer

107 views

### Question on deriving $\alpha \rightarrow \Box \alpha$ in modal logic KTU

Let K and T be the usual modal logical principles $\Box (\alpha \rightarrow \beta) \rightarrow (\Box \alpha \rightarrow \Box \beta)$ and $\Box \alpha \rightarrow \alpha$. Let U be the modal logical ...

**2**

votes

**0**answers

120 views

### characterization of all periodic tiling of a simple set of Wang Tile

Consider a set of Wang Tile such that all the edges are either 1 or 0.... there are 16 elements in such a set.
Now, I wish to characterize all the periodic tilings of this set (better if they are ...

**0**

votes

**1**answer

81 views

### Question about the consistency of assuming (via axiom) that $\kappa < \nu$ for certain pairs of cardinal numbers provably satisfying $\kappa \leq \nu$

Call an ordered pair of formulae $\langle P(\kappa,\tilde{a}), Q(\nu,\tilde{a})\rangle$ in the language of $\{\in\}$ unproblematic iff
ZFC proves that for all $\tilde{a}$ and all cardinal numbers ...

**48**

votes

**3**answers

2k views

### How do I verify the Coq proof of Feit-Thompson?

I probably don't have the appropriate background to even ask this question. I know next to nothing about formal or computer-aided proof, and very little even about group theory. And this question is ...

**10**

votes

**1**answer

529 views

### Where can I find Gonthier's Coq code proving the four color theorem?

In a 2008 article in the Notices, Georges Gonthier announced a computer-checked proof of the four color theorem using Coq:
Gonthier, Georges. Formal proof—the four-color theorem.
Notices Amer. ...

**14**

votes

**0**answers

247 views

### Computability of Brauer groups

A friend of mine and I were talking about computable algebra, and this question came up. The answer may already be known, but I couldn't find it with Google:
Suppose I have a countable field, $k$. ...

**0**

votes

**0**answers

125 views

### Basis of periodic tiling of Wang tile

Given a set of Wang tile,
Given 3 periodic tiling: A, B, C
We define 3 vector F[A], F[B], F[C]
each vector correspond to the appearing frequency of each type of tiles in the tiling.
Now, we ...

**1**

vote

**1**answer

90 views

### simple cycle analog in 2D (with application in tiling)

We know that any closed cycle of a graph could be decomposed into sum of simple cycles. To translate this theorem into tiling of 1D (Wang tile). We know that any 1D periodic tiling could be ...

**11**

votes

**1**answer

339 views

### Is it possible for a theorem to be constructive only in a non-constructive metatheory?

There are several theorems in category-theoretic logic which say something like, "any proposition in X logic that is provable in topos logic assuming (the law of excluded middle and) the axiom of ...

**6**

votes

**2**answers

484 views

### Are all functions in Bishop's constructive mathematics continuous?

When I started to write this question I was really confused, but now I think I am starting to get it. Nonetheless I'd like some confirmation that my understanding is correct.
I have read, heard ...

**1**

vote

**1**answer

157 views

### relationship between corner tile and edge tile of wang tile

It is clear that any corner type of Wang Tile could be converted to edge type of Wang Tile by defining the edge color according to the corner color.
However, could we convert edge type of Wang Tile ...

**1**

vote

**0**answers

104 views

### Graph theoretical representation of Wang Tile

We note that for one dimensional tiling problem of Wang Tile could be represented by a graph. Each cycle on the graph represents a periodic solution.
However, is there a well established counter-part ...

**10**

votes

**1**answer

327 views

### Does small forcing preserve CH?

Suppose CH holds and $\mathbb{P}$ is a poset of size $\omega_1$, such that forcing with $\mathbb{P}$ preserves $\omega_1$. Does forcing with $\mathbb{P}$ preserve CH? If $\mathbb{P}$ is proper then ...

**10**

votes

**0**answers

157 views

### Can Gentzen-style proofs give omega-consistency and beyond?

In 1936, Gentzen famously showed that Primitive Recursive Arithmetic, plus the assumption that the ordinal $\epsilon_0$ is well-founded, is able to prove Con(PA). But of course, Con(PA) doesn't yet ...

**14**

votes

**6**answers

2k views

### What “forces” us to accept large cardinal axioms?

Large cardinal axioms are not provable using usual mathematical tools (developed in $\text{ZFC}$).
Their non-existence is consistent with axioms of usual mathematics.
It is provable that some of ...

**3**

votes

**2**answers

212 views

### Sufficient Condition for Defining $\in$

Consider the first order language $\mathcal{L}=\{\in,\in'\}$ with two binary relational symbols $\in , \in'$ and $ZFC$ as a $\{\in\}$-theory. If we define $\in'$ using $\{\in\}$-formula $\varphi(x,y)$ ...

**1**

vote

**1**answer

220 views

### A Special Pair of Formulas

Consider the first order language $\mathcal{L}=\{\in,\subseteq\}$ and $\{\in\}$-theory $\text{ZFC}$. Is there a formula $\psi (x,y) \in \{\subseteq\}-Form$ with the following ...

**27**

votes

**1**answer

814 views

### Is there a computable ordinal encoding the proof strength of ZF? Is it knowable?

In comments on Quora (see, for example, here, here, here), Ron Maimon has repeatedly expressed the strong opinion that Hilbert's program was not killed by Gödel's results in the way typically ...

**10**

votes

**2**answers

595 views

### Questions about Prikry forcing and Cohen forcing

I have some questions.
The first one is about the product of Prikry's forcing.
Let $\kappa$ be a measurable cardinal, $U_1, U_2$ be normal measures on $\kappa$ and let $\mathbb{P}_{U_1}, ...

**6**

votes

**1**answer

216 views

### Sets of cardinalities of bases without choice

For a vector space $V$, let $BS(V)$ be the set of cardinalities (not necessarily $\aleph$s) of bases of $V$. Of course, in ZFC each $BS(V)$ is a singleton, but supposing the axiom of choice fails, it ...

**9**

votes

**1**answer

292 views

### Inner model in which every uncountable cardinal is large

The following is known:
$(*)$ If $0^\sharp$ exists, then any uncountable cardinal is is an inaccessible cardinal (and even more) in $L$.
My question is that:
Are there any large cardinal ...

**3**

votes

**1**answer

155 views

### Proof of existence of recursively inaccessible and Mahlo ordinals

As in title - I'm looking for a proof of the existence of a countable recursively inaccessible or recursively Mahlo ordinals, especially the first one. When looking for it in all the papers I stumbled ...