The final generalization missing from this paper are logical proofs. Existing trial-and-error methods, like Bowman's Bingo, only focus on half of a logical proof, severely limiting the logic. Meanwhile, other existing methods, such as 3D Medusa and forcing chains, use the full proof, but limit the available logic to use during the proof.

At its core, logical proofs are based on the logic that the statement (A or not A) is always true (which will be the case, unless the puzzle has no solution, in which case it is invalid and not part of this discussion). When solving a Sudoku puzzle, we take a piece of paper and draw one line down the middle and one across the top to create a header row. In this header, on the left side, we make a statement like "cell A1 is a 3". On the right side, we make the inverse statement "cell A1 cannot be 3". The makes the left statement "A" and the right statement "not A". We then continue down each side adding statements based on the logic "if A then B." For instance, if cell A1 is 3, then cell A7 cannot be 3, allowing us the add "A7 cannot be 3" to the left side of our proof. Note that the Single-S, Two-S, and Multi-S Strategies mentioned in the paper can all be used within proofs to add statements to either side. Additionally, further logic proofs can be used on either side to create more statements on that side.

When both the right and left side of the proof share a statement "B", such as "cell D5 cannot be 7", then this statement is true for the puzzle being solved by the proof (or, in a case where the proof is used on the right or left side of another proof, this statement can be added to that side of the underlying proof). This is proven by the logic "if (A or not A) then B"; since "A or not A" is logically true, B logically must also be true.

Another possibility is for the right or left side of the proof to result in nil, meaning that it requires more than one number to exist within the same cell at the same time or does not allow any number to exist within some cell. In this case, the proof indicates that the initial statement on that side was false, meaning the inverse statement, along with its inferred statements, must be true.

There is no need for a wing generalization. While Kevin's generalization is pretty great and all, Subset Exclusion was designed to generalize wings.

Andrew, I have scrolled through paper and I'm impressed by its generalization of "XYZ-wing, WXYZ-wing, and other rare cases." It turns out that the "other rare cases" are not so rare -- I can use this technique to solve every of your examples of Aligned Pair Exclusion, a technique that supposedly requires a totally different logic! I feel that the potential for the idea is very vast.

The idea, in non-mathematical terms, is as follows:

Consider a "bent subset" that spread over a box and a row/column. Let A be the part of the subset inside the intersection, B and C the parts outside the intersection.

A A . | . B . | . . .
. C . | . . . | . . .
. . . | . . . | . . .

Then
(1) If B and C have no value in common, then
a) every value in B can be eliminated from every cell seeing that value in the subset.
b) every value in C can be eliminated from every cell seeing that value in the subset.
(2) If B and C have exactly 1 value in common, then that value can be eliminated from every cell seeing that value in the subset.

The proof of this is that if said value is ON, the "bent subset" will be reduced to a set containing fewer values than cells, and with B and C having no value in common. Because B and C has no value in common, it can be "bent" back into an equivalent normal subset which has fewer values than cells, which is a contradiction.

This is definitely a natural progression from Y-wing, XYZ-wing (3 cells) and WXYZ-wing (4 cells) to arbitrary number of cells. To see its potential, see how it solves all examples in the APE page (Example 1 and 4 are just Y-wing and XYZ-wing):

Example 2:
A1, B3, C2, C9 form a bent subset {1,3,7,8}
{A1, B3} and {C9} have only 3 in common.
Therefore every cell that sees every 3 in subset, C3 cannot contain 3.

Example 3:
A1, A3, C1, C3, H3 form a bent subset {1,4,5,7,9}
{A1,C1} and {H3} have only 7 in common.
Therefore every cell that sees every 7 in subset, B3 cannot contain 7.

Example 5:
B8, B9, C1, C3, C7 form a bent subset {1,4,5,7,9}
{B8, B9} and {C1, C3} have only 1 in common.
Therefore every cell that sees every 1 in subset, B1 cannot contain 7 (and also B2 and C9! If you use APE, you have to use it three times).

Example 6:
A3, B1, D3, E3, F3 form a bent subset {1,3,4,6,7}
{B1} and {D3, E3, F3} have only 6 in common.
Therefore every cell that sees every 6 in subset, D1 cannot contain 6.

Eight-cell Example:
I like the idea of using 8 cells simultaneously. But, with bent subset, we need to use only five cells:
B5, C5, D5, D6, E6 form a bent subset {1,2,6,7,9} (This is like WXYZ-wing in the narrow definition but with five cells)
{B5, C5} and {D6, E6} have only 2 in common.
Therefore, every cell that sees every 2 in subset, E5 cannot contain 2.

I believe this is the generalization of all Wing theories we are looking for!