"

The rules of the system

Each rule in our tableau system codifies some simple facts about our semantics. This is a general feature of deductive systems in logic. What is less so is the fact that tableau systems are not linear, but take a tree form. In fact, our tableau deductions will look something like the syntax trees we covered before. However, despite the similarities, do not confuse the two. They are entirely different systems with a different purpose. Tableau tree deductions are used to show whether

XX

is a tautologous formula, syntax tree derivations are used to show whether

XX

is a formula at all.

Just as syntax trees, tableau trees are also binary. This means that at any one point, the tree may branch to at most two separate points. But sometimes, there is no branching, and only one additional point is connected. Because of this, we may classify our rules as those which branch, and those which do not.

The basic idea behind the rules is that given a complex formula

XX

of the language assumed to be true, we can infer what other, less complex formulas must also be true as a consequence. For this, we need to know what formulas we may encounter in our language, and what we can do with them.

First, we have the basic case, where everything is either an atomic formula

PP

, a conjunction

YZY \wedge Z

, a disjunction

YZY \vee Z

, a conditional

YZY \rightarrow Z

, or a negation

¬Y\neg Y

. Now as it turns out, it is a good idea to take the negation of each of these formulas separately. So we have the negation of an atomic formula

¬P\neg P

, the negation of a conjunction

¬(YZ)\neg (Y \wedge Z)

, the negation of a disjunction

¬(YZ)\neg(Y \vee Z)

, the negation of a conditional

¬(YZ)\neg (Y \rightarrow Z)

, or the negation of a negation

¬¬Y\neg \neg Y

. This covers every possible negated formula form, and the two sets cover every possible formula form. Here is a diagram of this:

image

Remark 5.3. It might seem like there is a problem here, since

¬Y\neg Ydoes not appear in the diagram, only

¬¬Y\neg \neg Y. But this is not the case, since if we consider

¬Y\neg Y, and what

YYcould be, it could either be a negated formula or a non-negated one. If it is negated, then it is a double negation, which is covered by

¬¬Y\neg \neg Y. If it is a simple negation, then

YYis either a complex or an atomic formula, which is also covered by the diagram. So there is nothing missing.

Now, as far as our rules are concerned, we will not have rules for

PP

and

¬P\neg P

, but we will have rules for every other form. The principles behind these rules will be familiar if you have ever taken a logic course before.

Non-branching rules

First, we will consider non-branching rules, since they are simpler. And we shall start with the simplest of them all.

Double negation

The double negation rule is extremely simple. If you have a formula of form

¬¬X\neg \neg X

occurring on a branch of the tree, you can extend that branch with

XX

. In practice, this simply looks like this:

A logical proof with two numbered lines. Line 1 shows "¬¬X" with X double negated, and line 2 shows "X", deriving X from double negation elimination on line 1.
Double negation rule

Why does this rule work? Simply because of the way structures are defined. In particular, if you have a structure

𝐒\mathbf{S}

, and

𝐒¬¬X\mathbf{S} \models \neg \neg X

, then by definition of

¬\neg

,

𝐒⊭¬X\mathbf{S} \not\models \neg X

, and so by the same definition,

𝐒X\mathbf{S} \models X

. This works the other way around too, but we are always moving from more complex to simpler formulas in tableau systems, so we do not need to consider the reverse.

Here is a representation of the above in a truth table:

XX ¬X\neg X ¬¬X\neg \neg X
𝐓\mathbf{T} FF 𝐓\mathbf{T}
FF TT FF

Conjunction

The conjunction rule is another one of these really simple rules. It says that if you have a formula of form

XYX \wedge Y

on a branch, then you can extend that branch with either

XX

or

YY

, i.e., with either the left or the right side. Like this:

Mathematical text showing logical expressions: "1. X 'conjunction symbol' Y", and "2. X 'conjunction symbol' 1"
Mathematical text showing logical expressions: "1. X 'conjunction symbol' Y", and "2. Y 'conjunction symbol' 1"
Conjunction rule

Clearly, by two successive applications of the rule on

XYX \wedge Y

, you can also get the following:

Logical sequence with three numbered lines showing logical expressions. Line 1: X and Y. Line 2: X deduces and 1. Line 3: Y deduces and 1.

Now why does this rule work? Again, it is a simple matter of checking that whenever

𝐒XY\mathbf{S} \models X \wedge Y

