1,446 reputation
28
bio website
location
age
visits member for 1 year, 2 months
seen 7 hours ago

Jan
22
awarded  Yearling
Nov
9
answered Why do class-sized models escape the completeness theorem?
Sep
16
answered “Kolmogorov complexity with time”
Sep
14
revised What practical proofs work in intuitionistic but not minimal logic?
said where ex falso was necessary
Sep
14
revised What practical proofs work in intuitionistic but not minimal logic?
added 1343 characters in body
Sep
14
comment What practical proofs work in intuitionistic but not minimal logic?
@CarlMummert I'll edit to explain.
Sep
14
answered What practical proofs work in intuitionistic but not minimal logic?
Sep
11
comment Does this variant of unrestricted comprehension fall prey to a modified Russell's paradox?
I mean from $(A \in \{A\} \wedge \{A\}\in A)$ deduce $\exists y(y \in \{A\} \wedge \{A\} \in y)$. In other words, there is a $y$ such that $y \in \{A\} \wedge \{A\} \in y$, because $A$ is an example of such a $y$. Then $x := \{A\}$ cannot satisfy $x \neq A \wedge \neg (\exists y(x \in y \wedge y \in x))$, so $\{A\} \notin A$.
Sep
11
comment Does this variant of unrestricted comprehension fall prey to a modified Russell's paradox?
Deduce $\exists y(y \in \{A\}\wedge\{A\}\in y)$ by setting $y := A$ and applying the assumption that $\{A\} \in A$. This sort of thing is a bit tricky.
Sep
10
revised Does this variant of unrestricted comprehension fall prey to a modified Russell's paradox?
edited body
Sep
10
comment Does this variant of unrestricted comprehension fall prey to a modified Russell's paradox?
Oh I see, I'll fix it.
Sep
10
answered Does this variant of unrestricted comprehension fall prey to a modified Russell's paradox?
Sep
10
comment Does this variant of unrestricted comprehension fall prey to a modified Russell's paradox?
As it stands, your axiom scheme is consistent: consider the model with one element, $\ast$, and define $\in$ by $\ast \notin \ast$. If you add the axiom $\exists x, y\; x \in y$ it might make something like Russell's paradox work. I'll think about it.
Aug
29
comment What does $x : X$ mean?
Note also that $\Pi_{x:\mathbb{N}}A$ is a type not dependent on $x$ and finding a proof of $\Pi_{x:\mathbb{N}}A$ in the empty context is equivalent to finding a proof of $A$ in the context $x:A$.
Aug
29
comment What does $x : X$ mean?
Let $A$ be a term for a type, with a free variable $x$ such that $x: \mathbb{N}$ appears in the context (a dependent type). For example $A := I_\mathbb{N}(x+1, 0) \rightarrow \bot$. You are free to say either "$A$ is a type when $x$ is of type $\mathbb{N}$" or "$A$ is a family of types indexed by $\mathbb{N}$." I would say the latter is more common, but both are valid interpretations.
Aug
29
comment What does $x : X$ mean?
A valid expression would be $x : \mathbb{N} \vdash t : I_\mathbb{N}(x + 1, 0) \rightarrow \bot$, where $I_\mathbb{N}(x + 1, 0)$ is the type of "proofs that $x+1$ and $0$ are equal", $\bot$ is the empty type and $t$ is a term that you need to find.
Aug
29
comment What does $x : X$ mean?
Like Zhen Lin said, $x$ should not be bound on the right hand side. Another issue is that $x + 1 \neq 0$ is not a valid judgement, because every judgement is either of the form $t : A$ or $t \equiv s : A$. To express what you want, you need to use identity types.
Aug
29
answered What does $x : X$ mean?
Aug
13
answered How can some statements be consistent with intuitionistic logic but not classical logic, when intuitionistic logic proves not not LEM?
Jul
28
comment When adjoining a new sort that is supposed to model the powerset of the original domain of discourse, what is the appropriate notion of embedding?
In NBG the extra axioms are (strengthened) foundation and limitation of size.