How is "$A$ generalizes $B$" formally defined?

This might look a bit silly but I was trying to find if there is specific symbol/formalization in logic to describe "$A$ generalizes $B$". At first I though simply about using implication, because it seems to just mean that $A \Rightarrow B$. For example

$a^p \equiv a \pmod p \Rightarrow 2^3 \equiv 2 \pmod 3$

In this case it is clear that left side is generalization of the right side. But then consider following implication:

There are infinitely many primes of form $4n+1$ $\Rightarrow$ There are infinitely many primes

Here left side of the implication does not seem to be generalization of the right side. Actually left side looks like more specific case.

Is this just intuition failure and both cases are in fact generalizations? Or is there some formal distinction between "generalizes" and "implies" relations? Also if not, why would we even use two different words for something if the semantics is same?

• I guess we say $A$ generalizes $B$ when we can deduce that $B$ is true, by knowing $A$, without a lot of effort. Mar 26, 2016 at 17:39
• I'd say, just using regular classical material implication cannot really capture that, because we have $A \Rightarrow B$ or $B \Rightarrow A$ for any two propositions $A$ and $B$; the meaning of $A$ can be completely unrelated from the meaning of $B$ and we still have $A \Rightarrow B$. Mar 26, 2016 at 17:44

As you (and Stefan Perko in the comments) noticed, there is no trivial relation between logical implication because of the weakening, and worse, the notion of "normal proof" (cut-free proof) eradicates the direct relation between a statement and its corollary.

So I think you need to see it through type theory. To do so, let's reformulate your two examples in the following way:

From $A \implies B$ you take some $a \in A$, $b \in b$, and get a $a \to b$.

While the second would be:

There is an Red $A$, so there is an $A$.

In other words, your first example consists in taking an instance of a relation between two types, while the second corresponds to the subtyping relation (a cat is an animal). There's a direct relation between proofs and types (the Curry-Howard-Lambek correspondence), so these examples translate well in a corresponding theoretical programming language, the System $F_{<:}$ (F-sub). In practice, proof assistants (Coq) use even more elaborate type systems, but this is sufficient to model your two examples. In this calculus the first example consists of having a term of a certain type, and the second of having a subtype.

Here is a different way to look at generalization. Any result is the form $A \rightarrow B$. However for any such $A$, there is a set of objects $\{ a_i \}$ that satisfy $A$. Generalizing a result means that there exists of proper superset of $\{ a_i \}$, $A^S$, being a member of $A^S$ implies a common property $A'$, and $A' \rightarrow B$.