From orlowska@itl.waw.pl Mon Nov 15 19:32:33 1999 Date: Sat, 06 Nov 1999 14:25:05 +0100 From: Ewa Orlowska To: PTLiFN Subject: Sesja 26 listopada Session of the Polish Association for Logic and Philosophy of Science dedicated to the memory of Andrzej Mostowski and Helena Rasiowa Friday 26 November, 1999 National Institute of Telecommunications Szachowa 1, Warszawa-Miedzeszyn 10.45 - 11.00 Opening 11.00 - 11.30 Reflections on 'On models of axiomatic systems' (1952) Wilfrid Hodges Imperial College, London Abstract: Mostowski's paper from 1952 uses a version of the Tarski truth definition that is intermediate between Tarski's original version from around 1930 and his model-theoretic version with Vaught in the later 1950s. In the light of later developments (including the generalised quantifiers pioneered by Mostowski) one can ask whether the differences between these versions are significant, and what semantic questions the versions answer. 11.35 - 12.05 Applying certain result of A. Mostowski one can disprove a thesis of E. Engeler telling that the interpolation property holds for algorithmic logic Andrzej Salwicki Technical University of Bialystok Abstract: In a paper of Erwin Engeler dated 1970 one can find a theorem saying that logic of algorithmic properties enjoys the interpolation property. The paper does not contain a proof. The present author spent two years trying to prove the Engeler's conjecture and from time to time asked professor Mostowski for anadvice. Andrzej Mostowski was convinced that the property, also known as Crig's lemma cannot hold in algorithmic logic in spite of elegant proof of this property for logic of infinite disjunctions and conjunctions. Finally, using the techniques offered by Mostowski in his 3rd Congress of Logic, methodology and Philosophy of Sciences paper (Amsterdam, 1968) the present author found that Mostowski was right. In our talk we are going to present an application of Mostowski's method in a proof of the following theorem: The interpolation property (so called Craig's lemma) does not hold in algorithmic logic. 12.10 - 12.40 Mostowski's collapse and set constraints Leszek Pacholski Institute of Computer Science, University of Wroclaw Abstract: I shall present an application of the Mostowski collapse technique to a proof of decidability of the problems of consistency of set constraints with negation and projections. I shall also comment on how set constraints are being used for analysis and optimization of computer programs. 12.45 - 13.15 Avoiding diagonalisation in the Rosser theorem Henryk Kotlarski Mathematical Institute of the Polish Academy of Sciences, Warsaw Abstract: In the nineties several new proofs of Godel's incompleteness theorems were found. They are due to Jech, Kikuchi and the present author. More recently, Cieslinski and Adamowicz found still new proofs. In my lecture I shall sketch a proof of the following result, which is a variant of the classical Rosser's theorem (the result is published in "An addition to Rosser's theorem", Journal of Symbolic Logic 61(1), 1996, pp. 474--480). We define the quantifier rank of a formula in the natural way. We say that a proof has quantifier rank at most r if all formulas which occur in are of quantifier rank at most r. We define the inconsistency coefficient of T to be the least r such that there exists a proof of the statement 0=1 of quantifier rank r. THEOREM. Let T be a consistent, primitive recursive theory in the language of Peano Arithmetic and containing Peano Arithmetic. Then both theories: T + the inconsistency coefficient of T exists and is even T + the inconsistency coefficient of T exists and is odd are consistent. In other words, a consistent theory has nothing to say to what extent it is inconsistent. 13.20 - 13.50 On Herbrand-type consistency in weak theories Zofia Adamowicz Mathematical Institute of the Polish Academy of Sciences Pawel Zbierski Department of Mathematics of the University of Warsaw Abstract: We prove that the Goedel second incompleteness theorem holds for Herbrand consistency and a weak arithmetic. 13.55 - 15.00 Lunch break 15.00 - 15.30 T-norm-based multi-valued logics Francesc Esteva University of Barcelona Abstract: Recently different many-valued logical systems are defined to cope with the fuzzy logic defined by a t-norm and their residua. The first one is the so called BL logic defined by Hajek. It is built up from two primitive connectives (& and implication) and the truth constant 0. The conjunction is interpreted by a continuous t-norm and the implication by its residuum. Moreover min-conjunction (^) and max-disjunction (v) are definible in BL. After different attempts, finally it is proved that this logic is the logic of continuous t-norms and their residua. The most known Logical systems that are axiomatic extensions of BL are Lukasiewicz, product and Gödel Logics which standard completeness where proved previously. More recently and based on the fact that a t-norm has a residuum iff it is left continuous, a logical system corresponding to left continuous t-norms and their residua has been defined. The main difference is the fact that in this case min-conjunction is not definible and should be introduced as primitive connective. Some completeness results and standard completeness for this system and some subsystems are also studied. In the talk these basic systems will be presented joint with the corresponding algebraic counterpart (varieties of algebras) and completeness results. Moreover we will try to have a look on some special logical systems combining Lukasiewicz and Gödel Logics which has a nice standard completeness. 15.35 - 16.05 Fuzzy relational calculus for knowledge processing Etienne Kerre University of Gent Abstract: The concept of a relation is one of the most fundamental notions in pure as well as in applied sciences. Sometimes science itself has been described as the discovery of relations between objects, states, events,....Mathematically spoken, relations and in particular functional relations or shortly functions are basic concepts: how can we imagine mathematics without the use of the fundamental relations such as membership, inclusion, equality, inequality, greater than, sinus, exponential mapping, power functions....It is undeniable that the fuzzification of this fundamental notion (i.e. instead of dealing with connected or nonconnected objects one considers objects that are linked in some degree) has enriched the applicability of this notion. Due to the notions of after- and foreset introduced by Bandler and Kohout, some very important new ways of composing crisp and fuzzy relations and of imaging crisp and fuzzy sets under crisp and fuzzy relations have been introduced. They substantially increased the expressiveness of the fuzzy relational calculus, particularly for the representation and the processing of human knowledge. In this talk we will give an overview of this new machinery and show its expressive power to tackle incomplete information in several domains, among them: information retrieval, medical diagnosis, expert systems, relational databases, preference structures, ordering procedures. 16.10 - 16.40 A Decision Procedure for Proofs Visualisation Anita Wasilewska Maxim Lifantsev State University of New York at Stony Brook Laurent Vigneron LORIA, Universite Nancy 2, Abstract: We present here an approach we used for proving properties of clopen topological spaces, It combines powerful theorem provers techniques (and implementations) with a graphical technique based on a graphical representation of a rough set, called Rough Diagrams. Rough Diagrams are a generalization of a classical notion of Ven Diagrams for algebra of sets to clopen topological spaces. We use them as a powerful automated technique of constucting countermodels of properties the prover has a hard time proving and the user might suspect of being false. It means we propose to add a visual tool to a prover that after some fixed number of prover deductions would start constucting a visual countermodel for a property the prover is trying to prove. A prover with the visual tool is called a visual prover. The visual prover has a completness property: for any rough set equality we can construct its proof or its countermodel. The proof of the completness property of our visual prover consists of construction of all possible cases of rough set diagrams for a given number of sets. In order to reduce its complexity we introduce a notion of a universal rough diagram and show that the decision procedure can be defined in its terms only. 16.45 - 17.15 On the Ulam problem Wojciech Guzicki Department of Mathematics, University of Warsaw Abstract: Everybody knows "The 20 questions" game: one person thinks of an integer between 1 and n (originally1 million), another asks k yes-no questions (originally 20) and tries to guess the number. Many players also know the winning "halving" strategy. Ulam in his "Adventures of a Mathematician" asked a question how the winning strategy should change if the first player is allowed to lie once or twice. We will sketch how the answer to this question was obtained by several authors and how one should play against a liar. 17.20 - 17.50 Discernibility and Boolean Reasoning Andrzej Skowron Institute of Mathematics, University of Warsaw Abstract: A successful methodology based on the discernibility of objects and Boolean reasoning has been developed for computing of important for applications constructs like reducts and their approximations, decision rules, association rules, discretization of real value attributes, symbolic value grouping, searching for new features defined by oblique hyperplanes or higher order surfaces, pattern extraction from data. Most of the problems related to generation of the above mentioned constructs are NP-complete or NP-hard. However, it was possible to develop efficient heuristics returning suboptimal solutions of the problems. The results of experiments on many data sets are very promising. They show very good quality of solutions generated by the heuristics in comparison with other methods reported in literature (with respect to the classification quality of new objects and time necessary for computing of solutions). It is important to note that constructed heuristics have an important approximation property: expressions generated by heuristics (i.e., implicants) close to prime implicants define approximate solutions of problems. The Session will be held at the Conference Center of the National Institute of Telecommunications Warszawa-Miedzeszyn, street Szachowa 1. Transportation from the downtown Warsaw to the district Warszawa-Miedzeszyn: bus 521 from a bus stop in front of hotel Forum, get off at the stop 'Szachowa' or train from the station Warszawa-Srodmiescie, direction ^ŃEast^Ň (Kierunek wschodni) to Warszawa-Miedzeszyn -- Ewa Orlowska Institute of Telecommunications ul. Szachowa 1 04-894 Warsaw, Poland