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.

Inserting and Deleting Double Cuts

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

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.

A | ¬A | A ∧ ¬A | ¬(A ∧ ¬A) T | F | F | T F | T | F | T

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.)

A | ¬A | A ∧ A | A ∧ ¬A | A ∧ A ∧ ¬A | ¬(A ∧ A ∧ ¬A) T | F | T | F | F | T F | T | F | F | F | T

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.

Iteration also allows you to iterate an atom at a deeper cut level, however. Consider this following AEG, now.

And its truth table.

A | ¬A | B | A ∧ B | A ∧ B ∧ ¬A | ¬(A ∧ B ∧ ¬A) T | F | T | T | F | T F | T | F | F | F | T T | F | F | F | F | T F | T | T | F | F | T

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.

A | ¬A | B | A ∧ B | ¬(A ∧ B) | A ∧ B ∧ ¬(A ∧ B) | ¬(A ∧ B ∧ ¬(A ∧ B)) T | F | T | T | F | F | T F | T | F | F | T | F | T T | F | F | F | T | F | T F | T | T | F | T | F | T

If you have no intention of digesting a couple textbooks, trust that the patterns holds here.