
In mathematics and philosophy, Łukasiewicz logic (/ˌwʊkəˈʃɛvɪtʃ/ WUUK-ə-SHEV-itch, Polish: [wukaˈɕɛvitʂ]) is a non-classical, many-valued logic. It was originally defined in the early 20th century by Jan Łukasiewicz as a three-valued modal logic; it was later generalized to n-valued (for all finite n) as well as infinitely-many-valued (ℵ0-valued) variants, both propositional and first order. The ℵ0-valued version was published in 1930 by Łukasiewicz and Alfred Tarski; consequently it is sometimes called the Łukasiewicz–Tarski logic. It belongs to the classes of t-norm fuzzy logics and substructural logics.
Łukasiewicz logic was motivated by Aristotle's suggestion that bivalent logic was not applicable to future contingents, e.g. the statement "There will be a sea battle tomorrow". In other words, statements about the future were neither true nor false, but an intermediate value could be assigned to them, to represent their possibility of becoming true in the future.
This article presents the Łukasiewicz(–Tarski) logic in its full generality, i.e. as an infinite-valued logic. For an elementary introduction to the three-valued instantiation Ł3, see three-valued logic.
Language
The propositional connectives of Łukasiewicz logic are ("implication"), and the constant
("false"). Additional connectives can be defined in terms of these:
The and
connectives are called weak disjunction and conjunction, because they are non-classical, as the law of excluded middle does not hold for them. In the context of substructural logics, they are called additive connectives. They also correspond to lattice min/max connectives.
In terms of substructural logics, there are also strong or multiplicative disjunction and conjunction connectives, although these are not part of Łukasiewicz's original presentation:
There are also defined modal operators, using the :
Axioms
This section needs expansion with: additional axioms for finite-valued logics. You can help by adding to it. (August 2014) |
The original system of axioms for propositional infinite-valued Łukasiewicz logic used implication and negation as the primitive connectives, along with modus ponens:
Propositional infinite-valued Łukasiewicz logic can also be axiomatized by adding the following axioms to the axiomatic system of monoidal t-norm logic:
- Divisibility
- Double negation
That is, infinite-valued Łukasiewicz logic arises by adding the axiom of double negation to basic fuzzy logic (BL), or by adding the axiom of divisibility to the logic IMTL.
Finite-valued Łukasiewicz logics require additional axioms.
Proof Theory
This section needs expansion with: discussion of sequent calculi and natural deduction systems needed. You can help by adding to it. (June 2022) |
A hypersequent calculus for three-valued Łukasiewicz logic was introduced by Arnon Avron in 1991.
Sequent calculi for finite and infinite-valued Łukasiewicz logics as an extension of linear logic were introduced by A. Prijatelj in 1994. However, these are not cut-free systems.
Hypersequent calculi for Łukasiewicz logics were introduced by A. Ciabattoni et al in 1999. However, these are not cut-free for finite-valued logics.
A labelled tableaux system was introduced by Nicola Olivetti in 2003.
A hypersequent calculus for infinite-valued Łukasiewicz logic was introduced by George Metcalfe in 2004.
Real-valued semantics
Infinite-valued Łukasiewicz logic is a real-valued logic in which sentences from sentential calculus may be assigned a truth value of not only 0 or 1 but also any real number in between (e.g. 0.25). Valuations have a recursive definition where:
for a binary connective
and
and where the definitions of the operations hold as follows:
- Implication:
- Equivalence:
- Negation:
- Weak conjunction:
- Weak disjunction:
- Strong conjunction:
- Strong disjunction:
- Modal functions:
The truth function of strong conjunction is the Łukasiewicz t-norm and the truth function
of strong disjunction is its dual t-conorm. Obviously,
and
, so if
, then
while the respective logically-equivalent propositions have
.
The truth function is the residuum of the Łukasiewicz t-norm. All truth functions of the basic connectives are continuous.
By definition, a formula is a tautology of infinite-valued Łukasiewicz logic if it evaluates to 1 under each valuation of propositional variables by real numbers in the interval [0, 1].
Finite-valued and countable-valued semantics
Using exactly the same valuation formulas as for real-valued semantics Łukasiewicz (1922) also defined (up to isomorphism) semantics over
- any finite set of cardinality n ≥ 2 by choosing the domain as { 0, 1/(n − 1), 2/(n − 1), ..., 1 }
- any countable set by choosing the domain as { p/q | 0 ≤ p ≤ q where p is a non-negative integer and q is a positive integer }.
General algebraic semantics
The standard real-valued semantics determined by the Łukasiewicz t-norm is not the only possible semantics of Łukasiewicz logic. General algebraic semantics of propositional infinite-valued Łukasiewicz logic is formed by the class of all MV-algebras. The standard real-valued semantics is a special MV-algebra, called the standard MV-algebra.
Like other t-norm fuzzy logics, propositional infinite-valued Łukasiewicz logic enjoys completeness with respect to the class of all algebras for which the logic is sound (that is, MV-algebras) as well as with respect to only linear ones. This is expressed by the general, linear, and standard completeness theorems:
- The following conditions are equivalent:
is provable in propositional infinite-valued Łukasiewicz logic
is valid in all MV-algebras (general completeness)
is valid in all linearly ordered MV-algebras (linear completeness)
is valid in the standard MV-algebra (standard completeness).
Here valid means necessarily evaluates to 1.
Font, Rodriguez and Torrens introduced in 1984 the Wajsberg algebra as an alternative model for the infinite-valued Łukasiewicz logic.
A 1940s attempt by Grigore Moisil to provide algebraic semantics for the n-valued Łukasiewicz logic by means of his Łukasiewicz–Moisil (LM) algebra (which Moisil called Łukasiewicz algebras) turned out to be an incorrect model for n ≥ 5. This issue was made public by Alan Rose in 1956. C. C. Chang's MV-algebra, which is a model for the ℵ0-valued (infinitely-many-valued) Łukasiewicz–Tarski logic, was published in 1958. For the axiomatically more complicated (finite) n-valued Łukasiewicz logics, suitable algebras were published in 1977 by Revaz Grigolia and called MVn-algebras. MVn-algebras are a subclass of LMn-algebras, and the inclusion is strict for n ≥ 5. In 1982 Roberto Cignoli published some additional constraints that added to LMn-algebras produce proper models for n-valued Łukasiewicz logic; Cignoli called his discovery proper Łukasiewicz algebras.
Complexity
Łukasiewicz logics are co-NP complete.
Modal Logic
Łukasiewicz logics can be seen as modal logics, a type of logic that addresses possibility, using the defined operators,
A third doubtful operator has been proposed, .
From these we can prove the following theorems, which are common axioms in many modal logics:
We can also prove distribution theorems on the strong connectives:
However, the following distribution theorems also hold:
In other words, if , then
, which is counter-intuitive. However, these controversial theorems have been defended as a modal logic about future contingents by A. N. Prior. Notably,
.
References
- Łukasiewicz J., 1920, O logice trójwartościowej (in Polish). Ruch filozoficzny 5:170–171. English translation: On three-valued logic, in L. Borkowski (ed.), Selected works by Jan Łukasiewicz, North–Holland, Amsterdam, 1970, pp. 87–88. ISBN 0-7204-2252-3
- Hay, L.S., 1963, Axiomatization of the infinite-valued predicate calculus. Journal of Symbolic Logic 28:77–86.
- Lavinia Corina Ciungu (2013). Non-commutative Multiple-Valued Logic Algebras. Springer. p. vii. ISBN 978-3-319-01589-7. citing Łukasiewicz, J., Tarski, A.: Untersuchungen über den Aussagenkalkül. Comp. Rend. Soc. Sci. et Lettres Varsovie Cl. III 23, 30–50 (1930).
- Hájek P., 1998, Metamathematics of Fuzzy Logic. Dordrecht: Kluwer.
- Ono, H., 2003, "Substructural logics and residuated lattices — an introduction". In F.V. Hendricks, J. Malinowski (eds.): Trends in Logic: 50 Years of Studia Logica, Trends in Logic 20: 177–212.
- A. Avron, "Natural 3-valued Logics– Characterization and Proof Theory", Journal of Symbolic Logic 56(1), doi:10.2307/2274919
- A. Prijateli, "Bounded contraction and Gentzen-style formulation of Łukasiewicz logics", Studia Logica 57: 437-456, 1996
- A. Ciabattoni, D.M. Gabbay, N. Olivetti, "Cut-free proof systems for logics of weak excluded middle" Soft Computing 2 (1999) 147—156
- N. Olivetti, "Tableaux for Łukasiewicz Infinite-valued Logic", Studia Logica volume 73, pages 81–111 (2003)
- D. Gabbay and G. Metcalfe and N. Olivetti, "Hypersequents and Fuzzy Logic", Revista de la Real Academia de Ciencias 98 (1), pages 113-126 (2004).
- http://journal.univagora.ro/download/pdf/28.pdf citing J. M. Font, A. J. Rodriguez, A. Torrens, Wajsberg Algebras, Stochastica, VIII, 1, 5-31, 1984
- Lavinia Corina Ciungu (2013). Non-commutative Multiple-Valued Logic Algebras. Springer. pp. vii–viii. ISBN 978-3-319-01589-7. citing Grigolia, R.S.: "Algebraic analysis of Lukasiewicz-Tarski’s n-valued logical systems". In: Wójcicki, R., Malinkowski, G. (eds.) Selected Papers on Lukasiewicz Sentential Calculi, pp. 81–92. Polish Academy of Sciences, Wroclav (1977)
- Iorgulescu, A.: Connections between MVn-algebras and n-valued Łukasiewicz–Moisil algebras Part I. Discrete Mathematics 181, 155–177 (1998) doi:10.1016/S0012-365X(97)00052-6
- R. Cignoli, Proper n-Valued Łukasiewicz Algebras as S-Algebras of Łukasiewicz n-Valued Propositional Calculi, Studia Logica, 41, 1982, 3-16, doi:10.1007/BF00373490
- A. Ciabattoni, M. Bongini and F. Montagna, Proof Search and Co-NP Completeness for Many-Valued Logics. Fuzzy Sets and Systems.
- "Modal Logic: Contemporary View | Internet Encyclopedia of Philosophy". Retrieved 2024-05-03.
- Clarence Irving Lewis and Cooper Harold Langford. Symbolic Logic. Dover, New York, second edition, 1959.
- Robert Bull and Krister Segerberg. Basic modal logic. In Dov M. Gabbay and Franz Guenthner, editors, Handbook of Philosophical Logic, volume 2. D. Reidel Publishing Company, Lancaster, 1986
- Alasdair Urquhart. An interpretation of many-valued logic. Zeitschr. f. math. Logik und Grundlagen d. Math., 19:111–114, 1973.
- A.N. Prior. Three-valued logic and future contingents. 3(13):317–26, October 1953.
Further reading
- Rose, A.: 1956, Formalisation du Calcul Propositionnel Implicatif ℵ0 Valeurs de Łukasiewicz, C. R. Acad. Sci. Paris 243, 1183–1185.
- Rose, A.: 1978, Formalisations of Further ℵ0-Valued Łukasiewicz Propositional Calculi, Journal of Symbolic Logic 43(2), 207–210. doi:10.2307/2272818
- Cignoli, R., “The algebras of Lukasiewicz many-valued logic - A historical overview,” in S. Aguzzoli et al.(Eds.), Algebraic and Proof-theoretic Aspects of Non-classical Logics, LNAI 4460, Springer, 2007, 69-83. doi:10.1007/978-3-540-75939-3_5
In mathematics and philosophy Lukasiewicz logic ˌ w ʊ k e ˈ ʃ ɛ v ɪ tʃ WUUK e SHEV itch Polish wukaˈɕɛvitʂ is a non classical many valued logic It was originally defined in the early 20th century by Jan Lukasiewicz as a three valued modal logic it was later generalized to n valued for all finite n as well as infinitely many valued ℵ0 valued variants both propositional and first order The ℵ0 valued version was published in 1930 by Lukasiewicz and Alfred Tarski consequently it is sometimes called the Lukasiewicz Tarski logic It belongs to the classes of t norm fuzzy logics and substructural logics Lukasiewicz logic was motivated by Aristotle s suggestion that bivalent logic was not applicable to future contingents e g the statement There will be a sea battle tomorrow In other words statements about the future were neither true nor false but an intermediate value could be assigned to them to represent their possibility of becoming true in the future This article presents the Lukasiewicz Tarski logic in its full generality i e as an infinite valued logic For an elementary introduction to the three valued instantiation L3 see three valued logic LanguageThe propositional connectives of Lukasiewicz logic are displaystyle rightarrow implication and the constant displaystyle bot false Additional connectives can be defined in terms of these A defA A B def A B BA B def A B A B def A B B A def displaystyle begin aligned neg A amp def A rightarrow bot A vee B amp def A rightarrow B rightarrow B A wedge B amp def neg neg A vee neg B A leftrightarrow B amp def A rightarrow B wedge B rightarrow A top amp def bot rightarrow bot end aligned The displaystyle vee and displaystyle wedge connectives are called weak disjunction and conjunction because they are non classical as the law of excluded middle does not hold for them In the context of substructural logics they are called additive connectives They also correspond to lattice min max connectives In terms of substructural logics there are also strong or multiplicative disjunction and conjunction connectives although these are not part of Lukasiewicz s original presentation A B def A BA B def A B displaystyle begin aligned A oplus B amp def neg A rightarrow B A otimes B amp def neg A rightarrow neg B end aligned There are also defined modal operators using the A def A A A def A displaystyle begin aligned Diamond A amp def neg A rightarrow A Box A amp def neg Diamond neg A end aligned AxiomsThis section needs expansion with additional axioms for finite valued logics You can help by adding to it August 2014 The original system of axioms for propositional infinite valued Lukasiewicz logic used implication and negation as the primitive connectives along with modus ponens A B A A B B C A C A B B B A A B A A B displaystyle begin aligned A amp rightarrow B rightarrow A A rightarrow B amp rightarrow B rightarrow C rightarrow A rightarrow C A rightarrow B rightarrow B amp rightarrow B rightarrow A rightarrow A neg B rightarrow neg A amp rightarrow A rightarrow B end aligned Propositional infinite valued Lukasiewicz logic can also be axiomatized by adding the following axioms to the axiomatic system of monoidal t norm logic Divisibility A B A A B displaystyle A wedge B rightarrow A otimes A rightarrow B Double negation A A displaystyle neg neg A rightarrow A That is infinite valued Lukasiewicz logic arises by adding the axiom of double negation to basic fuzzy logic BL or by adding the axiom of divisibility to the logic IMTL Finite valued Lukasiewicz logics require additional axioms Proof TheoryThis section needs expansion with discussion of sequent calculi and natural deduction systems needed You can help by adding to it June 2022 A hypersequent calculus for three valued Lukasiewicz logic was introduced by Arnon Avron in 1991 Sequent calculi for finite and infinite valued Lukasiewicz logics as an extension of linear logic were introduced by A Prijatelj in 1994 However these are not cut free systems Hypersequent calculi for Lukasiewicz logics were introduced by A Ciabattoni et al in 1999 However these are not cut free for n gt 3 displaystyle n gt 3 finite valued logics A labelled tableaux system was introduced by Nicola Olivetti in 2003 A hypersequent calculus for infinite valued Lukasiewicz logic was introduced by George Metcalfe in 2004 Real valued semanticsInfinite valued Lukasiewicz logic is a real valued logic in which sentences from sentential calculus may be assigned a truth value of not only 0 or 1 but also any real number in between e g 0 25 Valuations have a recursive definition where w 8 ϕ F w 8 w ϕ displaystyle w theta circ phi F circ w theta w phi for a binary connective displaystyle circ w 8 F w 8 displaystyle w neg theta F neg w theta w 0 0 displaystyle w left overline 0 right 0 and w 1 1 displaystyle w left overline 1 right 1 and where the definitions of the operations hold as follows Implication F x y min 1 1 x y displaystyle F rightarrow x y min 1 1 x y Equivalence F x y 1 x y displaystyle F leftrightarrow x y 1 x y Negation F x 1 x displaystyle F neg x 1 x Weak conjunction F x y min x y displaystyle F wedge x y min x y Weak disjunction F x y max x y displaystyle F vee x y max x y Strong conjunction F x y max 0 x y 1 displaystyle F otimes x y max 0 x y 1 Strong disjunction F x y min 1 x y displaystyle F oplus x y min 1 x y Modal functions F x min 1 2x F x max 0 2x 1 displaystyle F Diamond x min 1 2x F Box x max 0 2x 1 The truth function F displaystyle F otimes of strong conjunction is the Lukasiewicz t norm and the truth function F displaystyle F oplus of strong disjunction is its dual t conorm Obviously F 5 5 0 displaystyle F otimes 5 5 0 and F 5 5 1 displaystyle F oplus 5 5 1 so if T p 5 displaystyle T p 5 then T p p T p p 0 displaystyle T p wedge p T neg p wedge neg p 0 while the respective logically equivalent propositions have T p p T p p 1 displaystyle T p vee p T neg p vee neg p 1 The truth function F displaystyle F rightarrow is the residuum of the Lukasiewicz t norm All truth functions of the basic connectives are continuous By definition a formula is a tautology of infinite valued Lukasiewicz logic if it evaluates to 1 under each valuation of propositional variables by real numbers in the interval 0 1 Finite valued and countable valued semanticsUsing exactly the same valuation formulas as for real valued semantics Lukasiewicz 1922 also defined up to isomorphism semantics over any finite set of cardinality n 2 by choosing the domain as 0 1 n 1 2 n 1 1 any countable set by choosing the domain as p q 0 p q where p is a non negative integer and q is a positive integer General algebraic semanticsThe standard real valued semantics determined by the Lukasiewicz t norm is not the only possible semantics of Lukasiewicz logic General algebraic semantics of propositional infinite valued Lukasiewicz logic is formed by the class of all MV algebras The standard real valued semantics is a special MV algebra called the standard MV algebra Like other t norm fuzzy logics propositional infinite valued Lukasiewicz logic enjoys completeness with respect to the class of all algebras for which the logic is sound that is MV algebras as well as with respect to only linear ones This is expressed by the general linear and standard completeness theorems The following conditions are equivalent A displaystyle A is provable in propositional infinite valued Lukasiewicz logic A displaystyle A is valid in all MV algebras general completeness A displaystyle A is valid in all linearly ordered MV algebras linear completeness A displaystyle A is valid in the standard MV algebra standard completeness Here valid means necessarily evaluates to 1 Font Rodriguez and Torrens introduced in 1984 the Wajsberg algebra as an alternative model for the infinite valued Lukasiewicz logic A 1940s attempt by Grigore Moisil to provide algebraic semantics for the n valued Lukasiewicz logic by means of his Lukasiewicz Moisil LM algebra which Moisil called Lukasiewicz algebras turned out to be an incorrect model for n 5 This issue was made public by Alan Rose in 1956 C C Chang s MV algebra which is a model for the ℵ0 valued infinitely many valued Lukasiewicz Tarski logic was published in 1958 For the axiomatically more complicated finite n valued Lukasiewicz logics suitable algebras were published in 1977 by Revaz Grigolia and called MVn algebras MVn algebras are a subclass of LMn algebras and the inclusion is strict for n 5 In 1982 Roberto Cignoli published some additional constraints that added to LMn algebras produce proper models for n valued Lukasiewicz logic Cignoli called his discovery proper Lukasiewicz algebras ComplexityLukasiewicz logics are co NP complete Modal LogicLukasiewicz logics can be seen as modal logics a type of logic that addresses possibility using the defined operators A def A A A def A displaystyle begin aligned Diamond A amp def neg A rightarrow A Box A amp def neg Diamond neg A end aligned A third doubtful operator has been proposed A defA A displaystyle odot A def A leftrightarrow neg A From these we can prove the following theorems which are common axioms in many modal logics A A A AA A A A B A B A B A B displaystyle begin aligned A amp rightarrow Diamond A Box A amp rightarrow A A amp rightarrow A rightarrow Box A Box A rightarrow B amp rightarrow Box A rightarrow Box B Box A rightarrow B amp rightarrow Diamond A rightarrow Diamond B end aligned We can also prove distribution theorems on the strong connectives A B A B A B A B A B A B A B A B displaystyle begin aligned Box A otimes B amp leftrightarrow Box A otimes Box B Diamond A oplus B amp leftrightarrow Diamond A oplus Diamond B Diamond A otimes B amp rightarrow Diamond A otimes Diamond B Box A oplus Box B amp rightarrow Box A oplus B end aligned However the following distribution theorems also hold A B A B A B A B A B A B A B A B displaystyle begin aligned Box A vee Box B amp leftrightarrow Box A vee B Box A wedge Box B amp leftrightarrow Box A wedge B Diamond A vee Diamond B amp leftrightarrow Diamond A vee B Diamond A wedge Diamond B amp leftrightarrow Diamond A wedge B end aligned In other words if A A displaystyle Diamond A wedge Diamond neg A then A A displaystyle Diamond A wedge neg A which is counter intuitive However these controversial theorems have been defended as a modal logic about future contingents by A N Prior Notably A A A displaystyle Diamond A wedge Diamond neg A leftrightarrow odot A ReferencesLukasiewicz J 1920 O logice trojwartosciowej in Polish Ruch filozoficzny 5 170 171 English translation On three valued logic in L Borkowski ed Selected works by Jan Lukasiewicz North Holland Amsterdam 1970 pp 87 88 ISBN 0 7204 2252 3 Hay L S 1963 Axiomatization of the infinite valued predicate calculus Journal of Symbolic Logic 28 77 86 Lavinia Corina Ciungu 2013 Non commutative Multiple Valued Logic Algebras Springer p vii ISBN 978 3 319 01589 7 citing Lukasiewicz J Tarski A Untersuchungen uber den Aussagenkalkul Comp Rend Soc Sci et Lettres Varsovie Cl III 23 30 50 1930 Hajek P 1998 Metamathematics of Fuzzy Logic Dordrecht Kluwer Ono H 2003 Substructural logics and residuated lattices an introduction In F V Hendricks J Malinowski eds Trends in Logic 50 Years of Studia Logica Trends in Logic 20 177 212 A Avron Natural 3 valued Logics Characterization and Proof Theory Journal of Symbolic Logic 56 1 doi 10 2307 2274919 A Prijateli Bounded contraction and Gentzen style formulation of Lukasiewicz logics Studia Logica 57 437 456 1996 A Ciabattoni D M Gabbay N Olivetti Cut free proof systems for logics of weak excluded middle Soft Computing 2 1999 147 156 N Olivetti Tableaux for Lukasiewicz Infinite valued Logic Studia Logica volume 73 pages 81 111 2003 D Gabbay and G Metcalfe and N Olivetti Hypersequents and Fuzzy Logic Revista de la Real Academia de Ciencias 98 1 pages 113 126 2004 http journal univagora ro download pdf 28 pdf citing J M Font A J Rodriguez A Torrens Wajsberg Algebras Stochastica VIII 1 5 31 1984 Lavinia Corina Ciungu 2013 Non commutative Multiple Valued Logic Algebras Springer pp vii viii ISBN 978 3 319 01589 7 citing Grigolia R S Algebraic analysis of Lukasiewicz Tarski s n valued logical systems In Wojcicki R Malinkowski G eds Selected Papers on Lukasiewicz Sentential Calculi pp 81 92 Polish Academy of Sciences Wroclav 1977 Iorgulescu A Connections between MVn algebras and n valued Lukasiewicz Moisil algebras Part I Discrete Mathematics 181 155 177 1998 doi 10 1016 S0012 365X 97 00052 6 R Cignoli Proper n Valued Lukasiewicz Algebras as S Algebras of Lukasiewicz n Valued Propositional Calculi Studia Logica 41 1982 3 16 doi 10 1007 BF00373490 A Ciabattoni M Bongini and F Montagna Proof Search and Co NP Completeness for Many Valued Logics Fuzzy Sets and Systems Modal Logic Contemporary View Internet Encyclopedia of Philosophy Retrieved 2024 05 03 Clarence Irving Lewis and Cooper Harold Langford Symbolic Logic Dover New York second edition 1959 Robert Bull and Krister Segerberg Basic modal logic In Dov M Gabbay and Franz Guenthner editors Handbook of Philosophical Logic volume 2 D Reidel Publishing Company Lancaster 1986 Alasdair Urquhart An interpretation of many valued logic Zeitschr f math Logik und Grundlagen d Math 19 111 114 1973 A N Prior Three valued logic and future contingents 3 13 317 26 October 1953 Further readingRose A 1956 Formalisation du Calcul Propositionnel Implicatif ℵ0 Valeurs de Lukasiewicz C R Acad Sci Paris 243 1183 1185 Rose A 1978 Formalisations of Further ℵ0 Valued Lukasiewicz Propositional Calculi Journal of Symbolic Logic 43 2 207 210 doi 10 2307 2272818 Cignoli R The algebras of Lukasiewicz many valued logic A historical overview in S Aguzzoli et al Eds Algebraic and Proof theoretic Aspects of Non classical Logics LNAI 4460 Springer 2007 69 83 doi 10 1007 978 3 540 75939 3 5