,

𝐒X\mathbf{S} \models X

, and

𝐒Y\mathbf{S} \models Y

. In fact, this is literally just the definition of how

\wedge

behaves in any structure, so we don’t have to show anything. Of course, we can represent this in a truth table, the exact one that was given above for

\wedge

:

XX YY XYX \wedge Y
𝐓\mathbf{T} 𝐓\mathbf{T} 𝐓\mathbf{T}
TT FF FF
FF TT FF
FF FF FF

Negated disjunction

The next type of non-branching rule that we cover is a bit more elaborate than the previous ones. It is of the following form, similar to the simple

\wedge

rule above.

Two numbered logical expressions. 1: ¬(X 'conjunction symbol' Y). 2: ¬X, derived from ¬'conjunction symbol' 1.
Two numbered logical expressions. 1: ¬(X 'conjunction symbol'  Y). 2: ¬Y, derived from ¬'conjunction symbol' 1
Negated disjunction rule

Now why does this work? The above is an instance of what may be called DeMorgan’s laws. The relevant instance is the following (usually formulated in the second part as a single conjunction

¬X¬Y\neg X \wedge \neg Y

):

Proposition 5.6. If

𝐒¬(XY)\mathbf{S} \models \neg (X \vee Y), then

𝐒¬X\mathbf{S} \models \neg Xand

𝐒¬Y\mathbf{S} \models \neg Y.

Proof. Suppose

𝐒¬(XY)\mathbf{S} \models \neg (X \vee Y). Then,

𝐒⊭XY\mathbf{S} \not\models X \vee Y. Now

𝐒XY\mathbf{S} \models X \vee Yiff either

𝐒X\mathbf{S} \models X,

𝐒Y\mathbf{S} \models Y, or both. Thus if

𝐒⊭XY\mathbf{S} \not\models X \vee Y, that means none of these cases hold. So that leaves us with

𝐒⊭X\mathbf{S} \not\models Xand

𝐒⊭Y\mathbf{S} \not\models Y. Thus,

𝐒¬X\mathbf{S} \models \neg Xand

𝐒¬Y\mathbf{S} \models \neg Y. ◻

As you can see, our rule just codifies the above instance of DeMorgan’s law. And once again, with two successive application of the rule, you can get the negation of either formula

XX

or formula

YY

, if needed. Compare the following table:

XX YY ¬X\neg X ¬Y\neg Y XYX \wedge Y ¬(XY)\neg (X \wedge Y)
TT TT FF FF TT FF
TT FF FF TT FF FF
FF TT TT FF FF FF
FF FF 𝐓\mathbf{T} 𝐓\mathbf{T} FF 𝐓\mathbf{T}

We can stop now for a second and look at our initial question, that of proving that

X¬XX \vee \neg X

is a tautology. As mentioned, in order to do this, we need to put its negation at the top of our tree. Then, we have to apply our rules until we get to an explicit contradiction of form

Y¬YY \wedge \neg Y

(for some

YY

). Thus:

Logical proof table showing a sequence of steps, including negations and disjunctions, deriving "X" from "¬(X ∨ ¬X)" using rules like negation and disjunction elimination.

The above is a complete proof of

X¬XX \vee \neg X

being a tautology. You might be asking what the symbol

\otimes

stands for at the end. It represents that the branch (the only one of the tree) is ‘closed’, because both a formula and its negation occurs on it. Where? Well, that is given by the numbers below

\otimes

, namely line 2 and 4. Line 2 has the formula

¬X\neg X

, while line 4 has the formula

XX

on it, so we have both

XX

and

¬X\neg X

. Thus, we have our desired explicit contradiction derived from the negation of the tautology candidate. This means that

X¬XX \vee \neg X

is a tautology according to our system. Nice!


Let’s get back to our other rules before we go further into examples.

Negated conditional

The negated conditional is another one of those non-branching rules that are not immediately obvious. It is specified as follows:

Logical expression showing two numbered statements: 1) not (X implies Y), 2) X implies not statement 1.Logical expression showing two numbered statements: 1) not (X implies Y), 2) not Y implies not statement 1.
Negated conditional rule

Why does this work? Again, it just codifies a fact, the following fact, from our semantics:

Proposition 5.7. If

𝐒¬(XY)\mathbf{S} \models \neg (X \rightarrow Y), then

