Skip to main content
Search type Search syntax
Tags [tag]
Exact "words here"
Author user:1234
user:me (yours)
Score score:3 (3+)
score:0 (none)
Answers answers:3 (3+)
answers:0 (none)
isaccepted:yes
hasaccepted:no
inquestion:1234
Views views:250
Code code:"if (foo != bar)"
Sections title:apples
body:"apples oranges"
URL url:"*.example.com"
Saves in:saves
Status closed:yes
duplicate:no
migrated:no
wiki:no
Types is:question
is:answer
Exclude -[tag]
-apples
For more details on advanced search visit our help page
Results tagged with
Search options questions only not deleted user 17064

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, theories of truth, truth revision, consistency.

18 votes
1 answer
366 views

Proof as a Σ₁ approximation to truth: what about higher degrees?

Let us posit that the goal of mathematics is to study mathematical truths, and let us stick to arithmetic for simplicity: so let $\mathscr{T} \subseteq \mathbb{N}$ be the set of (Gödel codes of) true …
Gro-Tsen's user avatar
  • 32.5k
12 votes
1 answer
296 views

Does this "mixable" property have a standard name in constructive mathematics?

While thinking about constructive mathematics, I stumbled on the following notion, and I would like to know if it has a standard name, a simpler equivalent, or has appeared in the literature: Say tha …
Gro-Tsen's user avatar
  • 32.5k
4 votes
1 answer
195 views

Does second-order Heyting arithmetic have the disjunction and existence properties?

Consider full second-order Heyting arithmetic, axiomatized in two-sorted first-order intuitionistic logic (with “number” and “class” variables) by the usual Peano axioms (with induction being stated q …
Gro-Tsen's user avatar
  • 32.5k
9 votes
1 answer
333 views

Are finitely enumerated and subfinite sets Dedekind-finite?

The context of this question is constructive mathematics, such as in the internal logic of a topos with natural numbers object, or in IZF. Let us say that a set $X$ is: finite when there exists a nat …
Gro-Tsen's user avatar
  • 32.5k
5 votes
1 answer
314 views

Does the Rieger-Nishimura lattice over a subset of $\mathbb{R}^k$ stabilize?

Notation: If $U,V$ are open subsets of a topological space $X$, let us write $U\Rrightarrow V$ for the Heyting operation: the largest open subset $W$ of $X$ such that $U\cap W \subseteq V$ (i.e., the …
Gro-Tsen's user avatar
  • 32.5k
10 votes
1 answer
403 views

Examples of Kreisel-Putnam topological spaces

Let us say that a topological space $X$ is a Kreisel-Putnam space when it satisfies the following property: For all open sets $V_1, V_2$ and regular open set $W$ of $X$, if a point $x\in X$ has a …
Gro-Tsen's user avatar
  • 32.5k
10 votes
1 answer
366 views

Fibers of the morphism from the free Heyting algebra to the free Boolean algebra

For $k\in\mathbb{N}$, let $H_k$ be the free Heyting algebra on $k$ variables $p_1,\ldots,p_k$ and $B_k$ be the free Boolean algebra on the same $k$ variables. Thus, $B_k$ has $2^{2^k}$ elements (corr …
Gro-Tsen's user avatar
  • 32.5k
4 votes
1 answer
353 views

Is there a correspondence between principles of omniscience and computability classes?

My question will be speculative and therefore a little vague. I wonder if attempts have been made to define a correspondence between, on the one hand, limited principles of omniscience that can be add …
Gro-Tsen's user avatar
  • 32.5k
11 votes
2 answers
707 views

Is there a modern account of Veblen functions of *several* variables?

Veblen $\phi$ functions extend the $\xi \mapsto \phi(\xi) := \omega^\xi$ and the $\xi \mapsto \phi(1,\xi) := \varepsilon_\xi$ functions on the ordinals by repeatedly taking fixed points (I won't repea …
Gro-Tsen's user avatar
  • 32.5k
7 votes
2 answers
469 views

What is the strength of “if $c≥0$ then $[0,c] = c·[0,1]$” in constructive math (w.r.t., LPO,...

Context: This question is about constructive mathematics, such as in the internal logic of a topos with natural numbers object, or in IZF. (I wish to avoid the axiom of countable choice if possible, …
Gro-Tsen's user avatar
  • 32.5k
3 votes
2 answers
501 views

Various notions of Turing reduction for partial functions

If $f$ and $g$ are partial functions $\mathbb{N} \to \mathbb{N}$, define six preorder relations $f \preceq g$ as follows: $f \mathop{\preceq_{\mathrm{S}}} g$ ("$f$ is strict/Sasso reducible to $g$") …
6 votes
1 answer
178 views

Variable elimination for propositional formulas in Heyting algebras

By an (intuitionistic) propositional formula $\varphi(x_1,\ldots,x_n)$ I mean a formula built up from a (finite) number of variables $x_1,\ldots,x_n$ using connectors $\top, \bot, \land, \lor, \Righta …
Gro-Tsen's user avatar
  • 32.5k
7 votes
1 answer
135 views

Invertibility and comparison to zero in the MacNeille sections (bounded extended reals)

(The following three paragraphs are given for context. Readers already aware of the terminology can skip to “the problem” below.) In a spatial topos $\mathop{\textbf{Sh}}(X)$ the MacNeille sections ( …
Gro-Tsen's user avatar
  • 32.5k
6 votes
1 answer
301 views

What is the power of the “anti-halting” oracle?

Let me first ask the question, and then, as it may seem a bit cryptic, explain how it comes up (and whence the “anti-halting oracle” in the title): Notations: we write $\langle m,n\rangle$ for a stand …
Gro-Tsen's user avatar
  • 32.5k
5 votes
1 answer
116 views

Understanding the definition of a (computably / continuously) “transparent” function

The following definitions of a “transparent function” are essentially taken from references [1] (where it is called a “jump operator”), [2] and [3], except that the variation “primitively recursively …
Gro-Tsen's user avatar
  • 32.5k

15 30 50 per page