meta user
network profile
| bio | website | textproof.com/stewart |
|---|---|---|
| location | Berlin, Germany | |
| age | 43 | |
| visits | member for | 2 years, 10 months |
| seen | May 18 at 13:16 | |
| stats | profile views | 359 |
Freelance copy-editor.
You can read my irregular waffles at advogato.org/person/chalst/.
I have a Math Overflow account.
|
May 15 |
comment |
Cardinality of the set of prime numbers +1 for avoiding Axiom-of-choice -strength principles in your answer. |
|
May 7 |
awarded | Caucus |
|
May 3 |
comment |
Why an inconsistent formal system can prove everything? @Joshua: All the theorems and valid inference rules involving $\perp$ are still theorems/ valid rules if you substitute that symbol by any other proposition: there is no difference between that symbol and a schematic variable. |
|
Apr 12 |
comment |
Direct cut-elimination for natural deduction. Peter: Thanks; I probably subconsciously "borrowed" from Girard's treatment of the topic in Ch. 10 of Proofs and Types: paultaylor.eu/stable/Proofs+Types.html |
|
Apr 12 |
comment |
Direct cut-elimination for natural deduction. The key innovation in Prawitz's treatment that eluded Gentzen was how he handled formulae in rules with indirect elimination rules, which are needed for disjunction and existential elimination. You need to think of paths of formulae through these rules, and add permutations to the system to ensure that introduction and elimination rules can meet up. |
|
Apr 8 |
answered | Alternative set theories |
|
Nov 14 |
answered | Why is the set of all real numbers uncountable? |
|
Nov 13 |
reviewed | Reviewed Why is the affine hull of the unit circle R^2? |
|
Nov 13 |
answered | Are coinductive proofs necessary? |
|
Nov 13 |
revised |
What is the difference between these two convergence notations: $f_n \to f$ and $f_n \nearrow f$ or $f_n \searrow f$ edited tags |
|
Nov 12 |
comment |
Logical Operators priorities "mathematical logicians are somewhat more likely to use the former" - I've seen the non-Curry-friendly associativity used for implication, but that I can recall, only together with the exponential notation (i.e. $A^B$ for $B \rightarrow A$). My look over my (mostly set theory, category theory, modal logic, type theory and algebraic logic) bookshelf suggests that when they use arrows for implication, mathematical logicians are most likely to prefer parentheses over an associativity rule, but otherwise, they always go for right associativity. What makes you think the opposite? |
|
Nov 11 |
reviewed | Reviewed Probability Question: Poisson and pmf |
|
Nov 11 |
awarded | Custodian |
|
Nov 11 |
reviewed | Reviewed Suppose $(Y,\tau')$ is Hausdorff and a function $f : (X,\tau)\to (Y,\tau')$ |
|
Nov 11 |
answered | Help proving $ \sim \sim (p \to q),\sim \sim p \vdash \sim \sim q $ with intuitionistic axioms |
|
Nov 9 |
comment |
Is the associative property of XOR provable or axiomatic? @trideceth12: The best I saw was a YouTube video - you have to watch over 3 minutes to see what is going on, so maybe a question here is more useful. Link - youtube.com/watch?v=tpdDlsg4Cws |
|
Nov 8 |
comment |
Is the associative property of XOR provable or axiomatic? @trideceth12: Yes, it's a ternary operator, with four clauses, one for each row ending with a 1 for the last column. The first row is $\neg p \wedge \neg q \wedge r$, and you or all the clauses together to get the DNF. This process must be described somewhere; I'll take a look. |
|
Nov 8 |
answered | Is the associative property of XOR provable or axiomatic? |
|
Nov 7 |
answered | Why does mathematical convention deal so ineptly with multisets? |
|
Nov 7 |
comment |
Squaring inequality $a>b+c$ It's easy to check your proof by thinking of it geometrically: draw a square with side b+c: the squares with sides b and c can be fitted with space left over, and the larger square fits inside the square of side a. |