𝐒X\mathbf{S} \models Xand

𝐒¬Y\mathbf{S} \models \neg Y.

Proof. Suppose

𝐒¬(XY)\mathbf{S} \models \neg (X \rightarrow Y). Then,

𝐒⊭XY\mathbf{S} \not\models X \rightarrow Y. But

𝐒XY\mathbf{S} \models X \rightarrow Yiff whenever

𝐒X\mathbf{S} \models X,

𝐒Y\mathbf{S} \models Y. So again, by negating both sides of the biconditional,

𝐒⊭XY\mathbf{S} \not\models X \rightarrow Yiff it is not the case that if

𝐒X\mathbf{S} \models X, then

𝐒Y\mathbf{S} \models Y. So

𝐒⊭XY\mathbf{S} \not\models X \rightarrow Yiff

𝐒X\mathbf{S} \models Xbut

𝐒⊭Y\mathbf{S} \not\models Y. Or in other words, iff

𝐒X\mathbf{S} \models Xand

𝐒¬Y\mathbf{S} \models \neg Y. Which is what we wanted to show. ◻

Here is the truth-table fragment to compare:

XX YY ¬Y\neg Y XYX \rightarrow Y ¬(XY)\neg (X \rightarrow Y)
TT TT FF TT FF
𝐓\mathbf{T} FF 𝐓\mathbf{T} FF 𝐓\mathbf{T}
FF TT FF TT FF
FF FF TT TT FF

This concludes our non-branching rules. Now we turn to our branching ones.

Branching rules

As mentioned above, our tree only ever branches to two separate branches from any one point. Thus, our branching rules are all of the form:

X branches to Y and to Z.

Why do we need branching rules? Note that in all of the above examples, the assumption that a certain complex formula is true determined exactly the truth values of some simpler formulas. In the truth table illustrations, this just means that for each complex formula, they were only true in one, and only one, row (the one in gray), so we just had to check what truth values the simpler formulas received in that row (put in bold). However, many formulas are true in several rows in a truth-table. In that case, we need to consider the possibilities that afford the complex formula to be true separately. And this gets compounded if we go further and encounter another such formula, and another one, and so on.

Disjunction

The disjunction rule is the simplest rule of the branching ones. In many ways, it is like the conjunction rule. It looks like this:

Logical equation illustrating a truth value sequence, featuring two lines. First line: "X or Y." branches to the second line: X, Y, or 1.
Disjunction rule

Here is the reasoning behind this rule. As we know,

𝐒XY\mathbf{S} \models X \vee Y

iff

𝐒X\mathbf{S} \models X

or

𝐒Y\mathbf{S} \models Y

(or both). The problem is that just the fact that

𝐒XY\mathbf{S} \models X \vee Y

does not tell us whether

𝐒X\mathbf{S} \models X

or

𝐒Y\mathbf{S} \models Y

or both. It only tells us that it is at least one of these. Given this lack of information, we need to consider the consequences separately. Interestingly, we need not consider the case where both

XX

and

YY

is true separately. But we also don’t make any explicit assumptions about what the truth-value of the other formula is on either branch. So all we do is consider the case where

XX

is true, whatever truth value

YY

may have (

TT

or

FF

), and consider the case where

YY

is true, whatever truth value

XX

may have (

TT

or

FF

). Here is the table representation:

XX YY XYX \vee Y
𝐓\mathbf{T} 𝐓\mathbf{T} 𝐓\mathbf{T}
𝐓\mathbf{T} FF 𝐓\mathbf{T}
FF 𝐓\mathbf{T} 𝐓\mathbf{T}
FF FF FF

As described above, when we branch to

XX

, we are considering either line 1 or line 2 of the truth table. When we branch to

YY

, we are considering either line 1 or line 3 of the truth table.

Negated conjunction

Negated conjunction is also an instance of DeMorgan’s laws. It is as follows:

Flowchart showing a logical deduction. Line 1: ¬(X ∧ Y); Line 2: ¬X, ¬Y, derived from ¬∧ 1, indicating negation of a conjunction.
Negated conjunction rule

Again, we can show the following:

Proposition 5.8. If

𝐒¬(XY)\mathbf{S} \models \neg (X \wedge Y), then

𝐒¬X\mathbf{S} \models \neg Xor

𝐒¬Y\mathbf{S} \models \neg Y(or both).

