day
Reputation
Top tag
Next privilege 250 Rep.
 May18 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? May18 comment What is the name for the operation of swapping the two components of a complex number (rectangular form)? @JasonChen: Yes. May18 asked What is the name for the operation of swapping the two components of a complex number (rectangular form)? Jul1 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? Jun30 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. Jun30 awarded Critic Jun3 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$. May3 comment What is the notion for this arrow in category theory? Ah, of course, thanks. Unfortunately you did not put it into an answer. May3 asked What is the notion for this arrow in category theory? Mar3 awarded Teacher Mar3 answered Universal quantification via lambda binding? Mar3 awarded Tumbleweed Feb24 asked Universal quantification via lambda binding? Jan6 comment What's the meaning of algebraic data type? @hardmath: The simple example does demonstrate constructors, of type () -> Weekday. Jan6 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$. May29 awarded Scholar May29 accepted What is the so-called eigenvariable or parameter in natural deduction? May29 accepted What's wrong with this inference in natural deduction? May25 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. May24 awarded Student