UNCORRECTED PROOF
CAMWA: 3975 + Model pp. 1–10 (col. ig: NIL)
ARTICLE IN PRESS
Compu e s and Ma hema ics wi h Applica ions xx (xxxx) xxx–xxx
www.else ie .com/loca e/camwa
Languages o logic and hei applica ions
K. P´
asz o Va gaa,∗, M. V´
a e ´
eszb
aDepa men o P og amming Languages and Compile s, E¨
o ¨
os Lo ´
and Uni e si y, H-1117 Budapes , P´
azm´
any P´
e e s´
e ´
any 1/C., Hunga y
bFacul y o In o ma ics, Uni e si y o Deb ecen, H-4010 Deb ecen, P.O.Box 12., Hunga y
Recei ed 15 May 2007; accep ed 7 June 2007
1
2
Abs ac 3
Conce ning he logical desc ip ion languages, in he pas 40–50 yea s many au ho s ha e in oduced a numbe o s uc u ally 4
e y di e en i s -o de languages. Some o hese languages ollow he s uc u e o a gi en u u e model, o he ones ha e been 5
p epa ed o he desc ip ion o an a bi a y model. O he a ia ions o he i s -o de languages do no ollow he whole s uc u e o 6
any model: hey ha e been p epa ed only o he ela ions de inable o e he uni e se in o de o be able o p o e he gene aliza ions 7
o a numbe o di icul logical esul s. 8
The seman ics o he i s -o de languages is based on he in e p e a ion o hei ex alogical symbols by a sui able model. In 9
some cases, in he in e p e a ion all possible models can be in ocus, bu he e a e cases when he models o e a special uni e se 10
a e ega ded. The naming p oblem o he uni e se elemen o he model a ises a his s age. The e o s o sol ing his p oblem 11
lead o di e en app oaches. 12
He e, we p esen he mos impo an language de ini ions and some cha ac e is ic seman ics. We in es iga e he di e en 13
app oaches and conclude ha hey do no indica e essen ial di e ences. In ac , hey ha e been only mo i a ed by seeking o 14
an easie way o achie e he jus ixed a ge . Mo eo e , we y o poin ou he sui abili y connec ions o languages and seman ics 15
de ini ions. 16
c
2007 Published by Else ie L d 17
Keywo ds: Fi s -o de languages; Syn ax; Seman ics
18
1. Syn ax 19
Leibniz (1640–1710) was he i s , who b ough up he idea o a comple e o mal logical easoning sys em. He 20
ied o de elop a language, and a calculus o easoning, called hem he “lingua cha ac e is ica” (uni e sal language) 21
and he “calculus a iocina o ” (calculus o easoning). Leibniz’s wo k in his a ea was basically unknown ill i s 22
publica ion in [1], so his ideas we e p escien bu no in luen ial. F ege de eloped he base o he mode n logical 23
g amma in his book [2] in 1879. He ga e he i s o mal ea men o logic including bo h quan i ie s, ela ion 24
symbols and p oposi ional connec i es. F ege ga e, also o he i s ime, he de ini ion o a p oo as a ini e sequence 25
o o mulae, each o which is ei he an axiom o ollows om p e ious o mulae o he p oo by an applica ion o 26
a ule o in e ence. The app ecia ion o F ege’s wo ks is also pos e io p obably because o hei ha d eadabili y. 27
∗Co esponding au ho .
E-mail add esses: [email p o ec ed] (K. P´
asz o Va ga), [email p o ec ed].hu (M. V´
a e ´
esz).
0898-1221/$ - see on ma e c
2007 Published by Else ie L d
doi:10.1016/j.camwa.2007.06.007
Please ci e his a icle in p ess as: K. P´
asz o Va ga, M. V´
a e ´
esz, Languages o logic and hei applica ions, Compu e s and Ma hema ics wi h
Applica ions (2007), doi:10.1016/j.camwa.2007.06.007
UNCORRECTED PROOF
CAMWA: 3975
ARTICLE IN PRESS
2K. P´
asz o Va ga, M. V´
a e ´
esz / Compu e s and Ma hema ics wi h Applica ions xx (xxxx) xxx–xxx
In 1889 Peano published a pape [3] simila o F ege’s concep ion, bu his no a ion sys em was qui e o he . In con as 1
wi h F ege’s pape s, his no a ion sys em became known as and widely used. Roughly speaking, Peano’s no a ion2
ex ended and modi ied by Russell and Hilbe is used oday. Mo eo e , o ge ing ha F ege was he i s who applied3
his calculus, i is called Hilbe s yle in he li e a u e. In he 1920s, L¨
owenheim and Skolem obse ed ha unc ion4
symbols and cons an symbols (p ospec i e names o elemen s o a domain) may be use ul o o mal ea men o 5
logic. In e ec , cons uc ions om hese i ems make se s o e ms in o he i s -o de logic languages.6
In ac , de elopmen and publica ions o di e en e sions o he i s -o de logic languages in cu en use ha e7
some pe iods. In he i s gene al wo ks a e 1930s [4–6] he sys em o ex alogical symbols o i s -o de languages8
ook shape om he signs o (ma hema ical and logical) unc ions. The logical componen s o logic languages a e9
common (connec i es, quan i ie s and a coun able se o (indi iduum) a iables). Now, we gi e a o mal de ini ion o 10
wha such a language cons i u es.11
De ini ion 1.1. The alphabe o a i s -o de language consis s o 12
(i) logical symbols:13
(1) connec i es and quan i ie s: ¬,∧,∨,⊃,∀,∃,14
(2) a iables: x1,x2,x3, . . .,15
(ii) ex alogical symbols:16
(1) o each na u al numbe n, named n-a y p edica e symbols: Pn
1,Pn
2,Pn
3, . . .,17
(2) o each na u al numbe n, named n-a y unc ion symbols: n
1, n
2, n
3, . . .,18
(3) cons an symbols: c1,c2,c3, . . . ( he cons an symbols may be simply lis ed as 0-a y unc ion symbols19
0
1, 0
2, 0
3, . . .),20
(iii) punc ua ion: ’)’, ’(’ and ’,’.21
The objec o s udy in ma hema ics is equen ly a se oge he wi h a s uc u e de ined on i . Fo example, he se 22
o iangles wi h simila i y ela ions, he se o eal numbe s wi h he ope a ions o addi ion and mul iplica ions, and23
so on. A mo e p ecise de ini ion o his concep has been in oduced by he nex de ini ion o a o mal sys em. The24
o mal sys em is a uple hU,R,M,Ciwhe e Uis a nonemp y se , Ris a ini e se o ela ions on U,Mis a ini e se 25
o ope a ions on U,Cis a ini e (possibly emp y) se o dis inguished elemen s on U.26
Then, he o mal sys ems ha e been cha ac e ized wi h signa u es. A signa u e µis a mapping ha associa es some27
na u al numbe called a i y o e e y ela ion and ope a ion. The a i y gi es he numbe o a gumen s o ela ions o 28
ope a ions. Thus, he o mal sys em is a quin uple hU,R,M,C, µi. The desc ip ion languages o he o mal sys ems29
appea wi h signa u es in he o m hR∗,M∗,C∗, µiwhe e he elemen s o R∗,M∗,C∗a e names o he elemen s o 30
R,M,Cand µis he associa ed signa u e.31
Example 1.1. The a i hme ic as a o mal sys em is he quin uple hN0,R,M,C, µi. The desc ip ion language is he32
uple h{≤},{s,+,×},{0}, µiwhe e33
–≤is he name o he only ela ion in R,34
–s,+,×a e he signs o he ope a ions in M,35
– 0 iden i ies he smalles elemen o he uni e se N0,36
– and he signa u e is he ollowing:37
Rµ(R)Mµ(M)
≤2s1
+2
×2
38
The e ec o he abo e men ioned app oach appea s la e in he a ious de ini ions o he i s -o de languages.39
As in De ini ion 1.1, hese languages con ain h ee pa s, (i) logical symbols, (ii) ex alogical symbols and40
(iii) punc ua ion. The ex alogical symbols a y om language o language, while he i ems (i) and (iii) a e common41
o all languages.42
De ini ion 1.2. A i s -o de language o his kind is de e mined by speci ying43
Please ci e his a icle in p ess as: K. P´
asz o Va ga, M. V´
a e ´
esz, Languages o logic and hei applica ions, Compu e s and Ma hema ics wi h
Applica ions (2007), doi:10.1016/j.camwa.2007.06.007
UNCORRECTED PROOF
CAMWA: 3975
ARTICLE IN PRESS
K. P´
asz o Va ga, M. V´
a e ´
esz / Compu e s and Ma hema ics wi h Applica ions xx (xxxx) xxx–xxx 3
(ii) he se s o ex alogical symbols 1
(1) P: a nonemp y se o p edica e symbols, 2
(2) F: a se o unc ion symbols, 3
(3) C: a se o cons an symbols, 4
and a signa u e µ ha consis s o mappings µPand µF, whe e 5
–µP:P→Ngi es he a i y o e e y p edica e symbol, 6
–µF:F→Ngi es he a i y o e e y unc ion symbol. 7
We use he no a ion hP,F,C, µi o he i s -o de language de e mined by he se s P,F,Cwi h signa u e µ.8
E en now, i is usual o hink o cons an symbols as 0-a y unc ion symbols. In hese cases, a i s -o de language is 9
a iple hP,F, µi. The symbol se s P,Fand Cmay be ini e o in ini e and, excep P, hey may be e en emp y. Le 10
us men ion ha 11
•in wo ks [7–10] he se s o p edica e and unc ion symbols a e ini e. These languages con ain 12
(1) a ini e nonemp y se Po he p edica e symbols P1,P2,...,Pk(k≥1), 13
(2) a ini e se Fo he unc ion symbols 1, 2,..., l(l≥0), 14
(3) a ini e o coun able se Co he cons an symbols c1,c2, . . . and a signa u e µsome imes designa ed as 15
P1P2· · · Pk; 1 2· · · l
n1n2· · · nk;m1m2· · · ml.16
•Ce ain au ho s [11–15] wo k wi h in ini e se s o p edica e and unc ion symbols. In [16] E sho and Palu yin 17
allow ini e and in ini e se s, as well. 18
Finally, i should be men ioned ha Smullyan [17] also de eloped a de ini ion o he i s -o de languages. His 19
language does no con ain any unc ion and cons an symbol, i includes only he so-called pa ame e symbols ins ead. 20
De ini ion 1.3. The Smullyan’s e sion o he i s -o de languages consis s o logical symbols (i), ex alogical 21
symbols (ii) and punc ua ion (iii). 22
(ii) The ex alogical symbols a e de e mined by a pai hP,Pa i, whe e 23
(1) Pis a coun able lis o n-a y p edica e symbols o e e y na u al numbe , 24
(2) Pa is a coun able lis o symbols called pa ame e s. 25
The ole o pa ame e symbols is qui e di e en om cons an symbols. 26
Ha ing speci ied he basic elemen o syn ax, he alphabe , we go on o g amma ules o he languages. The 27
de ini ion can be o mula ed o all logic languages in a common way. We speci y he exp essions ( e ms and o mulae) 28
o a i s -o de language by induc i e de ini ions which selec ce ain “well- o med” s ings o symbols, exac ly hose 29
we ake as meaning ul ones. I is ob ious ha only he symbols o he gi en logic language appea in he nex g amma 30
ules e ec i ely. 31
De ini ion 1.4 (Te ms). 32
(i) Any a iable, any cons an symbol and any pa ame e symbol is a e m. 33
(ii) I is an n-a y unc ion symbol and 1, 2,..., na e e ms, hen ( 1, 2,..., n)is a e m oo. 34
(iii) A s ing is a e m only in he case i i can be cons uc ed by ini ely many applica ions o he ules (i)–(ii). 35
De ini ion 1.5 (Fo mulae). 36
(i) I Pis an n-a y p edica e symbol and 1, 2,..., na e e ms, hen P( 1, 2,..., n)is an (a omic) o mula. 37
(ii) (1) I Ais a o mula so is ¬A.38
(2) I Aand Ba e o mulae, so a e (A∧B), (A∨B),(A⊃B).39
(3) I Ais a o mula and xis a a iable, hen ∀x A and ∃x A a e o mulae. 40
(iii) A s ing is a o mula only i i can be gene a ed by ini ely many applica ions o he ules (i)–(ii). 41
We dis inguish ee and bound occu ences o a iables. An occu ence o a a iable xin a o mula Ais bound i 42
he e is a sub o mula o Acon aining ha occu ence o xsuch ha i begins wi h ∀xo ∃x. An occu ence o xin A43
is ee i i is no bound. Addi ionally, an exp ession is called closed i no a iable has ee occu ence in i . 44
Please ci e his a icle in p ess as: K. P´
asz o Va ga, M. V´
a e ´
esz, Languages o logic and hei applica ions, Compu e s and Ma hema ics wi h
Applica ions (2007), doi:10.1016/j.camwa.2007.06.007
UNCORRECTED PROOF
CAMWA: 3975
ARTICLE IN PRESS
4K. P´
asz o Va ga, M. V´
a e ´
esz / Compu e s and Ma hema ics wi h Applica ions xx (xxxx) xxx–xxx
2. Seman ics1
In [2] F ege ga e he concep o quan i ie s as anging o e all objec s. The model in which a se is gi en and2
a iables ange o e ha gi en se was no in oduced. In he 1890s, Sch ¨
ode de eloped he idea o he model o he3
i s -o de logic languages. A model consis s o a nonemp y se , he domain o uni e se, oge he wi h ela ions and4
unc ions on his se acco ding o ela ion and unc ion symbols in he language. A i s -o de language wi h a model5
becomes a desc ip ion language o an assigning o mal sys em. A his s age, i becomes easonable o ask whe he 6
some o mulae a e ue o no in a gi en model.7
De ini ion 2.1. A model o he i s -o de language hP,F,C, µiis a pai hU,Iiwhe e8
(i) Uis a nonemp y se , called he uni e se,9
(ii) Iis a mapping, called in e p e a ion ha associa es10
(1) some n-a y ela ion I(P):Un→ { ue, alse} o e e y n-a y p edica e symbol Po P,11
(2) some n-a y unc ion I( ):Un→U o e e y n-a y unc ion symbol o F,12
(3) and some membe I(c)∈U o e e y cons an symbol cin C.13
To de e mine he meaning o e ms and o mulae, we ha e o de ine he e alua ion o he a iables o he language.14
In an e alua ion, he a iables mean elemen s o he uni e se. Two ways o e e ence o he uni e se elemen s will be15
p esen ed: ei he wi h a mapping κ:V→Ucalled an assignmen o wi h ex ending he language.16
Suppose, we ha e a model, which gi es he meaning o he cons an and unc ion symbols o he language, and17
we ha e an assignmen e alua ing he a iables. Then, we ha e enough in o ma ion o calcula e alues o a bi a y18
e ms.19
De ini ion 2.2. Le hU,Iibe a model o he language hP,F,C, µi, and le κbe an assignmen in his model. To20
each e m o hP,F,C, µi, we assign a alue | |I,κ in Uas ollows:21
(i) (1) o a cons an symbol c∈C,|c|I,κ is he elemen I(c)o U,22
(2) o a a iable x,|x|I,κ is he elemen κ(x)o U,23
(ii) | ( 1, 2,..., n)|I,κ =I( )(| 1|I,κ ,| 2|I,κ ,...,| n|I,κ ).24
This de ini ion associa es an elemen in Uwi h each e m o he language. I he e m is closed i s alue does no 25
depend on he assignmen κ.26
Now, we associa e a u h alue wi h each o mula. Fo his, we need a p elimina y no ion. Le xbe a a iable. The27
assignmen κ∗in he model hU,Iiis an x- a ian o he assignmen κ, i κ∗(y)=κ(y) o any a iable yexcep x.28
De ini ion 2.3. Le hU,Iibe a model o he language hP,F,C, µi, and le κbe an assignmen in his model. To29
each o mula Ao hP,F,C, µi, we assign a u h alue |A|I,κ as ollows:30
(i) |P( 1, 2,..., n)|I,κ =I(P)(| 1|I,κ ,| 2|I,κ ,...,| n|I,κ ).31
(ii) (1) |¬A|I,κ = ue, i and only i |A|I,κ = alse,32
(2) |A∧B|I,κ = ue, i and only i |A|I,κ = ue and |B|I,κ = ue,33
(3) |A∨B|I,κ = ue, i and only i |A|I,κ = ue o |B|I,κ = ue,34
(4) |A⊃B|I,κ = ue, i and only i |A|I,κ = alse o |B|I,κ = ue,35
(iii) (1) |∀x A|I,κ = ue, i and only i |A|I,κ∗= ue o e e y assignmen κ∗which is an x- a ian o κ,36
(2) |∃x A|I,κ = ue, i and only i |A|I,κ = ue o some assignmen κ∗which is an x- a ian o κ.37
Jus as wi h e ms, i he o mula is closed hen i s u h alue does no depend on he assignmen . Mo eo e , he38
alue o an exp ession wi h n ee a iables depends on he assignmen o hese a iables, so i s meaning in he model39
is an n-a y unc ion o ela ion o e he uni e se.40
By he g amma , a pa icula language exp ession can con ain only ini e numbe o symbols. Thus, o speci y41
he meaning o an exp ession, we ha e o know he in e p e a ion only o he symbols occu ing in he exp ession42
(ins ead o he whole language). We can say ha he seman ics does no mean he in e p e a ion o he language i sel ,43
bu he in e p e a ion o symbols o he gi en exp ession. This ac makes easonable he in oduc ion o languages44
wi h ini e p edica e, unc ion and cons an symbol se s.
Please ci e his a icle in p ess as: K. P´
asz o Va ga, M. V´
a e ´
esz, Languages o logic and hei applica ions, Compu e s and Ma hema ics wi h
Applica ions (2007), doi:10.1016/j.camwa.2007.06.007
UNCORRECTED PROOF
CAMWA: 3975
ARTICLE IN PRESS
K. P´
asz o Va ga, M. V´
a e ´
esz / Compu e s and Ma hema ics wi h Applica ions xx (xxxx) xxx–xxx 5
The ollowing de ini ions based on he no ion o in e p e a ion ha e g ea impo ance o logic. 1
De ini ion 2.4. (i) A o mula Ais said o be alid, |H A, i |A|I,κ = ue o any model hU,Iiand any assignmen 2
κin his model. 3
(ii) A se So o mulae is sa is iable i he e is a model hU,Iio Land an assignmen κin his model so ha 4
|A|I,κ = ue o e e y o mula Ao S.5
A u he undamen al idea o logic is he no ion o seman ic consequence. 6
De ini ion 2.5. We say ha a o mula Ais a seman ic consequence o a se So o mulae (w i en S|H A) i S∪{¬A}7
is unsa is iable. 8
The seman ic decision p oblem is o decide whe he his ela ionship holds be ween Sand A. The e exis s an 9
equi alen o mula ion o his p oblem i S6= ∅.10
Theo em 2.1 (Deduc ion Theo em). Le A be a o mula. Suppose B is a membe o he se So o mulae. Then, 11
S|H A i and only i S {B} |H B⊃A. 12
As i was shown in [7,12,14], he languages can be ex ended wi h new symbols deno ing di e en elemen s o 13
he uni e se o be able o desc ibe a p e-in e p e a ion. The in oduc ion o symbols o naming he elemen s o he 14
uni e se is common in he desc ip ion language o some ma hema ical s uc u es. Fo example, we can ex end he 15
desc ip ion language o he a i hme ics by naming he na u al numbe s. The name o a numbe can be a sequence o 16
digi s 0,1,...,9. We do his ega dless o he successo unc ion gua an ees he e e encing o na u al numbe s. The 17
usage o he ex ended languages is com o able in applica ions. 18
Following Gi a d’s idea, i Uis he uni e se o a model o a i s -o de language, we in oduce a cons an symbol 19
cu o naming each elemen uo U.20
De ini ion 2.6. A model M o he language L= hP,F,∅, µiconsis s o 21
(i) a nonemp y se U, he domain o he model M,22
(ii) a mapping I, he in e p e a ion o he model M, ha associa es 23
(1) o e e y n-a y p edica e symbol Po P, a ela ion I(P):Un→ { ue, alse},24
(2) o e e y n-a y unc ion symbol o F, a unc ion I( ):Un→U.25
We ex end he language L o L[M]by in oducing new cons an symbols cu o all u∈U. Then, we ex end he 26
in e p e a ion o he new symbols: I(cu)=u∈U o all cu.27
De ini ion 2.7. Fi s , we associa e a alue | |Iwi h each closed e m o he ex ended language L[M]as ollows: 28
(i) |cu|I=u,29
(ii) | ( 1, 2,..., n)|I=I( )(| 1|I,| 2|I,...,| n|I).30
De ini ion 2.8. Now, we associa e a u h alue |A|Iwi h each closed o mula Ao L[M]as ollows: 31
(i) |P( 1, 2,..., n)|I=I(P)(| 1|I,| 2|I,...,| n|I),32
(ii) equally as (ii) in De ini ion 2.3,33
(iii) (1) |∀x A|I= ue i and only i |Ax
cu|I= ue o all uin U,34
(2) |∃x A|I= ue i and only i he e exis s an usuch in U ha |Ax
cu|I= ue.35
Finally, we show he seman ics o Smullyan’s language hP,Pa i. Fi s , we gi e a nonemp y se Ucalled uni e se, 36
hen we in oduce he no ion o o mulae wi h elemen s in Uo mo e b ie ly U- o mulae. 37
De ini ion 2.9 (U- o mulae). 38
(i) I Pis an n-a y p edica e symbol and 1, 2,..., na e ei he a iables o elemen s o U, hen P( 1, 2,..., n)is 39
an a omic U- o mula. 40
(ii) (1) I Ais an U- o mula so is ¬A.41
(2) I Aand Ba e U- o mulae, so a e (A∧B), (A∨B),(A⊃B).42
(3) I Ais an U- o mula and xis a a iable, hen ∀x A and ∃x A a e U- o mulae. 43
(iii) An exp ession is a U- o mula only i i can be gene a ed by he condi ions (i)–(ii).
Please ci e his a icle in p ess as: K. P´
asz o Va ga, M. V´
a e ´
esz, Languages o logic and hei applica ions, Compu e s and Ma hema ics wi h
Applica ions (2007), doi:10.1016/j.camwa.2007.06.007

UNCORRECTED PROOF
CAMWA: 3975
ARTICLE IN PRESS
6K. P´
asz o Va ga, M. V´
a e ´
esz / Compu e s and Ma hema ics wi h Applica ions xx (xxxx) xxx–xxx
No e ha , a U- o mula does no con ain any pa ame e , mo eo e i is no in he o iginal language hP,Pa ii only1
one elemen o Uoccu s in i .2
O e a ixed uni e se U, he meaning o p edica e symbols o language is gi en by an in e p e a ion Iwhich3
assigns a ela ion I:Un→ { ue, alse} o each n-a y p edica e symbol Po P.4
De ini ion 2.10. In a model hU,Iio he language hP,Pa iwe can ge u h alues o he closed U- o mulae:5
(i) |P(u1,u2,...,un)|I=I(P)(u1,u2,...,un).6
(ii) equally as (ii) in De ini ion 2.3,7
(iii) (1) |∀x A|I= ue i and only i |Ax
u|I= ue o all u∈U,8
(2) |∃x A|I= ue i and only i he e is a u∈U ha |Ax
u|I= ue.9
We ha e conside ed so a closed U- o mulae. Now, le A(a1,a2,...,an)be a closed o mula con aining exac ly10
he pa ame e s a1,a2,...,an. Obse e ha , we will no ix any in e p e a ion o he pa ame e s. Fo any uni e se11
Uand any elemen s u1,u2,...,uno U, we ob ain A(u1,u2,...,un)by subs i u ing u1 o a1,. . .,un o anin he12
sen ence A(a1,a2,...,an).13
De ini ion 2.11. A(a1,a2,...,an)is called sa is iable i he e exis s a leas one model hU,Iiand a leas one n- uple14
(u1,u2,...,un)o Usuch ha |A(u1,u2,...,un)|I= ue.15
One can see ha he wo g oups o he i s -o de languages a e he classical languages hP,F,C, µiand he16
language hP,Pa i.17
•The symbol sys em and uni o m syn ax make he di e en languages sui able o o maliza ion o an a bi a y18
i s -o de p oblem, bu language hP,Pa i. Missing unc ion symbols do no cause any p oblem, because an n-a y19
ope a ion can be de ined by an (n+1)-a y ela ion.20
•The seman ics is uni o m, so bo h he seman ic p ope ies o a o mula o se o o mulae and he no ion o seman ic21
consequence can be de ined o e e y language in he same way. Simila ly, he p oo o deduc ion heo em and he22
d a ing o he seman ic decision p oblem do no depend on he language.23
3. Naming he uni e se elemen s24
Now, we show he necessi y o naming he uni e se elemen s o ob ain some impo an esul s in logic.25
In he cou se o he solu ion o a seman ic decision p oblem, he issue o pe spicui y o all he in e p e a ions o e 26
a gi en uni e se is aised. We can gi e any in e p e a ion wi h he e alua ion o he so-called g ound a oms (closed U-27
a oms) in he language hP,Pa i. Remembe , he U- o mulae, so he g ound a oms a e eally in an ex ended language.28
He e, he in e p e a ions can be conside ed as poin s o a ield de e mined by all he g ound a oms: a sequence o all29
g ound a oms is called a base and an in e p e a ion is a subsequence o he base, componen s o which we conside 30
ue. In e p e a ions de e mined in such o m can be gi en by a seman ic ee building on he base.31
Example 3.1. Le h{P},Pa ibe a language whe e Pis a bina y p edica e symbol and le U= {a,b}be a uni e se.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)a e in e p e a ions.33
The comple e seman ic ee based on his base is gi en in Fig. 1.Q134
In case o classical languages hP,F,Ci, when we canno wo k wi h g ound a oms since an assignmen maps35
a iables o elemen s o a uni e se, and he membe s o he uni e se p obably will no be e ms o he language we36
a e using. So, i we eplace a a iable in a o mula by wha an assignmen maps i o, we will no ge a o mula o ou 37
o iginal language as a esul . He e, we can see he eason o he Ge a d’s language ex ension. In he ex ended language38
we can desc ibe he g ound a oms, and examine he in e p e a ions o e he gi en uni e se wi h he help o a seman ic39
ee. O cou se, besides he elemen s o P, we mus in e p e all he elemen s o F o a comple e in e p e a ion i 40
F6= ∅.Q241
I is incon enien and impossible o conside all in e p e a ions o e all uni e ses. I would be nice i we could42
cons uc a special uni e se such ha we would ha e o ake in o accoun only he in e p e a ions o e ha uni e se.43
De ini ion 3.1. A He b and uni e se o a i s -o de language L= hP,F,Ci(C6= ∅) is he se o closed e ms44
gene a ed om unc ion symbols o Fand cons an symbols o C.45
Please ci e his a icle in p ess as: K. P´
asz o Va ga, M. V´
a e ´
esz, Languages o logic and hei applica ions, Compu e s and Ma hema ics wi h
Applica ions (2007), doi:10.1016/j.camwa.2007.06.007
UNCORRECTED PROOF
CAMWA: 3975
ARTICLE IN PRESS
K. P´
asz o Va ga, M. V´
a e ´
esz / Compu e s and Ma hema ics wi h Applica ions xx (xxxx) xxx–xxx 7
Fig. 1.
Obse e ha , he membe s o he He b and uni e se a e g ound e ms o Land a he same ime names o uni e se 1
elemen s. He e, he names o he elemen s depend on he language. Lis ing he membe s o he He b and uni e se 2
de e mines an in e p e a ion o he unc ion symbols: naming he elemen s o he uni e se wi h h1,h2, . . . we ge an 3
in e p e a ion o he unc ion symbols o e he se {h1,h2, . . .}.4
The ollowing heo em is impo an because i aces back he examina ion o clauses o hP,F,Ci o he 5
examina ion o o mulae o hP,∅,Cio e he He b and uni e se. (The clauses a e closed o mulae in o m 6
∀x1∀x2· · · ∀xnAwhe e Ais a disjunc ion o a oms and nega ions o a oms.) 7
Theo em 3.1. A se o clauses So Lis unsa is iable i and only i he se o all g ound ins ances om he He b and 8
uni e se o he clauses in Sis unsa is iable. 9
This esul led o he de elopmen o he so-called g ound esolu ion calculus. The esolu ion ule o g ound 10
clauses is 11
L1∨ · · · ∨ Ln∨A¬A∨K1∨ · · · ∨ Km
L1∨ · · · ∨ Ln∨K1∨ · · · ∨ Km
.12
He e, Li,Kj(1≤i≤n,1≤j≤m)a e g ound a oms o nega ion o hem, and Ais a single a om. A g ound 13
esolu ion de i a ion ou o se S0o g ound clauses is a sequence S0,S1, . . . o se s o g ound clauses such ha o 14
each k≥1, Sk+1is ob ained by he applica ion o his esolu ion ule o some pai o clauses in Sk. The g ound 15
esolu ion p ocedu e e mina es, when an Skcon aining he so-called emp y clause (wi h no a om) a ises. Such an Sk16
is unsa is iable. 17
A mo e gene al esolu ion ule o ms he basis o he p omised me hod o a bi a y clauses, which is mo e e icien 18
han he s aigh o wa d me hod o enume a ing g ound ins ances o ce ain clauses desc ibed be o e. The p incipal 19
idea behind his concep is ha o uni ica ion. Uni ica ion is a p ocess p o iding a sys ema ic means o inding 20
subs i u ions which gi e ise o se s o g ound ins ances o clauses whose exis ence is gua an eed by Theo em 3.1. To 21
desc ibe such a subs i u ion i can be necessa y naming he uni e se elemen s, oo. 22
Se s, whe he ini e o in ini e, obeying he ollowing condi ions a e o undamen al impo ance in he ableau 23
calculus. 24
De ini ion 3.2. Conside he language L= hP,Pa iwi h a uni e se U. A se Ho closed U- o mulae is called a 25
i s -o de Hin ikka se wi h espec o U, p o ided His a p oposi ional Hin ikka se (see [17]), and in addi ion: 26
(1) I ∀x A ∈H, hen Ax
u∈H o e e y uin U.27
(2) I ∃x A ∈H, hen Ax
u∈H o a leas one elemen uin U.28
The nex heo em connec s syn ax and seman ics. 29
Theo em 3.2 (Hin ikka’s Lemma). E e y i s -o de Hin ikka se Hwi h espec o Uis sa is iable o e he 30
uni e se U.31
Please ci e his a icle in p ess as: K. P´
asz o Va ga, M. V´
a e ´
esz, Languages o logic and hei applica ions, Compu e s and Ma hema ics wi h
Applica ions (2007), doi:10.1016/j.camwa.2007.06.007
UNCORRECTED PROOF
CAMWA: 3975
ARTICLE IN PRESS
8K. P´
asz o Va ga, M. V´
a e ´
esz / Compu e s and Ma hema ics wi h Applica ions xx (xxxx) xxx–xxx
Acco ding o [17] he i s -o de ableau ules o he language hP,Pa ia e he ollowing:1
∀x A
Ax
a
( o any a∈Pa ), ∃x A
Ax
a
( o a c i ical a∈Pa ).2
The second ule is a o maliza ion o he nex in o mal a gumen . Suppose ha in he cou se o a p oo , we ha e3
es ablished ∃x A. Then, we can say, le abe he name o an elemen ha ing he p ope y A. He e, we can use only such4
a symbol ha has no been assigned any ole ye . Since he pa ame e s o he language hP,Pa ia e “uncommi ed”,5
a c i ical (so ha a new) one is always a ailable o his pu pose. He e, we can see he mo i a ion o in oduc ion o 6
pa ame e s o he logic language.7
The ableau ules p o ide o a ise Hin ikka se s wi h espec o he se o pa ame e s as a uni e se on he open8
b anches (b anch wi hou any complemen o mula pai ) o any inished sys ema ic ableau. The uni e se is a special9
one: he pa ame e s a e names o he uni e se elemen s again. F om he Hin ikka’s lemma we ha e a once ha in any10
inished sys ema ic ableau, e e y open b anch is sa is iable (o e his uni e se).11
In he case o he languages hP,F,Ci he i s -o de ableau ules a e gi en in he nex o m [11]12
∀x A
Ax
( o any e m ), ∃x A
Ax
y
( o a c i ical a iable y).13
An a bi a y e m is subs i u ed in o he body o a uni e sal o mula and any a iable is subs i u ed in o he body o an14
exis en ial o mula which is no ee in any o mula o he b anch which is being ex ended. The ules p o ide only, ha 15
he se o o mulae a ising on an open b anch is a Hin ikka se in hP,F,Ci. Acco ding o [11] his se is sa is iable16
o e he se o equi alence classes o e ms in oduced by ableau ules.17
4. Towa d he uni ied way o p o e comple eness18
Soundness and comple eness o a deduc ion sys em show i s sui abili y o he ea men o logic. In his case, he19
syn ac ic and seman ic cons uc ions o logic a e equi alen . The de ini ions o soundness and comple eness p ope ies20
and hei p oo s depend on he deduc ion sys em i sel .21
A deduc ion sys em is called sound, whene e i s decision p oblem is sol ed o a gi en se o o mulae, hen his22
o mula se has a special seman ic p ope y. Le us lis he soundness heo ems (H) o he Hilbe sys em, (R) o he23
esolu ion calculus and (T) o he ableau calculus.24
Theo em 4.1 (Soundness).25
(H) I a o mula A is deducible om a se So o mulae (in he Hilbe sys em), hen S|H A.26
(R) I he emp y clause has esolu ion deduc ion om a se So clauses, hen Sis unsa is iable.27
(T) I he ableau o a se So o mulae is closed, hen Sis unsa is iable.28
To p o e he soundness p ope y o a deduc ion sys em is no ha d. In e e y case, he key ac needed is he29
soundness o he deduc ion ules.30
Comple eness o a deduc ion sys em means ha i a se o o mulae has he seman ic p ope y gi en by soundness,31
hen he calculus wo ks success ully o e ha se o o mulae. The comple eness heo ems o he abo e sys ems a e32
as ollows.33
Theo em 4.2 (Comple eness).34
(H) I S|H A, hen A is deducible om S.35
(R) I a se So clauses is unsa is iable, hen he emp y clause has esolu ion deduc ion om S.36
(T) I a se So o mulae is unsa is iable, hen he ableau o Sis closed.37
By seman ics, a se o o mulae is ei he sa is iable o no . This seman ic p ope y di ides he se Ωo se s o 38
o mulae in o wo disjoin pa s. In a gi en calculus we can de ine a syn ac ic p ope y o he se s o o mulae39
di iding he se Ωin o wo disjoin pa s, as well. This is gene ally called consis ency (inconsis ency) p ope y. The40
de ini ion o he (in)consis ency p ope y depends on he deduc ion sys em.
Please ci e his a icle in p ess as: K. P´
asz o Va ga, M. V´
a e ´
esz, Languages o logic and hei applica ions, Compu e s and Ma hema ics wi h
Applica ions (2007), doi:10.1016/j.camwa.2007.06.007
UNCORRECTED PROOF
CAMWA: 3975
ARTICLE IN PRESS
K. P´
asz o Va ga, M. V´
a e ´
esz / Compu e s and Ma hema ics wi h Applica ions xx (xxxx) xxx–xxx 9
De ini ion 4.1. (H) Sis inconsis en i Aand ¬Aa e deducible om S.1
(R) A se So clauses is inconsis en i he emp y clause has esolu ion deduc ion om he se S.2
(T) The se So o mulae is inconsis en i he ableau o Sis closed. 3
I is ob ious ha , he soundness and comple eness p ope ies o a deduc ion sys em can be exp essed by he 4
(in)consis ency p ope y: soundness equi es ha i Sis inconsis en , hen Smus be unsa is iable, and comple eness 5
equi es ha i Sis unsa is iable, hen Smus be inconsis en . Then, comple eness o a deduc ion sys em is p o ed 6
by showing ha he consis ency–inconsis ency (syn ac ic) p ope ies and he sa is iabili y–unsa is iabili y (seman ic) 7
p ope ies di ide in o he same wo pa s he se Ωo se s o o mulae. 8
Le Γdeno e any p ope y o o mula se s which is o ini e cha ac e . I means ha a se Shas he p ope y Γi 9
and only i all ini e subse o Sha e he p ope y Γ.10
De ini ion 4.2. In he language L= hP,Pa i, a p ope y Γo ini e cha ac e is called an analy ic consis ency 11
p ope y o i s -o de logic i Γis an analy ic consis ency p ope y o p oposi ional logic [17], and i o e e y se 12
So o mulae o Lha ing he p ope y Γ he ollowing condi ions hold: 13
(1) I ∀x A ∈S, hen o e e y a∈Pa ,S∪ {Ax
a}has he p ope y Γ.14
(2) I ∃x A ∈S, hen S∪ {Ax
a}has he p ope y Γ, i a∈Pa does no occu in S.15
An impo an example o an analy ic consis ency p ope y is he consis ency p ope y in he ableau me hod. 16
Theo em 4.3 (Uni ying P inciple). I Γis an analy ic consis ency p ope y, Sis a se o pa ame e - ee o mulae in 17
hP,Pa i, and Shas he p ope y Γ, hen Sis sa is iable. 18
I is clea ha a se So o mulae ha ing an analy ic consis ency p ope y can be embedded in o a Hin ikka se 19
wi h espec o he se o pa ame e s as a uni e se, so i is sa is iable. 20
Consequen ly, ins ead o p o ing he di e en comple eness heo ems i is su icien o es whe he he consis ency 21
p ope y in a gi en deduc ion sys em is an analy ic consis ency p ope y. I he consis ency p ope y is an analy ic 22
consis ency p ope y, hen his ac is equi alen o he comple eness o his deduc ion sys em. By his esul we ge a 23
uni ied me hod o ea he comple eness p oblem o a deduc ion sys em in he i s -o de logic. 24
The e is ano he impo an applica ion o he uni ying p inciple. I is easily e i ied ha he ollowing p ope y Γ25
is an analy ic consis ency p ope y: Le a se So pa ame e - ee o mulae in hP,Pa iha e he p ope y Γ, i all o 26
i s ini e subse s a e sa is iable. Using Theo em 4.3, we ge he so-called compac ness heo em o i s -o de logic: I 27
e e y ini e subse o Sis sa is iable, so is S.28
5. Applica ions 29
Many applica ions o logic, mainly in he a i icial in elligence, a e ela ed o he deduc ion sys ems. In hese 30
applica ions, naming he uni e se elemen s is ine i able. To sol e a p oblem by a deduc ion sys em he ollowing 31
s eps a e execu ed. 32
(I) The i s ask is o c ea e an ideal wo ld, a ma hema ical model o he p oblem, in which he classical logic can 33
be used o eason co ec ly. (Whe he he model accu a ely e lec s he eal wo ld is a sepa a e issue.) In his 34
model we ha e a uni e se. Ou ideal wo ld is cha ac e ized by ope a ions and ela ions on his uni e se. 35
(II) The second ask is o ind a desc ip ion language o he ideal wo ld. The ex alogical pa o he alphabe consis s 36
o p edica e and unc ion symbols iden i ying he ela ions and ope a ions o he model. Fo desc ibing asse ions 37
abou uni e se elemen s, i is necessa y o in oduce cons an symbols naming hem. 38
(III) This language is sui able o o maliza ion o he o iginal p oblem. The esul o o maliza ion is o en a ini e se 39
o o mulae (p emises) and a o mula (conclusion) in he language. The hi d ask is o es whe he he conclusion 40
is a consequence o p emises. The ac ually used deduc ion sys em ies o gi e he answe wi h sol ing i s own 41
decision p oblem acco ding o he o iginal one. 42
In he case o using he esolu ion calculus ( o example in a P olog sys em) he He b and uni e se is used, 43
whe e he cons an symbols o he language a e he cons an elemen s o he He b and uni e se. I he e a e 44
unc ion symbols in he language, hen he g ound e ms a e also elemen s o he He b and uni e se. As he 45
p oblem has he o iginally ixed uni e se, hen he He b and uni e se shows an in e p e a ion o unc ion symbols 46
Please ci e his a icle in p ess as: K. P´
asz o Va ga, M. V´
a e ´
esz, Languages o logic and hei applica ions, Compu e s and Ma hema ics wi h
Applica ions (2007), doi:10.1016/j.camwa.2007.06.007