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.

1 vote
0 answers
55 views

Construction of the smallest nucleus above a prenucleus: what does this proof tell us?

While reading Hyland's paper on the effective topos [retyped version here] in the L. E. J. Brouwer Centenary Symposium, specifically prop. 16.3, I realized that the following proposition is implicit: …
Gro-Tsen's user avatar
  • 32.5k
13 votes
2 answers
993 views

What's the deal with De Morgan algebras and Kleene algebras?

The notion of Boolean algebras, and the corresponding classical propositional logic, is very standard, and it is easy to find information about them (for example, among many other such works, there is …
Gro-Tsen's user avatar
  • 32.5k
8 votes
1 answer
298 views

What topos-theoretic construction lies behind the “symmetric model” construction (used to re...

Suppose we want to prove that (classical!) $\mathsf{ZF}$ does not prove, say, “for every infinite set $A \subseteq \{0,1\}^{\mathbb{N}}$ there exists an injection $\mathbb{N} \to A$” (I take this exam …
Gro-Tsen's user avatar
  • 32.5k
3 votes
1 answer
152 views

Stone-Čech compactification of a Boolean subalgebra of $\{0,1\}^S$

Setup: Let $S$ be a set. Let $B$ be a Boolean subalgebra of $\{0,1\}^S$; i.e., just to be clear $B$ contains the constant $0$ and $1$ functions, and is stable under binary pointwise $\land$, $\lor$ a …
Gro-Tsen's user avatar
  • 32.5k
5 votes
1 answer
161 views

Countably compact Boolean algebras versus distributivity

Let us say that a complete Boolean algebra $B$ is: countably distributive when for any sequence $(I_n)_{n\in\mathbb{N}}$ of sets and any elements $(u_{n,i})_{n\in\mathbb{N},i\in I_n}$ of $B$ we have …
Gro-Tsen's user avatar
  • 32.5k
10 votes
0 answers
144 views

Closed sets versus closed sublocales in general topology in constructive math

This question is set in constructive mathematics (without Choice), such as in the internal logic of a topos with natural numbers object, or in IZF. Short version of the question: if $X$ is a sober top …
Gro-Tsen's user avatar
  • 32.5k
8 votes
2 answers
496 views

Condition to guarantee that an inhabited and bounded set of reals has a supremum

This question is about constructive mathematics (without Choice), such as in the internal logic of a topos with natural numbers object, or in IZF. The “reals” (and the symbol $\mathbb{R}$) refer to t …
Gro-Tsen's user avatar
  • 32.5k
14 votes
3 answers
1k views

Examples of concrete games to apply Borel determinacy to

I'm teaching a course on various mathematical aspects of games, and I'd like to find some examples to illustrate Borel determinacy. Open or closed determinacy is easy to motivate because it proves th …
Gro-Tsen's user avatar
  • 32.5k
5 votes
0 answers
151 views

What is known about propositional realizability for the second Kleene algebra and related PCAs?

Short version: Various things are known about realizability of propositional formulas for Kleene's “first algebra” (i.e., $\mathbb{N}$), like examples of realizable but unprovable formulas, and some t …
Gro-Tsen's user avatar
  • 32.5k
7 votes
0 answers
155 views

Logical properties of realizability (topoi or McCarty models) defined by alpha-recursion on ...

Setup: Let $\alpha$ be an admissible ordinal (viꝫ., one such that $L_\alpha$ is a model of Kripke-Platek set theory), identified as usual with the set of ordinals $<\alpha$. Then there is a standard …
Gro-Tsen's user avatar
  • 32.5k
6 votes
1 answer
289 views

Need help in trying to understand an argument by V. A. Yankov on the nonrealizability of Sco...

(This is really long because I give a lot of context, but you can skip right to the end where the excerpt I'm trying to make sense of is copied and translated.) Background: I'm trying to understand th …
Gro-Tsen's user avatar
  • 32.5k
13 votes
0 answers
251 views

Intuitionistic proofs of propositional formulae versus natural transformations between finit...

The setup: Given a formula $\varphi$ of intuitionistic propositional logic (i.e., made from the connectors $\Rightarrow$, $\land$, $\lor$, $\top$ and $\bot$ from propositional variables $A,B,C,\ldots$ …
Gro-Tsen's user avatar
  • 32.5k
14 votes
1 answer
545 views

How exactly are realizability and the Curry-Howard correspondence related?

Consider, on the one hand: the Curry-Howard correspondence between, on the one hand, types and terms (programs) in various flavors of typed $\lambda$-calculus, and on the other, propositions and proo …
Gro-Tsen's user avatar
  • 32.5k
12 votes
2 answers
424 views

Trading Choice for Comprehension (or Replacement)

This question is basically a request for clarification about a remark made by Sam Sanders in a comment to another question: IIUC what he's saying, there are statements that can be proved either with a …
Gro-Tsen's user avatar
  • 32.5k
8 votes
2 answers
581 views

Turing degrees of sets separating two computably inseparable sets (theorems and antitheorems)

Let $A\subseteq\mathbb{N}$ be the set of Gödel codes of theorems of Peano arithmetic, and $B\subseteq\mathbb{N}$ be the set of codes of antitheorems (i.e, refutable statements, statements whose negati …
Gro-Tsen's user avatar
  • 32.5k

15 30 50 per page