## (1) What are the grammatical rules for specifying a semantics?

<semantics> ::= <principle>

<principle> ::= <classical-principle>

| it isn't the case that <principle>

| <principle> and <principle>

| <principle> or <principle>

| if <principle> then <principle>

| there exists <quantified-upon> such that <principle>

| for all <quantified-upon>, <principle>

| <set> is the intersection of all subsets of A that satisfy <principle>

| <set> is maximal w.r.t. <principle>

| <set> is minimal w.r.t. <principle>

| <complex-set> is a subset of <complex-set>

| <argument> is in <domain>

<classical-principle> ::= <set> is conflict-free

| <set> satisfies admissibility

| <set> satisfies reinstatement

<quantified-upon> ::= <argument> ℜ <argument>

| <argument> in <set>

| <set> subset of <set>

<complex-set> ::= <domain>

| <complex-set> union <complex-set>

| <complex-set> intersection <complex-set>

| A \ <complex-set>

| ℜ⁺ <set>

| ℜ⁻ <set>

<domain> ::= <set>

| ℜ⁺ <argument>

| ℜ⁻ <argument>

<set> ::= A | S | S1 | S2 | S3 | ...

<argument> ::= a | b | c | ... | x | y | z

<semantics> ::= <principle>

## (2) At some point, not all symbols a, b, c,..., x, y, z or S1, S2, S3,...

are available to choose from?

S1, S2, S3,... are variables denoting sets of arguments.

So, they should only occur quantified.

When <principle> is developed into "<argument> is in
<domain>", the scroll menu therefore only allows to choose between
variables that are currently quantified.

By contrast, A and S are not variables (hence they can always be chosen to expand <set>).

## (3) There is a warning pop-up "Would you really want to use ...?

When
<quantified-upon> is developed, if a variable chosen for
<argument> or <set> is already quantified, then there is a
warning pop-up:

The user must decide whether the new occurrence of the variable
introduces a new quantification, in which case the user must choose a
fresh variable.

**Example:**

Assume that "For all a in S, there exists <quantified-upon> such
that <principle>" is expanded by developing
<quantified-upon> into "<argument> ℜ <argument>".

Assume further that the user chooses "b" to develop the first
<argument> and chooses "a" to develop the second <argument>.

There is a warning pop-up "Would you really want to use a?".

If the user answers yes, then the result "For all a in S, there exists
bℜa such that <principle>" means "For all a in S, there exists b
of the kind bℜa such that <principle>".

In this case, the results means that for all a in S, an argument x
satisfying aℜx must exist such that <principle> (parameterized by
a, x) holds.

If the user answers no, then after the user chooses an alternative
variable -say c- instead of a, the result will be "For all a in S, there
exists bℜc such that <principle>".

Here, the result means that for all a in S, two arguments x and y
satisfying xℜy must exist such that <principle> (parameterized by
a, x, y) holds.