136 reputation
3
bio website lri.fr/~rouxcody
location Orsay, France
age
visits member for 2 years
seen 2 days ago

I am currently a postdoc in theoretical computer science, my main fields of interest revolve around logic and type theory, termination checking, satisfiability modulo theories.


Mar
17
comment Why can't you pick socks using coin flips?
As a more concrete example, the Hahn-Banach theorem is a powerful and useful theorem of Hilbert spaces which is commonly used in QM and operator theory.
Feb
27
comment Is there any point in a logician studying $\infty$-categories?
Constructive mathematics is actually relevant to mathematicians at large! Who would have thunk it? Also; Topoi are constructive in general: the algebra of open sets of a space is Heyting but not Boolean in general.
Feb
20
comment Smallest next real number after an integer
It's not just you! One possible way to do this (quite naturally) is by constructing the "surreal numbers": en.wikipedia.org/wiki/Surreal_number. The clean cut definitions are a bit technical though, so you might want to look at some of the references at the end of the article.
Oct
17
awarded  Critic
May
30
comment Why do we believe the Church-Turing Thesis?
@NickKidman: Light travels always at the same speed relative to the observer regardless of the situation. However, light traveling from a point near the edge of a black hole may be very hard to detect, as it has been red-shifted to possibly extreme amounts.
Mar
28
comment Why do we negate the imaginary part when conjugating?
Well of course it's possible to elaborate on this notion of duality: the conjugation operator can be seen as the extension a map which sends roots of the polynomial $X^2 + 1$ to roots of the same, and it is the only such map other than the identity. The study of these maps is the main object of Galois theory.
Mar
7
comment Could I be using proof by contradiction too much?
You have made a common mistake: Cantor's diagonal argument is a proof of a negative statement, and as such is perfectly valid proof in the intuitionistic framework. Additionaly, the Axiom of infinity is not rejected by all intuitionists, though the schism between intuitionist mathematics and classical mathematics is more significant in situations where that axiom holds.
Nov
12
comment Decomposing $\mathbb{N}$
Hint: split $\mathbb{N}$ into two infinite disjoint sets, one of which will be all of $N_1$, the other which will contain most of the elements of each $N_i$, $i\geq 2$...
Oct
18
comment Are the “proofs by contradiction” weaker than other proofs?
I want to add that constructive proofs have computational content: if you prove the existence of an object, it is possible to perform a computation and obtain (a representation of) that object. In this sense it seems reasonable to reject non-constructive proofs of existence, as they give absolutely no method of obtaining a description of the asserted object.
May
25
comment A Formal and Precise treatment of Simplification?
Just googling "rewriting" might be a bit too general. You might want to check out "Shostak theories" which are logical theories in which one has a natural notion of "canonical form" and of "solution of an equation". The field of rewriting is so incredibly vast, however, that you might start with the Baader & Nipkow reference to get a grip on the different subfields.
Mar
27
awarded  Supporter
Mar
27
awarded  Teacher
Mar
26
answered A Formal and Precise treatment of Simplification?