Proof. Suppose

𝐒¬(XY)\mathbf{S} \models \neg (X \wedge Y). Then,

𝐒⊭XY\mathbf{S} \not\models X \wedge Y. But

𝐒XY\mathbf{S} \models X \wedge Yiff

𝐒X\mathbf{S} \models Xand

𝐒Y\mathbf{S} \models Y, so

𝐒⊭XY\mathbf{S} \not\models X \wedge Yiff either

𝐒⊭X\mathbf{S} \not\models Xor

𝐒⊭Y\mathbf{S} \not\models Y, or both. So

𝐒¬X\mathbf{S} \models \neg X, or

𝐒¬Y\mathbf{S} \models \neg Y, or both. ◻

Again, on either branch, we do not make assumptions about the truth value of the formula on the other branch. Thus, on the left branch, we assume

¬X\neg X

is true, but nothing about

¬Y\neg Y

being true or false, and conversely for the right branch. In table representation:

XX YY ¬X\neg X ¬Y\neg Y XYX \wedge Y ¬(XY)\neg (X \wedge Y)
TT TT FF FF TT FF
TT FF FF 𝐓\mathbf{T} FF 𝐓\mathbf{T}
FF TT 𝐓\mathbf{T} FF FF 𝐓\mathbf{T}
FF FF 𝐓\mathbf{T} 𝐓\mathbf{T} FF 𝐓\mathbf{T}

Conditional

The rule for conditionals is our last rule for the system. It also has a form that may make you stop and think why it is formulated as such.

Logical proof diagram with two premises. Premise 1: if X, then Y. Premise 2 branches to not X and to Y from line 1 followed by,  "conditional symbol" 1.
Conditional rule

The reasoning behind it is as follows:

Proposition 5.9. If

𝐒XY\mathbf{S} \models X \rightarrow Y, then

𝐒¬X\mathbf{S} \models \neg Xor

𝐒Y\mathbf{S} \models Y(or both).

Proof. The proof follows the usual lines. Suppose

𝐒XY\mathbf{S} \models X \rightarrow Y. Then, whenever

𝐒X\mathbf{S} \models X,

𝐒Y\mathbf{S} \models Y. We have already seen that this is false when

𝐒X\mathbf{S} \models Xbut

𝐒⊭Y\mathbf{S} \not\models Y. This leaves 3 other options left for it to be true.

  1. First, if

    𝐒X\mathbf{S} \models Xand

    𝐒Y\mathbf{S}\models Y, clearly,

    𝐒XY\mathbf{S} \models X \rightarrow Y. Note that

    𝐒X\mathbf{S} \models Xonly if

    𝐒⊭¬X\mathbf{S} \not\models \neg X, but

    𝐒Y\mathbf{S} \models Y.

  2. Second, if

    𝐒⊭X\mathbf{S} \not\models Xbut

    𝐒Y\mathbf{S} \models Y, then

    𝐒XY\mathbf{S}\models X \rightarrow Yagain. This is the case where both

    𝐒¬X\mathbf{S} \models \neg X(because

    𝐒⊭X\mathbf{S} \not\models X) and

    𝐒Y\mathbf{S} \models Y.

  3. Third, if

    𝐒⊭X\mathbf{S} \not\models Xand

    𝐒⊭Y\mathbf{S} \not\models Y, then still,

    𝐒XY\mathbf{S} \models X \rightarrow Y. Again, this means that

    𝐒¬X\mathbf{S} \models \neg X, but

    𝐒⊭Y\mathbf{S} \not\models Yin this case.

As you can see, in all three cases where

𝐒XY\mathbf{S} \models X \rightarrow Y, it is true that either

𝐒¬X\mathbf{S} \models \neg Xor

𝐒Y\mathbf{S} \models Yor both. Indeed, those are exactly the three options we have for

XYX \rightarrow Yto be true in

𝐒\mathbf{S}. ◻

Or in truth table form:

XX YY ¬X\neg X XYX \rightarrow Y
TT 𝐓\mathbf{T} 𝐅\mathbf{F} 𝐓\mathbf{T}
TT FF FF FF
FF 𝐓\mathbf{T} 𝐓\mathbf{T} 𝐓\mathbf{T}
FF 𝐅\mathbf{F} 𝐓\mathbf{T} 𝐓\mathbf{T}

