Search Results
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 |
7
votes
3
answers
687
views
Is there a completeness proof of intuitionistic predicate calculus using Heyting algebra sem...
According to godelian in Henkin-style completeness proofs for intuitionistic logic there are multiple intuitionstically valid proofs of the completeness of inuitionistic predicate calculus (IPC) via m …
6
votes
1
answer
454
views
How do working constructivists get by with out the zero product property?
It is stated by Douglas Bridges in Constructive mathematics: a foundation for computable analysis that the following property, which I will call the zero product property:
If $x,y \in \mathbb{R}$ and …
3
votes
1
answer
325
views
Subset Collection axiom
In Constructive Set Theory (CZF) the Power Set axiom is replaced with the Subset Collection axiom which I will state here:
$$ \exists c \forall u [\forall x \in a \exists y \in b (\psi(x,y,u)) \longri …
4
votes
0
answers
349
views
Is intuitionistic predicate logic (semantically) complete or incomplete?
According to Constructivism in Mathematics: An Introduction by Troelstra A.S. and Van Dalen (https://archive.org/details/constructivismin0002troe/page/718/mode/2up) it is proven in an intuitionisitc m …
2
votes
0
answers
146
views
In a constructive order/lattice theory are the arbitrary join and the weak suprema the same?
For a poset $X$ we define an upperbound $w \in X$ of a subset $S \subseteq X$ to be a weak-supremum if
$(\forall a \in S (a \leq b)) \implies w \leq b$.
While a supremum is defined more carefully (in …
8
votes
1
answer
298
views
In CZF (w/ Subset Collection removed) the Powerset axiom Implies Subset Collection
The Subset Collection axiom:
$$ \forall a \forall b \exists c \forall u [\forall x \in a \exists y \in b (\psi(x,y,u)) \longrightarrow \exists d \in c (\forall x \in a \exists y \in d (\psi(x,y,u)) \l …