FOL, First-order logic
Predicate Calculus
Functional logic / quantification logic, formalized as predicate calculus, is a development of Frege's early predicate logic. Propositional Logic is a simpler logical system, while predicate logic is more sophisticated, allowing us to express objects, their properties, and relations between objects. It is a logic that uses quantifier symbols for objects that can be subjects in the subject-predicate structure that exists in propositions. Therefore, unlike propositional logic, it can handle inference rules based on the analysis of the internal structure of propositions, whereas in propositional logic, the proposition is the minimum unit, so analysis of the internal structure of propositions cannot be performed. Predicate logic was independently invented by Gottlob Frege in Europe and Charles Sanders Peirce in America.
Predicate logic Notion
Predicate Logic Theorems
First-order logic
First-order logic—also known as predicate logic, quantificational logic, and first-order predicate calculus—is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quantified variables over non-logical objects, and allows the use of sentences that contain variables, so that rather than propositions such as "Socrates is a man", one can have expressions in the form "there exists x such that x is Socrates and x is a man", where "there exists" is a quantifier, while x is a variable.[1] This distinguishes it from propositional logic, which does not use quantifiers or relations;[2] in this sense, propositional logic is the foundation of first-order logic.
https://en.wikipedia.org/wiki/First-order_logic

Seonglae Cho