differentiate the terms deductive system, model/structure, formal system, first-order logic

304 Views Asked by At

I can not bring the terms deductive system, model/structure, formal system, first-order logic into order in my head ;-) It seems to me that they are not overly used in a consistent manner and sometimes even have different meanings. Maybe you can help me to sort it out in my brain ;-)

The deductive system (DS) is the syntactical manipulation mechanism, which allows formal deductions (i.e. something like Hilbert calculus). So we can decide something like $A \vdash_{DS} B$.

While a model/structure (M) gives semantic meaning to the formal language, i.e. allows for semantic truth interpretation of sentences. So we can decide something like $A \models_{M} B$.

A formal system then is the triple of a particular deductive system, a particular model and a formal language?

If talking about first-order logic we just mean the formal language together with one deductive system and a model/structure. So actually the characteristics, when talking about first-order logic is the available language, symbols, etc?

1

There are 1 best solutions below

8
On

When people say "first-order logic" they mean a logic that has a certain kind of language (built up from function symbols and relation symbols in the usual way), a certain kind of deductive system, and a certain semantics using structures. There are many variations that are all called "first-order logic", but they all behave in generally the same way.

The key aspects of first-order logic, apart from the specific kind of language, are that it has several key properties:

  • Soundness: If a formula is provable, it is true in every structure (for the same language)

  • Completeness: If a formula is true in every structure for its language, then the formula is provable

  • Compactness: If a formula is a consequence of an infinite set $A$ of formulas, it is a consequence of some finite subset $F$ of $A$.

  • The Löwenheim–Skolem theorem

All the systems that people call "first order logic" will have these properties.