As usual, the rule form only explicitly represents the possibility where

¬X\neg X

is true, and the possibility where

YY

is true, leaving open whether

YY

is true or false on the left branch (and similarly for

¬X\neg X

on the right one).

The strategy

Here is the strategy again, now with all our rules in hand. Suppose you have a formula

XX

that is a candidate for being a tautology. In order for us to show this in our system, we first have to take

¬X\neg X

, and put that at the root of our tree. Then, we have to apply our rules until we have an explicit contradiction of form

YY

and

¬Y\neg Y

on each branch of the tree.

Suppose we want to show something quite elaborate, like the following:

(XY)(¬XY)(X \rightarrow Y) \rightarrow (\neg X \vee Y)

Remark 5.4. You may note the similarity between this formula schema and the rule for conditionals. Of course, this is no accident. In fact, every one of our rules can be turned into a tautology in our system, with the use of

\rightarrow.

Since the formula is

(XY)(¬XY)(X \rightarrow Y) \rightarrow (\neg X \vee Y)

, again, we put its negation at the root, thus:

A logical expression in symbolic notation: ¬((X → Y) → (¬X ∨ Y)) with 'Start' to its right, indicating the beginning of a logical proof.

The next step is to apply one of the rules. For this, you need to identify whether the formula is negated or not, and what the main connective of the formula is, or in the negated case, what the main connective after the negation sign is. Here, the answer is: it is a negated conditional. Obviously, you then apply the negated conditional rule. In fact, we don’t quite see where we are going yet, so we can apply it twice to get both possibilities. Thus:

Diagram of a logical proof with three steps. Step 1: ¬((X → Y) → (¬X ∨ Y)) labeled "Start." Steps 2 and 3 derive X → Y and ¬(¬X ∨ Y).

Now that we have two formulas, we have a choice how we want to proceed. On the other hand, unlike with other systems, we do not have a choice about which rules to apply. Each formula admits of one, and only one, rule, depending on its form.

In general, it is usually better to apply first all the rules that do not branch, and then apply any branching rules. If you think about it, this makes sense, since each branching rule doubles the work we have to carry out. At any rate, the non-branching rule is the one for

¬\neg \vee

, so we can start with that, and apply it twice:

Logic proof showing steps from 1 to 5. Step 1: negated implication. Step 2: implication. Steps end in the negation of Y. Labeled as "Start" and numbered.

So far, we only have a single branch, and that branch is open. On the other hand, we still have formulas on which to apply rules. So we are certainly not done. One trivial step is to get rid of the double negation in line 4. This will not help us much, but it will simplify things a bit. Thus:

Logical proof steps numbered 1 to 6 with rules applied on the right. The proof involves negations and implications, concluding with 'X' as the result.

Now most of the formulas in the proof are ‘exhausted’. There is no rule for

¬Y\neg Y

or

XX

to apply, and for all the other formulas (except one), we have applied the appropriate rules as many times as possible. So we are left with

XYX \rightarrow Y

. This is a branching rule, so now we branch.

A logical proof diagram showing statements and deductions labeled 1 to 7, using symbols like ¬, ∨, and →. Steps are aligned with corresponding justifications on the right.

Our tree is now complete, there are no more rules to apply. Now comes the crucial part. You have to see if each of the branches are closed. Again, this means that you have a formula of form

ZZ

and a formula of form

¬Z\neg Z

on each branch. Note that each branch is the sequence of formulas from the root to one of the leaves. Thus, the first branch here is from

¬((XY)(¬XY))\neg((X \rightarrow Y) \rightarrow (\neg X \vee Y))

to

¬X\neg X

, the second branch is from

¬((XY)(¬XY))\neg((X \rightarrow Y) \rightarrow (\neg X \vee Y))

to

YY

, through all the other formulas.

Let’s take the first branch. Can you see a contradiction? I can, since line 6 has

XX

on it, and line 7 (left) has

¬X\neg X

on it. So the first branch is closed. Thus:

A logical proof tree illustrating steps to derive a contradiction. The proof shows false premises leading to a contradiction symbol, ⊗.

What about the second branch? Again, there is a contradiction, since line 5 has

¬Y\neg Y

, while line 7 (right) has

YY

. Thus:

A logical proof diagram showing numbered steps. Each step consists of a logical expression, with arrows and lines indicating logical deductions.

