174 reputation
6
bio website
location
age
visits member for 3 years, 2 months
seen Jun 13 at 14:09

May
18
comment What is the name for the operation of swapping the two components of a complex number (rectangular form)?
@DanielFischer: Thanks. Maybe you want to put it as an answer?
May
18
comment What is the name for the operation of swapping the two components of a complex number (rectangular form)?
@JasonChen: Yes.
May
18
asked What is the name for the operation of swapping the two components of a complex number (rectangular form)?
Jul
1
comment Predicate vs function
Thanks for the answer. So the role of function symbols cannot be unified into predicate symbols, we do need them, even though their functionality can be simulated by a predicate (together with the uniqueness condition). But it seems not all their functionality can be simulated. In particular, I do not know how to simulate those function symbols that act as constructors, for example, succ, and zero (a so-called constant, which is typically regarded as a function symbol of zero arity). Do you have any idea?
Jun
30
comment Predicate vs function
Great answer by providing both syntactic and semantic point of view. For "and while we cannot use this to create syntactical terms, we can always write a formula and require that a variable satisfies this condition", I would appreciate if you could elaborate a bit more. What does the first "this" stand for? Why can we not use it to create syntactic terms? How to write such a formula and require what variable to satisfy the uniqueness condition? It would be clearer if we consider the function symbols zero and succ for Peano numbers. Could you illustrate your point for them? Thanks.
Jun
30
awarded  Critic
Jun
3
comment What is the intuition behind the “par” operator in linear logic?
$\DeclareMathOperator{\par}{\unicode{8523}}$ The encoding of $A \multimap A$ should be $A^\bot \par A$.
May
3
comment What is the notion for this arrow in category theory?
Ah, of course, thanks. Unfortunately you did not put it into an answer.
May
3
asked What is the notion for this arrow in category theory?
Mar
3
awarded  Teacher
Mar
3
answered Universal quantification via lambda binding?
Mar
3
awarded  Tumbleweed
Feb
24
asked Universal quantification via lambda binding?
Jan
6
comment What's the meaning of algebraic data type?
@hardmath: The simple example does demonstrate constructors, of type () -> Weekday.
Jan
6
comment What's the meaning of algebraic data type?
Typo: "... or it contains 2 elements ($X^3$) ...", the term in parentheses should be $X^2$.
May
29
awarded  Scholar
May
29
accepted What is the so-called eigenvariable or parameter in natural deduction?
May
29
accepted What's wrong with this inference in natural deduction?
May
25
comment What is the so-called eigenvariable or parameter in natural deduction?
Thanks, Charles. Concerning your third paragraph, my question is it seems to me that in the intr or elim rule for a single universally quantified formula, these two kinds of variables don't occur at the same time, above the intr node no universally quantified variable but only what you called existentially quantified one, below vice versa. How do you explain this? Another question, your first sentence mentioned "the usual formalization", I suppose there are unusual ones? Could you point to me one? Thanks.
May
24
awarded  Student