Are there formal systems that allow you to make human-like higher-order statements?

For humans, it's very natural to make higher-order statements. For example, you could state the following (with pseudo-Prolog syntax):

Socrates is smart:

smart(socrates).

John is a man:

man(john).

Socrates believes all men are mortal:

believes(socrates, (mortal(X) :- man(X))).

If someone is smart and believes something, it must be true:

Y :- smart(X), believes(X, Y).

I checked out a couple of "higher-order" extensions to Prolog, but neither can accept the kinds of statements like the last two examples.

Are there formal systems that allow you to make human-like higher-order statements, such as these?

Solution