Languages of logic and their applications

UNCORRECTED PROOF CAMWA: 3975 + Model pp. 1–10 (col. fig: NIL) ARTICLE IN PRESS Computers and Mathematics with Applications xx (xxxx) xxx–xxx www.elsevier.com/locate/camwa Languages of logic and their applications K. P´ asztor Vargaa,∗, M. V´ arter´ eszb aDepartment of Programming Languages and Compilers, E¨ otv¨ os Lor´ and University, H-1117 Budapest, P´ azm´ any P´ eter s´ et´ any 1/C., Hungary bFaculty of Informatics, University of Debrecen, H-4010 Debrecen, P.O.Box 12., Hungary Received 15 May 2007; accepted 7 June 2007 1 2 Abstract 3 Concerning the logical description languages, in the past 40–50 years many authors have introduced a number of structurally 4 very different first-order languages. Some of these languages follow the structure of a given future model, other ones have been 5 prepared for the description of an arbitrary model. Other variations of the first-order languages do not follow the whole structure of 6 any model: they have been prepared only for the relations definable over the universe in order to be able to prove the generalizations 7 of a number of difficult logical results. 8 The semantics of the first-order languages is based on the interpretation of their extralogical symbols by a suitable model. In 9 some cases, in the interpretation all possible models can be in focus, but there are cases when the models over a special universe 10 are regarded. The naming problem of the universe element of the model arises at this stage. The efforts for solving this problem 11 lead to different approaches. 12 Here, we present the most important language definitions and some characteristic semantics. We investigate the different 13 approaches and conclude that they do not indicate essential differences. In fact, they have been only motivated by seeking for 14 an easier way to achieve the just fixed target. Moreover, we try to point out the suitability connections of languages and semantics 15 definitions. 16 c 2007 Published by Elsevier Ltd 17 Keywords: First-order languages; Syntax; Semantics 18 1. Syntax 19 Leibniz (1640–1710) was the first, who brought up the idea of a complete formal logical reasoning system. He 20 tried to develop a language, and a calculus of reasoning, called them the “lingua characteristica” (universal language) 21 and the “calculus ratiocinator” (calculus of reasoning). Leibniz’s work in this area was basically unknown till its 22 publication in [1], so his ideas were prescient but not influential. Frege developed the base of the modern logical 23 grammar in his book [2] in 1879. He gave the first formal treatment of logic including both quantifiers, relation 24 symbols and propositional connectives. Frege gave, also for the first time, the definition of a proof as a finite sequence 25 of formulae, each of which is either an axiom or follows from previous formulae of the proof by an application of 26 a rule of inference. The appreciation of Frege’s works is also posterior probably because of their hard readability. 27 ∗Corresponding author. E-mail addresses: [email protected] (K. P´ asztor Varga), v[email protected].hu (M. V´ arter´ esz). 0898-1221/$ - see front matter c 2007 Published by Elsevier Ltd doi:10.1016/j.camwa.2007.06.007 Please cite this article in press as: K. P´ asztor Varga, M. V´ arter´ esz, Languages of logic and their applications, Computers and Mathematics with Applications (2007), doi:10.1016/j.camwa.2007.06.007 UNCORRECTED PROOF CAMWA: 3975 ARTICLE IN PRESS 2K. P´ asztor Varga, M. V´ arter´ esz / Computers and Mathematics with Applications xx (xxxx) xxx–xxx In 1889 Peano published a paper [3] similar to Frege’s conception, but his notation system was quite other. In contrast1 with Frege’s papers, this notation system became known fast and widely used. Roughly speaking, Peano’s notation2 extended and modified by Russell and Hilbert is used today. Moreover, forgetting that Frege was the first who applied3 this calculus, it is called Hilbert style in the literature. In the 1920s, L¨ owenheim and Skolem observed that function4 symbols and constant symbols (prospective names for elements of a domain) may be useful for formal treatment of5 logic. In effect, constructions from these items make sets of terms into the first-order logic languages.6 In fact, development and publications of different versions of the first-order logic languages in current use have7 some periods. In the first general works after 1930s [4–6] the system of extralogical symbols of first-order languages8 took shape from the signs of (mathematical and logical) functions. The logical components of logic languages are9 common (connectives, quantifiers and a countable set of (individuum) variables). Now, we give a formal definition of10 what such a language constitutes.11 Definition 1.1. The alphabet of a first-order language consists of12 (i) logical symbols:13 (1) connectives and quantifiers: ¬,∧,∨,⊃,∀,∃,14 (2) variables: x1,x2,x3, . . .,15 (ii) extralogical symbols:16 (1) for each natural number n, named n-ary predicate symbols: Pn 1,Pn 2,Pn 3, . . .,17 (2) for each natural number n, named n-ary function symbols: fn 1,fn 2,fn 3, . . .,18 (3) constant symbols: c1,c2,c3, . . . (the constant symbols may be simply listed as 0-ary function symbols19 f0 1,f0 2,f0 3, . . .),20 (iii) punctuation: ’)’, ’(’ and ’,’.21 The object of study in mathematics is frequently a set together with a structure defined on it. For example, the set22 of triangles with similarity relations, the set of real numbers with the operations of addition and multiplications, and23 so on. A more precise definition of this concept has been introduced by the next definition of a formal system. The24 formal system is a tuple hU,R,M,Ciwhere Uis a nonempty set, Ris a finite set of relations on U,Mis a finite set25 of operations on U,Cis a finite (possibly empty) set of distinguished elements on U.26 Then, the formal systems have been characterized with signatures. A signature µis a mapping that associates some27 natural number called arity to every relation and operation. The arity gives the number of arguments of relations or28 operations. Thus, the formal system is a quintuple hU,R,M,C, µi. The description languages of the formal systems29 appear with signatures in the form hR∗,M∗,C∗, µiwhere the elements of R∗,M∗,C∗are names of the elements of30 R,M,Cand µis the associated signature.31 Example 1.1. The arithmetic as a formal system is the quintuple hN0,R,M,C, µi. The description language is the32 tuple h{≤},{s,+,×},{0}, µiwhere33 –≤is the name of the only relation in R,34 –s,+,×are the signs of the operations in M,35 – 0 identifies the smallest element of the universe N0,36 – and the signature is the following:37 Rµ(R)Mµ(M) ≤2s1 +2 ×2 38 The effect of the above mentioned approach appears later in the various definitions of the first-order languages.39 As in Definition 1.1, these languages contain three parts, (i) logical symbols, (ii) extralogical symbols and40 (iii) punctuation. The extralogical symbols vary from language to language, while the items (i) and (iii) are common41 to all languages.42 Definition 1.2. A first-order language of this kind is determined by specifying43 Please cite this article in press as: K. P´ asztor Varga, M. V´ arter´ esz, Languages of logic and their applications, Computers and Mathematics with Applications (2007), doi:10.1016/j.camwa.2007.06.007 UNCORRECTED PROOF CAMWA: 3975 ARTICLE IN PRESS K. P´ asztor Varga, M. V´ arter´ esz / Computers and Mathematics with Applications xx (xxxx) xxx–xxx 3 (ii) the sets of extralogical symbols 1 (1) P: a nonempty set of predicate symbols, 2 (2) F: a set of function symbols, 3 (3) C: a set of constant symbols, 4 and a signature µthat consists of mappings µPand µF, where 5 –µP:P→Ngives the arity of every predicate symbol, 6 –µF:F→Ngives the arity of every function symbol. 7 We use the notation hP,F,C, µifor the first-order language determined by the sets P,F,Cwith signature µ.8 Even now, it is usual to think of constant symbols as 0-ary function symbols. In these cases, a first-order language is 9 a triple hP,F, µi. The symbol sets P,Fand Cmay be finite or infinite and, except P, they may be even empty. Let 10 us mention that 11 •in works [7–10] the sets of predicate and function symbols are finite. These languages contain 12 (1) a finite nonempty set Pof the predicate symbols P1,P2,...,Pk(k≥1), 13 (2) a finite set Fof the function symbols f1,f2,..., fl(l≥0), 14 (3) a finite or countable set Cof the constant symbols c1,c2, . . . and a signature µsometimes designated as 15 P1P2· · · Pk;f1f2· · · fl n1n2· · · nk;m1m2· · · ml.16 •Certain authors [11–15] work with infinite sets of predicate and function symbols. In [16] Ershov and Palutyin 17 allow finite and infinite sets, as well. 18 Finally, it should be mentioned that Smullyan [17] also developed a definition for the first-order languages. His 19 language does not contain any function and constant symbol, it includes only the so-called parameter symbols instead. 20 Definition 1.3. The Smullyan’s version of the first-order languages consists of logical symbols (i), extralogical 21 symbols (ii) and punctuation (iii). 22 (ii) The extralogical symbols are determined by a pair hP,Pari, where 23 (1) Pis a countable list of n-ary predicate symbols for every natural number, 24 (2) Par is a countable list of symbols called parameters. 25 The role of parameter symbols is quite different from constant symbols. 26 Having specified the basic element of syntax, the alphabet, we go on to grammar rules of the languages. The 27 definition can be formulated for all logic languages in a common way. We specify the expressions (terms and formulae) 28 of a first-order language by inductive definitions which select certain “well-formed” strings of symbols, exactly those 29 we take as meaningful ones. It is obvious that only the symbols of the given logic language appear in the next grammar 30 rules effectively. 31 Definition 1.4 (Terms). 32 (i) Any variable, any constant symbol and any parameter symbol is a term. 33 (ii) If fis an n-ary function symbol and t1,t2,...,tnare terms, then f(t1,t2,...,tn)is a term too. 34 (iii) A string is a term only in the case if it can be constructed by finitely many applications of the rules (i)–(ii). 35 Definition 1.5 (Formulae). 36 (i) If Pis an n-ary predicate symbol and t1,t2,...,tnare terms, then P(t1,t2,...,tn)is an (atomic) formula. 37 (ii) (1) If Ais a formula so is ¬A.38 (2) If Aand Bare formulae, so are (A∧B), (A∨B),(A⊃B).39 (3) If Ais a formula and xis a variable, then ∀x A and ∃x A are formulae. 40 (iii) A string is a formula only if it can be generated by finitely many applications of the rules (i)–(ii). 41 We distinguish free and bound occurrences of variables. An occurrence of a variable xin a formula Ais bound if 42 there is a subformula of Acontaining that occurrence of xsuch that it begins with ∀xor ∃x. An occurrence of xin A43 is free if it is not bound. Additionally, an expression is called closed if no variable has free occurrence in it. 44 Please cite this article in press as: K. P´ asztor Varga, M. V´ arter´ esz, Languages of logic and their applications, Computers and Mathematics with Applications (2007), doi:10.1016/j.camwa.2007.06.007 UNCORRECTED PROOF CAMWA: 3975 ARTICLE IN PRESS 4K. P´ asztor Varga, M. V´ arter´ esz / Computers and Mathematics with Applications xx (xxxx) xxx–xxx 2. Semantics1 In [2] Frege gave the concept of quantifiers as ranging over all objects. The model in which a set is given and2 variables range over that given set was not introduced. In the 1890s, Schr¨ oder developed the idea of the model for the3 first-order logic languages. A model consists of a nonempty set, the domain or universe, together with relations and4 functions on this set according to relation and function symbols in the language. A first-order language with a model5 becomes a description language of an assigning formal system. At this stage, it becomes reasonable to ask whether6 some formulae are true or not in a given model.7 Definition 2.1. A model for the first-order language hP,F,C, µiis a pair hU,Iiwhere8 (i) Uis a nonempty set, called the universe,9 (ii) Iis a mapping, called interpretation that associates10 (1) some n-ary relation I(P):Un→ {true,false}to every n-ary predicate symbol Pof P,11 (2) some n-ary function I(f):Un→Uto every n-ary function symbol fof F,12 (3) and some member I(c)∈Uto every constant symbol cin C.13 To determine the meaning of terms and formulae, we have to define the evaluation of the variables of the language.14 In an evaluation, the variables mean elements of the universe. Two ways of reference to the universe elements will be15 presented: either with a mapping κ:V→Ucalled an assignment or with extending the language.16 Suppose, we have a model, which gives the meaning of the constant and function symbols of the language, and17 we have an assignment evaluating the variables. Then, we have enough information to calculate values for arbitrary18 terms.19 Definition 2.2. Let hU,Iibe a model for the language hP,F,C, µi, and let κbe an assignment in this model. To20 each term tof hP,F,C, µi, we assign a value |t|I,κ in Uas follows:21 (i) (1) for a constant symbol c∈C,|c|I,κ is the element I(c)of U,22 (2) for a variable x,|x|I,κ is the element κ(x)of U,23 (ii) |f(t1,t2,...,tn)|I,κ =I(f)(|t1|I,κ ,|t2|I,κ ,...,|tn|I,κ ).24 This definition associates an element in Uwith each term of the language. If the term is closed its value does not25 depend on the assignment κ.26 Now, we associate a truth value with each formula. For this, we need a preliminary notion. Let xbe a variable. The27 assignment κ∗in the model hU,Iiis an x-variant of the assignment κ, if κ∗(y)=κ(y)for any variable yexcept x.28 Definition 2.3. Let hU,Iibe a model for the language hP,F,C, µi, and let κbe an assignment in this model. To29 each formula Aof hP,F,C, µi, we assign a truth value |A|I,κ as follows:30 (i) |P(t1,t2,...,tn)|I,κ =I(P)(|t1|I,κ ,|t2|I,κ ,...,|tn|I,κ ).31 (ii) (1) |¬A|I,κ =true, if and only if |A|I,κ =false,32 (2) |A∧B|I,κ =true, if and only if |A|I,κ =true and |B|I,κ =true,33 (3) |A∨B|I,κ =true, if and only if |A|I,κ =true or |B|I,κ =true,34 (4) |A⊃B|I,κ =true, if and only if |A|I,κ =false or |B|I,κ =true,35 (iii) (1) |∀x A|I,κ =true, if and only if |A|I,κ∗=true for every assignment κ∗which is an x-variant of κ,36 (2) |∃x A|I,κ =true, if and only if |A|I,κ =true for some assignment κ∗which is an x-variant of κ.37 Just as with terms, if the formula is closed then its truth value does not depend on the assignment. Moreover, the38 value of an expression with nfree variables depends on the assignment of these variables, so its meaning in the model39 is an n-ary function or relation over the universe.40 By the grammar, a particular language expression can contain only finite number of symbols. Thus, to specify41 the meaning of an expression, we have to know the interpretation only for the symbols occurring in the expression42 (instead of the whole language). We can say that the semantics does not mean the interpretation of the language itself,43 but the interpretation of symbols of the given expression. This fact makes reasonable the introduction of languages44 with finite predicate, function and constant symbol sets. Please cite this article in press as: K. P´ asztor Varga, M. V´ arter´ esz, Languages of logic and their applications, Computers and Mathematics with Applications (2007), doi:10.1016/j.camwa.2007.06.007 UNCORRECTED PROOF CAMWA: 3975 ARTICLE IN PRESS K. P´ asztor Varga, M. V´ arter´ esz / Computers and Mathematics with Applications xx (xxxx) xxx–xxx 5 The following definitions based on the notion of interpretation have great importance for logic. 1 Definition 2.4. (i) A formula Ais said to be valid, |H A, if |A|I,κ =true for any model hU,Iiand any assignment 2 κin this model. 3 (ii) A set Sof formulae is satisfiable if there is a model hU,Iiof Land an assignment κin this model so that 4 |A|I,κ =true for every formula Aof S.5 A further fundamental idea of logic is the notion of semantic consequence. 6 Definition 2.5. We say that a formula Ais a semantic consequence of a set Sof formulae (written S|H A) if S∪{¬A}7 is unsatisfiable. 8 The semantic decision problem is to decide whether this relationship holds between Sand A. There exists an 9 equivalent formulation of this problem if S6= ∅.10 Theorem 2.1 (Deduction Theorem). Let A be a formula. Suppose B is a member of the set Sof formulae. Then, 11 S|H A if and only if S\ {B} |H B⊃A. 12 As it was shown in [7,12,14], the languages can be extended with new symbols denoting different elements of 13 the universe to be able to describe a pre-interpretation. The introduction of symbols for naming the elements of the 14 universe is common in the description language of some mathematical structures. For example, we can extend the 15 description language of the arithmetics by naming the natural numbers. The name of a number can be a sequence of 16 digits 0,1,...,9. We do this regardless of the successor function guarantees the referencing of natural numbers. The 17 usage of the extended languages is comfortable in applications. 18 Following Girard’s idea, if Uis the universe of a model of a first-order language, we introduce a constant symbol 19 cufor naming each element uof U.20 Definition 2.6. A model Mfor the language L= hP,F,∅, µiconsists of 21 (i) a nonempty set U, the domain of the model M,22 (ii) a mapping I, the interpretation of the model M, that associates 23 (1) to every n-ary predicate symbol Pof P, a relation I(P):Un→ {true,false},24 (2) to every n-ary function symbol fof F, a function I(f):Un→U.25 We extend the language Lto L[M]by introducing new constant symbols cufor all u∈U. Then, we extend the 26 interpretation for the new symbols: I(cu)=u∈Ufor all cu.27 Definition 2.7. First, we associate a value |t|Iwith each closed term tof the extended language L[M]as follows: 28 (i) |cu|I=u,29 (ii) |f(t1,t2,...,tn)|I=I(f)(|t1|I,|t2|I,...,|tn|I).30 Definition 2.8. Now, we associate a truth value |A|Iwith each closed formula Aof L[M]as follows: 31 (i) |P(t1,t2,...,tn)|I=I(P)(|t1|I,|t2|I,...,|tn|I),32 (ii) equally as (ii) in Definition 2.3,33 (iii) (1) |∀x A|I=true if and only if |Ax cu|I=true for all uin U,34 (2) |∃x A|I=true if and only if there exists an usuch in Uthat |Ax cu|I=true.35 Finally, we show the semantics of Smullyan’s language hP,Pari. First, we give a nonempty set Ucalled universe, 36 then we introduce the notion of formulae with elements in Uor more briefly U-formulae. 37 Definition 2.9 (U-formulae). 38 (i) If Pis an n-ary predicate symbol and t1,t2,...,tnare either variables or elements of U, then P(t1,t2,...,tn)is 39 an atomic U-formula. 40 (ii) (1) If Ais an U-formula so is ¬A.41 (2) If Aand Bare U-formulae, so are (A∧B), (A∨B),(A⊃B).42 (3) If Ais an U-formula and xis a variable, then ∀x A and ∃x A are U-formulae. 43 (iii) An expression is a U-formula only if it can be generated by the conditions (i)–(ii). Please cite this article in press as: K. P´ asztor Varga, M. V´ arter´ esz, Languages of logic and their applications, Computers and Mathematics with Applications (2007), doi:10.1016/j.camwa.2007.06.007 UNCORRECTED PROOF CAMWA: 3975 ARTICLE IN PRESS 6K. P´ asztor Varga, M. V´ arter´ esz / Computers and Mathematics with Applications xx (xxxx) xxx–xxx Note that, a U-formula does not contain any parameter, moreover it is not in the original language hP,Pariif only1 one element of Uoccurs in it.2 Over a fixed universe U, the meaning of predicate symbols of language is given by an interpretation Iwhich3 assigns a relation I:Un→ {true,false}to each n-ary predicate symbol Pof P.4 Definition 2.10. In a model hU,Iiof the language hP,Pariwe can get truth values to the closed U-formulae:5 (i) |P(u1,u2,...,un)|I=I(P)(u1,u2,...,un).6 (ii) equally as (ii) in Definition 2.3,7 (iii) (1) |∀x A|I=true if and only if |Ax u|I=true for all u∈U,8 (2) |∃x A|I=true if and only if there is a u∈Uthat |Ax u|I=true.9 We have considered so far closed U-formulae. Now, let A(a1,a2,...,an)be a closed formula containing exactly10 the parameters a1,a2,...,an. Observe that, we will not fix any interpretation for the parameters. For any universe11 Uand any elements u1,u2,...,unof U, we obtain A(u1,u2,...,un)by substituting u1for a1,. . .,unfor anin the12 sentence A(a1,a2,...,an).13 Definition 2.11. A(a1,a2,...,an)is called satisfiable if there exists at least one model hU,Iiand at least one n-tuple14 (u1,u2,...,un)of Usuch that |A(u1,u2,...,un)|I=true.15 One can see that the two groups of the first-order languages are the classical languages hP,F,C, µiand the16 language hP,Pari.17 •The symbol system and uniform syntax make the different languages suitable for formalization of an arbitrary18 first-order problem, but language hP,Pari. Missing function symbols do not cause any problem, because an n-ary19 operation can be defined by an (n+1)-ary relation.20 •The semantics is uniform, so both the semantic properties of a formula or set of formulae and the notion of semantic21 consequence can be defined for every language in the same way. Similarly, the proof of deduction theorem and the22 drafting of the semantic decision problem do not depend on the language.23 3. Naming the universe elements24 Now, we show the necessity of naming the universe elements to obtain some important results in logic.25 In the course of the solution of a semantic decision problem, the issue of perspicuity of all the interpretations over26 a given universe is raised. We can give any interpretation with the evaluation of the so-called ground atoms (closed U-27 atoms) in the language hP,Pari. Remember, the U-formulae, so the ground atoms are really in an extended language.28 Here, the interpretations can be considered as points of a field determined by all the ground atoms: a sequence of all29 ground atoms is called a base and an interpretation is a subsequence of the base, components of which we consider30 true. Interpretations determined in such form can be given by a semantic tree building on the base.31 Example 3.1. Let h{P},Paribe a language where Pis a binary predicate symbol and let U= {a,b}be a universe.32 Then, P(a,a), P(b,b), P(a,b), P(b,a)is a base, P(a,a), P(b,b)and P(a,a), P(b,b), P(b,a)are interpretations.33 The complete semantic tree based on this base is given in Fig. 1.Q134 In case of classical languages hP,F,Ci, when we cannot work with ground atoms since an assignment maps35 variables to elements of a universe, and the members of the universe probably will not be terms of the language we36 are using. So, if we replace a variable in a formula by what an assignment maps it to, we will not get a formula of our37 original language as a result. Here, we can see the reason of the Gerard’s language extension. In the extended language38 we can describe the ground atoms, and examine the interpretations over the given universe with the help of a semantic39 tree. Of course, besides the elements of P, we must interpret all the elements of Ffor a complete interpretation if40 F6= ∅.Q241 It is inconvenient and impossible to consider all interpretations over all universes. It would be nice if we could42 construct a special universe such that we would have to take into account only the interpretations over that universe.43 Definition 3.1. A Herbrand universe for a first-order language L= hP,F,Ci(C6= ∅) is the set of closed terms44 generated from function symbols of Fand constant symbols of C.45 Please cite this article in press as: K. P´ asztor Varga, M. V´ arter´ esz, Languages of logic and their applications, Computers and Mathematics with Applications (2007), doi:10.1016/j.camwa.2007.06.007 UNCORRECTED PROOF CAMWA: 3975 ARTICLE IN PRESS K. P´ asztor Varga, M. V´ arter´ esz / Computers and Mathematics with Applications xx (xxxx) xxx–xxx 7 Fig. 1. Observe that, the members of the Herbrand universe are ground terms of Land at the same time names of universe 1 elements. Here, the names of the elements depend on the language. Listing the members of the Herbrand universe 2 determines an interpretation for the function symbols: naming the elements of the universe with h1,h2, . . . we get an 3 interpretation for the function symbols over the set {h1,h2, . . .}.4 The following theorem is important because it traces back the examination of clauses of hP,F,Cito the 5 examination of formulae of hP,∅,Ciover the Herbrand universe. (The clauses are closed formulae in form 6 ∀x1∀x2· · · ∀xnAwhere Ais a disjunction of atoms and negations of atoms.) 7 Theorem 3.1. A set of clauses Sof Lis unsatisfiable if and only if the set of all ground instances from the Herbrand 8 universe of the clauses in Sis unsatisfiable. 9 This result led to the development of the so-called ground resolution calculus. The resolution rule for ground 10 clauses is 11 L1∨ · · · ∨ Ln∨A¬A∨K1∨ · · · ∨ Km L1∨ · · · ∨ Ln∨K1∨ · · · ∨ Km .12 Here, Li,Kj(1≤i≤n,1≤j≤m)are ground atoms or negation of them, and Ais a single atom. A ground 13 resolution derivation out of set S0of ground clauses is a sequence S0,S1, . . . of sets of ground clauses such that for 14 each k≥1, Sk+1is obtained by the application of this resolution rule to some pair of clauses in Sk. The ground 15 resolution procedure terminates, when an Skcontaining the so-called empty clause (with no atom) arises. Such an Sk16 is unsatisfiable. 17 A more general resolution rule forms the basis of the promised method for arbitrary clauses, which is more efficient 18 than the straightforward method of enumerating ground instances of certain clauses described before. The principal 19 idea behind this concept is that of unification. Unification is a process providing a systematic means of finding 20 substitutions which give rise to sets of ground instances of clauses whose existence is guaranteed by Theorem 3.1. To 21 describe such a substitution it can be necessary naming the universe elements, too. 22 Sets, whether finite or infinite, obeying the following conditions are of fundamental importance in the tableau 23 calculus. 24 Definition 3.2. Consider the language L= hP,Pariwith a universe U. A set Hof closed U-formulae is called a 25 first-order Hintikka set with respect to U, provided His a propositional Hintikka set (see [17]), and in addition: 26 (1) If ∀x A ∈H, then Ax u∈Hfor every uin U.27 (2) If ∃x A ∈H, then Ax u∈Hfor at least one element uin U.28 The next theorem connects syntax and semantics. 29 Theorem 3.2 (Hintikka’s Lemma). Every first-order Hintikka set Hwith respect to Uis satisfiable over the 30 universe U.31 Please cite this article in press as: K. P´ asztor Varga, M. V´ arter´ esz, Languages of logic and their applications, Computers and Mathematics with Applications (2007), doi:10.1016/j.camwa.2007.06.007 UNCORRECTED PROOF CAMWA: 3975 ARTICLE IN PRESS 8K. P´ asztor Varga, M. V´ arter´ esz / Computers and Mathematics with Applications xx (xxxx) xxx–xxx According to [17] the first-order tableau rules for the language hP,Pariare the following:1 ∀x A Ax a (for any a∈Par), ∃x A Ax a (for a critical a∈Par).2 The second rule is a formalization of the next informal argument. Suppose that in the course of a proof, we have3 established ∃x A. Then, we can say, let abe the name for an element having the property A. Here, we can use only such4 a symbol that has not been assigned any role yet. Since the parameters of the language hP,Pariare “uncommitted”,5 a critical (so that a new) one is always available for this purpose. Here, we can see the motivation of introduction of6 parameters to the logic language.7 The tableau rules provide to arise Hintikka sets with respect to the set of parameters as a universe on the open8 branches (branch without any complement formula pair) of any finished systematic tableau. The universe is a special9 one: the parameters are names of the universe elements again. From the Hintikka’s lemma we have at once that in any10 finished systematic tableau, every open branch is satisfiable (over this universe).11 In the case of the languages hP,F,Cithe first-order tableau rules are given in the next form [11]12 ∀x A Ax t (for any term t), ∃x A Ax y (for a critical variable y).13 An arbitrary term is substituted into the body of a universal formula and any variable is substituted into the body of an14 existential formula which is not free in any formula of the branch which is being extended. The rules provide only, that15 the set of formulae arising on an open branch is a Hintikka set in hP,F,Ci. According to [11] this set is satisfiable16 over the set of equivalence classes of terms introduced by tableau rules.17 4. Toward the unified way to prove completeness18 Soundness and completeness of a deduction system show its suitability for the treatment of logic. In this case, the19 syntactic and semantic constructions of logic are equivalent. The definitions of soundness and completeness properties20 and their proofs depend on the deduction system itself.21 A deduction system is called sound, whenever its decision problem is solved for a given set of formulae, then this22 formula set has a special semantic property. Let us list the soundness theorems (H) for the Hilbert system, (R) for the23 resolution calculus and (T) for the tableau calculus.24 Theorem 4.1 (Soundness).25 (H) If a formula A is deducible from a set Sof formulae (in the Hilbert system), then S|H A.26 (R) If the empty clause has resolution deduction from a set Sof clauses, then Sis unsatisfiable.27 (T) If the tableau of a set Sof formulae is closed, then Sis unsatisfiable.28 To prove the soundness property of a deduction system is not hard. In every case, the key fact needed is the29 soundness of the deduction rules.30 Completeness of a deduction system means that if a set of formulae has the semantic property given by soundness,31 then the calculus works successfully over that set of formulae. The completeness theorems for the above systems are32 as follows.33 Theorem 4.2 (Completeness).34 (H) If S|H A, then A is deducible from S.35 (R) If a set Sof clauses is unsatisfiable, then the empty clause has resolution deduction from S.36 (T) If a set Sof formulae is unsatisfiable, then the tableau of Sis closed.37 By semantics, a set of formulae is either satisfiable or not. This semantic property divides the set Ωof sets of38 formulae into two disjoint parts. In a given calculus we can define a syntactic property for the sets of formulae39 dividing the set Ωinto two disjoint parts, as well. This is generally called consistency (inconsistency) property. The40 definition of the (in)consistency property depends on the deduction system. Please cite this article in press as: K. P´ asztor Varga, M. V´ arter´ esz, Languages of logic and their applications, Computers and Mathematics with Applications (2007), doi:10.1016/j.camwa.2007.06.007 UNCORRECTED PROOF CAMWA: 3975 ARTICLE IN PRESS K. P´ asztor Varga, M. V´ arter´ esz / Computers and Mathematics with Applications xx (xxxx) xxx–xxx 9 Definition 4.1. (H) Sis inconsistent if Aand ¬Aare deducible from S.1 (R) A set Sof clauses is inconsistent if the empty clause has resolution deduction from the set S.2 (T) The set Sof formulae is inconsistent if the tableau of Sis closed. 3 It is obvious that, the soundness and completeness properties of a deduction system can be expressed by the 4 (in)consistency property: soundness requires that if Sis inconsistent, then Smust be unsatisfiable, and completeness 5 requires that if Sis unsatisfiable, then Smust be inconsistent. Then, completeness of a deduction system is proved 6 by showing that the consistency–inconsistency (syntactic) properties and the satisfiability–unsatisfiability (semantic) 7 properties divide into the same two parts the set Ωof sets of formulae. 8 Let Γdenote any property of formula sets which is of finite character. It means that a set Shas the property Γif 9 and only if all finite subset of Shave the property Γ.10 Definition 4.2. In the language L= hP,Pari, a property Γof finite character is called an analytic consistency 11 property for first-order logic if Γis an analytic consistency property for propositional logic [17], and if for every set 12 Sof formulae of Lhaving the property Γthe following conditions hold: 13 (1) If ∀x A ∈S, then for every a∈Par,S∪ {Ax a}has the property Γ.14 (2) If ∃x A ∈S, then S∪ {Ax a}has the property Γ, if a∈Par does not occur in S.15 An important example of an analytic consistency property is the consistency property in the tableau method. 16 Theorem 4.3 (Unifying Principle). If Γis an analytic consistency property, Sis a set of parameter-free formulae in 17 hP,Pari, and Shas the property Γ, then Sis satisfiable. 18 It is clear that a set Sof formulae having an analytic consistency property can be embedded into a Hintikka set 19 with respect to the set of parameters as a universe, so it is satisfiable. 20 Consequently, instead of proving the different completeness theorems it is sufficient to test whether the consistency 21 property in a given deduction system is an analytic consistency property. If the consistency property is an analytic 22 consistency property, then this fact is equivalent to the completeness of this deduction system. By this result we get a 23 unified method to treat the completeness problem of a deduction system in the first-order logic. 24 There is another important application of the unifying principle. It is easily verified that the following property Γ25 is an analytic consistency property: Let a set Sof parameter-free formulae in hP,Parihave the property Γ, if all of 26 its finite subsets are satisfiable. Using Theorem 4.3, we get the so-called compactness theorem for first-order logic: If 27 every finite subset of Sis satisfiable, so is S.28 5. Applications 29 Many applications of logic, mainly in the artificial intelligence, are related to the deduction systems. In these 30 applications, naming the universe elements is inevitable. To solve a problem by a deduction system the following 31 steps are executed. 32 (I) The first task is to create an ideal world, a mathematical model for the problem, in which the classical logic can 33 be used to reason correctly. (Whether the model accurately reflects the real world is a separate issue.) In this 34 model we have a universe. Our ideal world is characterized by operations and relations on this universe. 35 (II) The second task is to find a description language for the ideal world. The extralogical part of the alphabet consists 36 of predicate and function symbols identifying the relations and operations of the model. For describing assertions 37 about universe elements, it is necessary to introduce constant symbols naming them. 38 (III) This language is suitable for formalization of the original problem. The result of formalization is often a finite set 39 of formulae (premises) and a formula (conclusion) in the language. The third task is to test whether the conclusion 40 is a consequence of premises. The actually used deduction system tries to give the answer with solving its own 41 decision problem according to the original one. 42 In the case of using the resolution calculus (for example in a Prolog system) the Herbrand universe is used, 43 where the constant symbols of the language are the constant elements of the Herbrand universe. If there are 44 function symbols in the language, then the ground terms are also elements of the Herbrand universe. As the 45 problem has the originally fixed universe, then the Herbrand universe shows an interpretation of function symbols 46 Please cite this article in press as: K. P´ asztor Varga, M. V´ arter´ esz, Languages of logic and their applications, Computers and Mathematics with Applications (2007), doi:10.1016/j.camwa.2007.06.007