Petr Pudlák
Reputation
1,571
Top tag
Next privilege 2,000 Rep.
 Apr1 comment Eilenberg Moore category Did you manage to construct E-M categories in Haskell? I'd be quite interested. Sep30 awarded Explainer Sep30 answered Fixed point combinator and functions with no fixed point Aug26 awarded Popular Question Aug8 awarded Yearling Jul11 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$. Jul11 revised How or why does intutionistic logic proof negations from within the theory, constructively? added 2359 characters in body Jul8 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. Jul7 answered How or why does intutionistic logic proof negations from within the theory, constructively? Jan8 comment Automatic theorem prover for proving simple theorems? Are you interested in propositional logic or first-order logic? Aug8 awarded Yearling Jun29 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. Jun29 comment Prove p from ¬¬p No problem, I added it to my answer. Jun29 revised Prove p from ¬¬p Added a proof of $\phi\Rightarrow\phi$. Jun15 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. Jun10 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. Jun9 answered Prove p from ¬¬p Jun9 awarded Citizen Patrol Jun8 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. Jun8 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.