first-order and higher-order logic, model theory, set theory, proof theory, computability theory, formal languages, definability, interplay of syntax and semantics, constructive logic, intuitionism, philosophical logic, modal logic, completeness, G?del incompleteness, decidability, undecidability, ...

**1**

vote

**1**answer

105 views

### Is $\in$-induction provable in first order Zermelo set theory?

Are there models of first order Zermelo set theory (axiomatized by: Extensionaity, Foundation, empty set, pairing, set union, power, Separation, infinity) in which $\in$-induction fail?
I asked this ...

**1**

vote

**0**answers

55 views

### Natural examples of recursive pseudowellorderings

Question: What are some natural examples of recursive pseudowellorderings?
By natural, I mean in the style of reasonable ordinal notation systems as opposed to dependent on a G?del numbering or an ...

**-4**

votes

**0**answers

49 views

### Predicate logic Maximum [on hold]

If P(x,y) : the pixel on row x and column y is lit.
How would I then express that:
Maximum one pixel is lit on every row
There is at least one row where exactly 1 pixel is lit.
I have tried using ...

**3**

votes

**0**answers

104 views

### Ordinal analysis and nonrecursive ordinals

Ordinal analysis is typically described as characterizing recursive ordinals in a theory $T$, but there is a sense in which it can characterize all $T$-ordinals, even those that are nonrecursive.
...

**5**

votes

**1**answer

186 views

### Progress towards a computational interpretation of the univalence axiom?

I will preface this by saying that I am not an expert on type theory. I am just a curious outsider slowly making my way through the HoTT book when I (rarely) have some spare time.
I am just curious ...

**10**

votes

**1**answer

746 views

### Relation between the Axiom of Choice and a the existence of a hyperplane not containing a vector

In a lot of problems in linear algebra one uses the existence, for each $E$ vector space over a field $k$, and each $x\in E$, of a Hyperplane $H$ such that $E=k\cdot x \oplus H$ (Let us denote $\...

**0**

votes

**0**answers

216 views

### Is there a known shorter axiomatization of NF than this?

Is there an already known axiomtization of $NF$ that is shorter than the following axiomatic system in first order logic with equality $``="$ and membership $``\in"$? And what is exactly meant by ...

**1**

vote

**1**answer

79 views

### Reduction of the predicate calculus to the propositional calculus in the case of one sigle object in the universe? [closed]

To what extent is it possible to formally susbstantiate the following affirmation that: "In a classical first order logical universe with exactly one unique and single object, the predicate calculus ...

**3**

votes

**0**answers

110 views

### If any satisfiable $\mathcal{L}_{κ,κ}(Q_{=κ})$-theory remains satisfiable when replacing $Q_{=κ}$ with $Q_{=μ}$, is $κ$ huge?

Recently, I have asked a model-theoretic question concerning a weakening of different forms of compactness. I now present another model-theoretic question as a weakening of hugeness.
If any ...

**7**

votes

**1**answer

227 views

### Can we inductively define Wadge-well-foundedness?

For a topological space $X$ (which I'll identify with its underlying set of points), we define the Wadge preorder $Wadge(X)$: elements of the preorder are subsets of $X$, and the ordering is given by $...

**0**

votes

**0**answers

60 views

### Functoriality of indiscernible sequences

Let $T$ be a first order theory of, say, some type of combinatorial geometries which contain indiscernible sequences of points. Let $(\Gamma,\mathcal{O})$ be a model of $T$, where $\Gamma$ is the ...

**2**

votes

**0**answers

84 views

### Lengths of proofs and quasilinear time

Length of proofs depends not only on the theory but also on its axiomatization. Once an axiomatization is fixed, typical proof systems are equivalent up to a polynomial factor. But what if we care ...

**0**

votes

**1**answer

290 views

### What are the difficulties involved in proving that the Kunen inconsistency holds in $NGB$

or (contrariwise) that $NGB$ + "There exists a Reinhardt cardinal" is consistent?
The question is partially in the title. $NGB$ is used for the reasons stated in the Hamkins, Kirmayer, and ...

**-7**

votes

**0**answers

466 views

### Is transcendental Goldbach Conjecture true of the real numbers?

Let $x0$ be the real number $Pi$, Consider the below sequence of real numbers:
$s{0}$ = .1415926535897932384626433832795028841971...
$s{1}$ = .415926535897932384626433832795028841971...
$s{2}$ = ....

**6**

votes

**3**answers

793 views

### Are there logical systems where formal proofs are not computer verifiable?

In a set-theoretic system using first-order logic, every proof could be written as a goal followed by a finite sequence of sentence where each one is justified by an axiom or previously established ...