I'm currently trying to get clear about some terms that are often used in computer science (I'm a computer science student), but were never formally introduced. Especially, I would like to know what a "predicate logic" is. Or is it "the predicate logic"?
Defintions
I think the following definitions are correct, by I'm not sure about it. This is what I came up with when I tried to answer my question:
What is a formal definition of "predicate logic"?
As I've wrote this question, I came across many other terms that I could not formally defined, but were used in my definition for "predicate logic". So maybe you can do this shorter. But please keep in mind that I'm not looking for examples, but for a formal definition.
Propositional calculus is a formal system. It contains propositions that can either be false or true. Those propositions can be combined ($\land, \lor, \Rightarrow, \Leftrightarrow, \neg$ and more, but all others can be represented by those logical connectives).
What is the difference between boolean algebra and propostional calculus?
A predicate is a function $p:X \rightarrow \{true, false\}$ where $X$ is any set.
What is the difference between a propsition and a predicate?
A predicate logic is a formal system that uses variables and quantifiers ($\forall$, $\exists$, $\exists!$) to formulate propositions.
Are there axioms for the / a predicate logic?
Best Answer
It is more helpful to view "predicate logic" as a taxonomic term (the same goes for the term "logic" itself). So the question becomes: what properties of a logic cause us to call it a "predicate logic"?
That's a hard question partially because "logic" itself is so broad. We can identify at least a few common properties, but not every predicate logic will have all of them. The basic examples, of course, are the logics that are called "first-order logic" in the literature. But there are also higher-order logics, modal predicate logics, temporal predicate logics, etc.
Here are a few common traits:
Predicate logics may have variables to range over "individual" objects. There many be more than one sort of "individual".
Predicate logics may have variables that range over higher types or predicates, with syntax to match.
Predicate logics often have quantifiers over the individuals and other sorts of objects
Predicate logics often come with semantics in which the predicate symbols in formulas are interpreted as relations on a set of "individuals".