A thing occurred to me while i was reviewing the idea of enumerative induction becus i mentioned it to a friend of mine. The thing is that such inductions are often presented in the a way like this:

A particular thing of the type F is also of the type G
Here is another one
And another
…
Thus, all things of type F are also of type G

Suppose we formalize it in a simple lazy way:

(∃!x₁)(F x₁∧G x₁)
(∃!x₂)(F x₂∧G x₂)
…
(∃!x_n)(F x_n∧G x_n)
⊢ (∀x)(Fx→Gx)

But wait, one might as well draw the conclusion:

 ⊢ (∀x)(Gx→Fx)

Surely that follows just as well. However, if we keep this in mind when reviewing the typical example, then we get a result that differs from normal:

This swan is white.
So is this one.
And this one.
…
So, all swans are white.

But following the above, we might as well just draw this conclusion:

So, all white things are swans.

I see no way to block that inference while letting the other thru, for the simple reason that F and G above are arbitrary. In second-order predicate logic, it looks something like this (with greek capital letters for predicate variables):

(∃Ψ)(∃Ω)(∃!x₁)(Ψx₁∧Ωx₁)
(∃Ψ)(∃Ω)(∃!x₂)(Ψx₂∧Ωx₂)
…
(∃Ψ)(∃Ω)(∃!x_n)(Ψx_n∧Ωx_n)
⊢ (∃Ψ)(∃Ω) (∀x)(Ψx→Ωx)
⊢ (∃Ψ)(∃Ω) (∀x)(Ωx→Ψx)

Altho, the formalizations above are broken in a slight way. They don’t capture the fact that the predicates in each premise have to be the same. So, one wud have to do it something like this:

(∃Ψ)(∃Ω)(∃!x₁)(∃!x₂)…(∃!x_n)(Ψx₁∧Ωx₁)∧(Ψx₂∧Ωx₂)∧…∧(∃!x_n)(Ψx_n∧Ωx_n)