What Are the Inference Rules for the AEG System?

I Don't Like Rules!

Too bad! Rules of inference are relations that unambiguously dictate how statements are manipulated in a logic. They help you reach useful conclusions about some statement's truth.

Adding and Deleting Double Cuts

This rule of inference states that you may introduce two cuts around any other node and also remove two cuts around any node, so long as the exterior cut only has one cut as a child.

Since A and ¬(¬A) evaluate to the same truth values for the same assignment of truth values to A, the two are logically equivalent. Therefore, wherever you see some statement form, you may double negate it and maintain the same truth or falsity when evaluating the form. And, since cuts are the AEG System's symbol for negation...

We can introduce double cuts and delete them!

Iterating and Deiterating Atoms

Iteration states that you may copy one atom and paste it anywhere inside the same AEG, but not outside. Likewise, Deiteration states that you may delete an atom so long as that atom is also in a shallower cut level of the same AEG. If you do not desire an explanation, stop reading here, before it's too late.

This rule is difficult to wrap your head around. Consider the following AEG.

With what we've explained so far, this corresponds to, in propositional calculus, ¬(A ∧ ¬A). This truth table looks like the following.

Now, consider this next AEG. It was the same as the above AEG, but the Iteration inference rule was applied, in Proof Mode, to the outermost A atom.

Let's look at this truth table now (Peirce My Heart team cannot legally be held responsible for any traumatic flashbacks.)

Note that A ∧ A evaluates to the same truth value that A does. Adding or removing A ∧ A does not affect the truth of the statement, because A still became a conjunct with its negation, which, since all statement forms are conjuncts here, and one of them evaluates to False, the entire statement must evaluate to False.

Now, consider this next AEG. We have two different atoms here.

And its truth table. Note that an empty cut surrounding The Sheet, which is by itself always True, means that we are negating truth, which is always False.

Consider this valid use of Iteration in Proof Mode on the above AEG, now.

And its truth table.

We reached a step where a statement letter and its negation are conjuncts again, as we did in the previous AEG.

Consider this following AEG, now.

And its truth table.

Let us now look at another valid use of Iteration. Again, we have used the Iteration inference rule in Proof Mode to produce this graph.

And its truth table.

Note that, similar to the previous AEG with only A for atoms, we have also come to the same situation where we have some statement and its negation as conjuncts.

If you have no intention of digesting a couple textbooks, trust that the patterns holds here. Adding or removing this negated conjunct does not affect the evaluation of the AEG as a whole, so we may add and remove them as we please, as a valid inference rule. (this probably needs work)