However, not all valid sequents in MPL or PL are truth-functionally valid and can be identified through replacement schemes. Here is an example:

Every F is G. a is F. So, a is G.
∀x(Fx→Gx), Fa ⊧ Ga

It should be intuitive that this is a valid sequent. But if you are not sure, perhaps this informal explanation might help. "∀x(Fx→Gx)" says that every F is a G. You can think of this wff as logically equivalent to an infinite conjunction "( (Fa→Ga) & (Fb→Gb) & (Fc→Gc) & ... )" where "a", "b", "c", etc. are names of all the objects in the domain. This infinite conjunction of course entails "(Fa→Ga)", which together with "Fa", entail "Ga" by modus ponens.

Now consider another example of a sequent in MPL that is valid but not truth-functionally valid :

a is F. a is G. So something is both F and G.

Fa, Ga ⊧ ∃x(Fx&Gx)

Again we can offer an informal explanation as to why this sequent is valid. An existentially quantified wff says that there is at least one object that satisfies some condition. So we can think of "∃x(Fx&Gx)" as logically equivalent to the infinite disjunction "( (Fa&Ga) ∨ (Fb&Gb) ∨ (Fc&Gc) ∨ ... )". The first two premises of the sequent entail "(Fa&Ga)", and this conjunction in turn entails the infinite disjunction. So the sequent is indeed valid. It should be pointed out though that this argument is not very rigorous, and that a more precise justification can and should be given. But we shall not discuss the details here. What is important to remember is that an existentially quantified wff can be thought of as an infinite disjunction, and a universally quantified wff as an infinite conjunction. Bearing these two points in mind should help you understand why the following sequents are all valid sequents of MPL:

Every F is G. Everything is F. So, everything is G.
∀x(Fx→Gx), ∀xFx ⊧ ∀xGx

Every F is G. Everything is not G. So, everything is not F.
∀x(Fx→Gx), ∀x~Gx ⊧ ∀x~Fx

Every F is G. Something is F. So, something is G.
∀x(Fx→Gx), ∃xFx ⊧ ∃xGx

Every F is G. Something is not G. So, something is not F.
∀x(Fx→Gx), ∃x~Gx, ⊧ ∃x~Fx

Everything is F or G. Everything is not F. So, everything is G.
∀x(Fx∨Gx), ∀x~Fx ⊧ ∀xGx

Everything is F or G. Something is not G. So, something is F.
∀x(Fx∨Gx), ∃x~Gx ⊧ ∃xFx

Everything is F and G. So, everything is F.
∀x(Fx&Gx) ⊧ ∀xFx

Something is F and G. So, something is F.
∃x(Fx&Gx) ⊧ ∃xFx

Every F is G. Every G is H. So, every F is H.
∀x(Fx→Gx), ∀x(Gx→Hx) ⊧ ∀x(Fx→Hx)

Every F is G. No G is H. So, no F is H.
∀x(Fx→Gx), ∀x(Gx→~Hx) ⊧ ∀x(Fx→~Hx)

Every F is G. Some F is not H. So, some G is not H.
∀x(Fx→Gx), ∃x(Fx&~Hx) ⊧ ∃x(Gx&~Hx)

Every F is G. Some H is not G. So, some H is not F.
∀x(Fx→Gx), ∃x(Hx&~Gx) ⊧ ∃x(Hx&~Fx)

No F is G. Some F is H. So, some H is not G.
∀x(Fx→~Gx), ∃x(Fx&Hx) ⊧ ∃x(Hx&~Gx)

No F is G. Some G is H. So, some H is not F.
∀x(Fx→~Gx), ∃x(Gx&Hx) ⊧ ∃x(Hx&~Fx)

See if you can explain informally why the above sequents are valid.