This completes the proof. Once you have a complete proof of a formula in the system, you can say that that formula is a theorem of zeroth-order logic. Thus,

(XY)(¬XY)(X \rightarrow Y) \rightarrow (\neg X \vee Y)

is a theorem of zeroth order logic. We represent this as follows:

(XY)(¬XY)\vdash(X \rightarrow Y) \rightarrow (\neg X \vee Y)

The symbol

\vdash

means something like ‘syntactically provable’. It is the syntactic equivalent to being a tautology in the semantics. In fact, being a tautology (in the semantics) can be represented as follows:

(XY)(¬XY)\models(X \rightarrow Y) \rightarrow (\neg X \vee Y)

This makes sense, as it is just like writing

𝐒(XY)(¬XY)\mathbf{S} \models (X \rightarrow Y) \rightarrow (\neg X \vee Y)

, except we omit a specific structure designation

𝐒\mathbf{S}

, since it is modeled by all structures, not just a specific one.

Definition 5.2 (Theorem). Let

XX,

YYbe any formulas. We call a branch of a tree closed provided there are some formulas of form

YY,

¬Y\neg Yoccurring on it. We call a tree closed if all its branches are closed. Then,

XXis a theorem of zeroth-order logic provided there is a closed tree with

¬X\neg Xat its root. In such cases, we also write

X\vdash X, and call the closed tree for

¬X\neg Xthe tableau (tree) proof of

XX.


Here is another proof to inspect, with more branching, before it is your turn:

Abstract logical proof tree diagram, lines numbered 1 to 9. Symbols include negations, conjunctions, and disjunctions. Branching and contradictions shown.

Note that we could have made this derivation even longer, but we opted to apply

¬\neg\wedge

to line 3 to extend only the right-side branch of the tree (to line 5). This is because it would not have made any difference on the left-hand side, given that it closed by

¬(Y¬Y)\neg (Y \vee \neg Y)

alone (line 4, then 8 and 9). In any derivation, you are looking to close every branch and nothing more. Thus, you can make derivations significantly shorter if you cut out the steps that are not necessary to close a branch.

Here is an intuitive explanation of why

((Y¬Y)X)(X(Y¬Y))((Y \vee \neg Y)\rightarrow X) \rightarrow (X \wedge (Y \vee \neg Y))

is a tautology. If you look at the first half of the formula, it says that

(Y¬Y)X(Y \vee \neg Y) \rightarrow X

. I.e., if

Y¬YY \vee \neg Y

, then

XX

. But since

Y¬YY \vee \neg Y

is known to be a tautology that holds in all structures, if it entails

XX

, then

XX

would also be a tautology (since again,

Y¬YY \vee \neg Y

holds in every structure, and so if in every structure, it entails

XX

,

XX

holds in every structure). But if that is the case, then both

Y¬YY \vee \neg Y

and

XX

must hold (both being tautologies).

Exercise 5.3. Prove that the following formulas are all theorems of the tableau system:

  1. Y(XY)Y \rightarrow (X \rightarrow Y)

    ;

  2. (¬X¬Y)¬(XY)(\neg X \wedge \neg Y) \rightarrow \neg(X \vee Y)

    ;

  3. (¬X¬Y)¬(XY)(\neg X \vee \neg Y) \rightarrow \neg(X \wedge Y)

    ;

  4. ¬(XY)(¬X¬Y)\neg (X \wedge Y) \rightarrow (\neg X \vee \neg Y)

    ;

  5. ¬(XY)(¬X¬Y)\neg (X \vee Y) \rightarrow (\neg X \wedge \neg Y)

    ;

  6. (¬XY)(XY)(\neg X \vee Y) \rightarrow (X \rightarrow Y)

    ;

  7. (XY)(¬Y¬X)(X \rightarrow Y) \rightarrow (\neg Y \rightarrow \neg X)

    ;

  8. ((XY)((XZ)(YZ)))Z((X \vee Y) \wedge ((X \rightarrow Z) \wedge (Y \rightarrow Z))) \rightarrow Z

    .

License

Icon for the Creative Commons Attribution-NonCommercial-ShareAlike 4.0 International License

Learning Logic Backwards Copyright © by Peter Susanszky is licensed under a Creative Commons Attribution-NonCommercial-ShareAlike 4.0 International License, except where otherwise noted.