1,451 reputation
114
bio website petr.pudlak.name
location Czech Republic
age
visits member for 1 year, 11 months
seen Jul 15 at 19:12

Jul
11
comment How or why does intutionistic logic proof negations from within the theory, constructively?
@NikolajK True. I extended the answer showing how one can interpret $A\to\bot$.
Jul
11
revised How or why does intutionistic logic proof negations from within the theory, constructively?
added 2359 characters in body
Jul
8
comment Lamport claims there is an error in Kelley's proof of the Schroeder-Bernstein theorem. What is it?
Would the proof be correct if we counted the (in)finiteness of ancestral sequences, instead of their cardinality? That is, count cycles as infinite sequences.
Jul
7
answered How or why does intutionistic logic proof negations from within the theory, constructively?
Jan
8
comment Automatic theorem prover for proving simple theorems?
Are you interested in propositional logic or first-order logic?
Sep
14
comment How to express paritioning of a set into two exact halfs using combinatorial species?
@ZhenLin I'd like to express it using the basic operations (which are described in the Wikipedia article).
Sep
14
revised How to express paritioning of a set into two exact halfs using combinatorial species?
added 24 characters in body
Sep
14
revised How to express paritioning of a set into two exact halfs using combinatorial species?
added 55 characters in body
Sep
14
asked How to express paritioning of a set into two exact halfs using combinatorial species?
Aug
8
awarded  Yearling
Jun
29
comment Intuition of implication in propositional logic
Another analogy is: If you don't eat your vegetables, you don't get your desert. If you don't eat the vegetables, I keep the promise and I won't give you the desert. If you do eat them, I don't have to do anything (because the premise is false). Neither way I'm obliged to give you the desert.
Jun
29
comment Prove p from ¬¬p
No problem, I added it to my answer.
Jun
29
revised Prove p from ¬¬p
Added a proof of $\phi\Rightarrow\phi$.
Jun
15
comment Prove p from ¬¬p
That's much better. It's correct now, except for step 4). In this logic system, you have no notion of $\lor$, and if you had, you have to prove its relation to $\Rightarrow$ as well as that $p\lor\lnot p$ is a tautology. Hint: You can prove $\phi\Rightarrow\phi$ by taking a suitable instance of ID and then using using MP twice, each time using a (different) suitable instance of II.
Jun
10
comment Prove p from ¬¬p
You've made several mistakes. The most important is in 2-3 where you eliminate the double negation. This is what you're trying to prove! So you've created a circular proof. Less important: It's true that $a \Rightarrow a$ is valid, but you have to prove it. Also you use the rule $b,\, a \Rightarrow (b\Rightarrow c)\,\vdash\, a\Rightarrow c$, which you need to prove first. Also, to derive 5 you don't need 4 (it's an axiom). Derivation of 7 from 6 doesn't make any sense to me.
Jun
9
answered Prove p from ¬¬p
Jun
9
awarded  Citizen Patrol
Jun
8
comment Is there an algorithm to separate lambda calculus terms using Böhm's theorem?
Oh, I didn't understand that you meant the combinators - the convention is that lower case letters are reserved for variables.
Jun
8
comment Is there an algorithm to separate lambda calculus terms using Böhm's theorem?
This has been answered recently on CS. Note that you can't separate $i$ and $k$, because they have free variables. Böhm's theorem applies only for closed terms.
Jun
1
accepted What is the distribution of primes modulo $n$?