What is a formal definition of "predicate logic"?

Question

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?

Answer 1

I'm afraid the definition you suggested has some shortcomings. To begin with your definition essentially makes use of the notion of a formal system, a notion that has not been formally defined. Furthermore, classical first-order logic satisfies a certain isomorphism condition: First-order sentences cannot be distinguished in isomorphic models. But your definition does not seem to capture this fact.

For a better start, let a logic, $\mathcal{L}$, consist of a function $L$ and a 2-place relation $\models_{\mathcal{L}}$. $L$ assigns a set $L(\sigma)$ (the set of $\sigma$-sentences of $\mathcal{L}$) to each signature $\sigma$ (set of non-logical constants) such that the following holds:

1. If $\sigma_0 \subseteq \sigma_1$, $L(\sigma_0) \subseteq L(\sigma_1)$.

2. If $\mathfrak{A} \models_{\mathcal{L}} \phi$, then there is some signature $\sigma$ such that $\mathfrak{A}$ is a model interpreting $\sigma$ and $\phi \in L(\sigma)$.

3. (isomorphism condition) If $\mathfrak{A} \models _{\mathcal{L}} \phi$ and $\mathfrak{A}, \mathfrak{B}$ are isomorphic, then $\mathfrak{B} \models_{\mathcal{L}} \phi$.

4. If $\sigma_0 \subseteq \sigma_1, \phi \in L(\sigma_0)$, and $\mathfrak{A}$ is a model interpreting $\sigma_1$, then $\mathfrak{A} \models_{\mathcal{L}} \phi$ iff $\mathfrak{A}|_{\sigma_0} \models_{\mathcal{L}} \phi$ (where $\mathfrak{A}|_{\sigma_0}$ is the $\sigma_0$-model having the same domain as $\mathfrak{A}$ and coinciding with $\mathfrak{A}$ on $\sigma_0$).

Now first-order logic, $\mathcal{L}_{I}$, is the logic whose function $L_I$ assigns to each signature $\sigma$ the set of first-order $\sigma$-sentences and whose 2-place relation $\models_{\mathcal{L}_I}$ is the usual satisfaction relation between first-order models and first-order sentences.

Answer 2

As you can read in the reference to Wiki or into a lot of good mathematical logic textbooks, there are some basic concepts in play :

formal system

language.

Propositional logic is based on a specific language; first-order logic (or predicate logic) is based on a "more wide" (i.e.more expressive) language.

In both cases we need formation rules, to build "correct expression", like terms and formulas.

Then we need transformation rules, usually called inference rules (e.g modus ponens): at least one, ususally more than one, and axioms (zero or more).

With this in place, we have a calculus or proof system: the basic concept of a proof system is that of derivation (from axioms or assumptions) of theorems.

Upo to now we have introduced the syntax; then we add the semantics that allows us to "give meaning" to terns (they have denotation) and formula (that stay for sentences).

In first-order logic (or predicate calculus) a predicate is a symbol; when we interpret it, the "standard" semantics for predicates are subset of the domain of our interpretation.

If we "apply" f-o logic to arithemetic, we may use a predicate like $\le$, and a term like $0$, in order to build a formula like :

$x \le 0$.

This formula is constructed with the binary predicate $\le$ (a binary realtion), and it holds for all numbers that are less or equal than $0$. So, in the domain of the natural numbers, this formula will be true for a number $k$ iff

$k \in \{ n \in \mathbb{N} : n \le 0 \} = \{ 0 \}$.

---

Added

For a "formal" approach, you can see Heinz-Dieter Ebbinghaus & Jörg Flum & Wolfgang Thomas, Mathematical logic (1984), Ch.XII : Characterizing First-Order Logic :

some results, due to Lindstrom, [...] show that first-order logic occupies a unique place among logical systems [...] :

(a) There is no logical system with more expressive power than first-order logic, for which both the compactness theorem and the Löwenheim-Skolem theorem hold.

(b) There is no logical system with more expressive power than first-order logic, for which the Löwenheim-Skolem theorem holds and for which the set of valid sentences is enumerable.

Where :

Definition 1.1. A logical system $\mathscr L$ consists of a function $L$ and a binary relation $\vDash_{\mathscr L}$.

$L$ associates with every symbol set $S$ a set $L(S)$, the set of $S$-sentences of $\mathscr L$.

The following properties are required:

(a) If $S_0 \subset S_1$, then $L(S_0) \subset L(S_1)$.

(b) If $\mathfrak A \vDash_{\mathscr L} \varphi$ (i.e., if $\mathfrak A$ and $\varphi$ are related under $\vDash_{\mathscr L}$), then, for some $S, \mathfrak A$ is an $S$-structure and $\varphi \in L(S)$.

(c) (Isomorphism property) If $\mathfrak A \vDash_{\mathscr L} \varphi$ and $\mathfrak A \cong \mathfrak B$ then $\mathfrak B \vDash_{\mathscr L} \varphi$.

(d) (Reduct property) If $S_0 \subset S_1, \varphi \in L(S_0)$, and $\mathfrak A$ is an $S_1$-structure then $\mathfrak A \vDash_{\mathscr L} \varphi$ iff $\mathfrak A \upharpoonright S_0 \vDash_{\mathscr L} \varphi$.

[...] in the case of [first-order logic] $\mathscr L_I$ we choose $L_I$ to be the function which assigns to a symbol set $S$ the set $L_I(S) := L_0^S$ of first-order $S$-sentences, and we take $\vDash_{\mathscr L}$ to be the usual satisfaction relation between structures and first-order sentences.