1,536 reputation
28
bio website
location
age
visits member for 1 year, 9 months
seen 9 hours ago

2d
answered Formal notion of computational content
May
26
comment Goedel's completeness theorem in and/or for intuitionistic first order logic
No problem! I rambled on a bit more than I intended; the comments about Markov's principle are actually unnecessary since I remembered Espinaldo's paper, but I'll leave them up in case they're useful.
May
21
comment Goedel's completeness theorem in and/or for intuitionistic first order logic
Regarding the completeness of Kripke models again, I've just remembered there's been some recent work by Espinaldo in this area. See Espinaldo, Semantic Completeness of First-Order Theories in Constructive Reverse Mathematics. As a corollary of his work, one can see that a general form of completeness for Kripke models is equivalent to excluded middle + the boolean prime ideal axiom. There are also references to earlier results in the same paper.
May
21
comment Goedel's completeness theorem in and/or for intuitionistic first order logic
Also I should point out that there are variants of Kripke models that have constructive completeness proofs (this is mentioned on the same SEP page I linked to above).
May
21
comment Goedel's completeness theorem in and/or for intuitionistic first order logic
The thing is, that even with a classical proof one can give an algorithm that works but is very inefficient: just run through every potential proof and check them one by one until you find one that works. I think a proof that requires Markov's principle could give a similarly inefficient and impractical algorithm. An algorithm based on sheaf models (which don't, I believe, require Markov's principle) could I think be much more efficient and maybe even work well in practice. I hope that helps.
May
21
comment Goedel's completeness theorem in and/or for intuitionistic first order logic
On Kripke models, the usual completeness proofs for example in Troelstra and van Dalen, Constructivism in Mathematics use excluded middle, but I found it hard to find a proof that it is stricly necessary. The SEP page on intuitionistic logic mentions that Kreisel showed that it requires Markov's Principle. This is actually not so bad constructively speaking, but it could cause a problem when it comes to extracting an algorithm.
May
21
comment Goedel's completeness theorem in and/or for intuitionistic first order logic
The thing about toposes is that certain basic propositions, like "sheaf toposes are toposes" require the power set axiom. This turns out to not be a problem when it comes to extracting algorithms, but power set is rejected by many constructivists for being "impredicative". In particular it is not usually part of type theory.
May
20
answered Goedel's completeness theorem in and/or for intuitionistic first order logic
May
20
comment Finite set with unknown number of elements
I think actually it's still okay. I'm claiming that it's a subfinite set, so it only needs to be a subset of a finitely enumerable set, which certainly includes the empty set. In any case $0$, which is implemented as the empty set is a natural number, so $\emptyset$ is finitely enumerable (on the other hand it is not countable).
May
20
comment Finite set with unknown number of elements
Maybe I'm misunderstanding your example. Certainly for a fixed $n$ the set $\{0,\ldots,n\}$ is finite, and your example appears to be a subset of this obtained by a single instance of separation.
May
20
answered Finite set with unknown number of elements
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.