5
votes
1answer
64 views

What bar should be used for definition of (formal) languages?

I wanted to know which standard symbol should be used as a delimiter when recursively defining a (formal) language, such as this fragment of arithmetic expressions : X ::= 0 | 1 | X+X | X*X | I use ...
7
votes
3answers
286 views

Designing a new tuple of Algebra Operators

It's neccessary to have at least two extra tuples of Albera Operators. A minimal tuple is a triple (to_be_subset_eq, meet_operator, join_operator). There are some ideas how to make 2 extra tupes. ...
8
votes
2answers
272 views

Space that disappears at the edges (beginning/end) of a math formula

Is there a way to produce a space that disappears at the beginning or end of a math formula? Idea: For the formula-final case, something that looks ahead or takes an obligatory argument might be a ...
9
votes
1answer
144 views

Can I use a written out logical connective, rather than a symbol?

My professor uses these really nice, written out, AND and IMPLIES, etc., symbols and I can't seem to figure out or find how he does it. I would love to use them, rather than \wedge or \land. Is it ...
3
votes
1answer
328 views

prooftree from bussproofs package inside “cases” environment

I am using bussproofs package to provide some type proofs. According to bussproofs manual, it is impossible to use prooftree inside math mode. However, I would like to insert prooftree in the cases ...
4
votes
1answer
641 views

negated double turnstile

I'm new to the turnstile package, and I'm trying to figure out how to get a negated double turnstile sign, like the one with the regular \nvDash, but that allows me to have arguments above and below ...
9
votes
2answers
2k views

How to get monospace logic formulas?

The following does not work in LaTeX because logic symbols can only be used in maths mode: \texttt{\forall x(\exists y((f(x)=y)\land(\neg(g(y)=y))))} I want to do this to stress the nature of such ...