Classical Logic II

College of Arts and Philosophy, Charles University, course syllabus

Program v LS 2011/12

21. února 2012
Přehled logické syntaxe. Důkaz a dokazatelnost, logické kalkuly, odvozovací pravidla, logické axiomy, volné a vázané výskyty proměnných, sentence. Logické a mimologické symboly. Pojem tautologie v predikátové logice. Axiomatická teorie. Teorie s axiomy Q1 a Q2 jako jednoduchý příklad teorie.
23. února 2012
Příklady na konstrukci důkazů v hilbertovském kalkulu. Dokazatelnost v teorii s axiomy Q1 a Q2, neformální důkazy. Věta o korektnosti. Platnost formule ve struktuře, splněnost formule ohodnocením ve struktuře.
Relevantní cvičení: Cvičení 3 a první část cvičení 12 ("formulujte teorii") v dílu I.
28. února 2012
Tarského definice. Platnost formule ve struktuře. Korektnost pravidla generalizace. Schéma důkazu věty o korektnosti. Prominentní struktury: struktura přirozených čísel, struktury reálných, racionálních a celých čísel. Standardní a nestandardní modely teorie s axiomy Q1 a Q2.
Relevantní cvičení: Najděte sentenci, která platí jen v jedné ze struktur <Z,+> a <Q,+>.
1. března 2012
Pojem vyplývání, logicky platné formule. Sporné a bezesporné teorie.
Relevantní cvičení: 7-9 v dílu I.
6. března 2012
Standardní a nestandardní modely teorií, jejichž jazyk obsahuje alespoň symboly pro scítání a násobení a jejichž axiomy obsahují alespoň axiomy Q1 a Q2. Standardní a nestandardní prvky v takových modelech. Numerály. Peanova a Robinsonova aritmetika. Příklady na použití axiomu indukce.
Relevantní cvičení: 10 v dílu II. Kromě toho, nalezněte formuli v aritmetickém jazyce, která říká číslo x je mocnina dvojky.
8. března 2012
Axiomatika Peanovy a Robinsonovy aritmetiky. Vztah schémat Ind a LNP. Formalizace pokročilejších pojmů a důkazů v PA, demonstrovaná na pojmu mocnina dvojky a na důkazu tvrzení, že prvočísel existuje nekonečně mnoho.
13. března 2012
Vlastnosti struktur a jejich prvků, které pravděpodobně nejsou vyjádřitelné sentencí resp. formulí. Ještě jeden příklad tvrzení dokazatelného v PA: věta o dělení se zbytkem. Konstrukce jednoduchého nestandardního modelu Robinsonovy aritmetiky, který ukazuje, že běžné vlastnosti operací a uspořádání v Q zpravidla dokazatelné nejsou.
15. března 2012
Pět schémat dokazatelných v Robinsonově aritmetice (pan Révay slíbil v úterý ukázat důkaz pátého z nich). Věta o silné úplnosti, věta o kompaktnosti a slabá verze Löwenheim-Skolemovy věty.
Relevantní cvičení: U věty o kompaktnosti si rozmyslete, jak spolu souvisejí obě formulace.
20. března 2012
Vaughtův test, jeho použití k důkazu úplnosti teorie DNO.
Relevantní cvičení: 18 a 20 v dílu I.
22. března 2012
Eliminace kvantifikátorů pro teorii SUCC.
27. března 2012
Eliminace kvantifikátorů, dokončení. Zmínka o důležitých teoríích umožňujících eliminaci kvantifikátorů: Presburgerova aritmetika, teorie reálných čísel.
29. března 2012
Existence a struktura nestandardního modelu Peanovy aritmetiky. Axiomatizovatelné a konečně axiomatizovatelné třídy struktur. Věta o kompaktnosti jako nástroj pro prokazování neaxiomatizovatelnosti určitých tříd struktur: třída všech konečných struktur pro nejvýše spočetný jazyk L, třída všech silně souvislých orientovaných grafů.
Relevantní cvičení: 13 a 14 v dílu I.
3. dubna 2012
Rekurzívně axiomatizovatelné teorie. Rozhodnutelné a nerozhodnutelné teorie. Craigův trik. Rozhodnutelnost konečného rozšíření rozhodnutelné teorie.
Relevantní cvičení: Uvažujte teorii S podobnou teorii teorii DNO až na to, že axiom neexistuje největší objekt je nahrazen jeho negací (axiom neexistuje nejmenší objekt zůstává beze změny). Zdůvodněte pomocí Vaughtova testu, že S je úplná teorie. Dále zdůvodněte, že teorie T, která vznikne z DNO či z S odstraněním axiomu o neexistenci resp. existenci největšího objektu, je příkladem neúplné avšak rozhodnutelné teorie.
5. dubna 2012
Hierarchie aritmetických formulí: Δ0-formule, Σ-formule, Σn- a Πn-formule. Pojem definovatené množiny (relace).
10. dubna 2012
Definovatelnost ve struktuře přirozených čísel. Definovatelné množiny a souvislost s eliminací kvantifikátorů.
12. dubna 2012
Kódování pomocí dvou pravítek. Definovatelnosti rekurzívně spočetných množin. Aritmetické a nearitmetické množiny. Zjednodušená verze První Gödelovy věty: je-li T teorie v aritmetickém jazyce taková, že N je její model, pak T je neúplná.
17. dubna 2012
Věta o Σ-úplnosti Robinsonovy aritmetiky. První Gödelova věta o neúplnosti.
19. dubna 2012
Důkaz První Gödelovy věty o neúplnosti. Rosserova věta, podstatná část důkazu.
Relevantní cvičení: cvičení 15-17 v dílu II se týkají Σ-úplnosti.
24. dubna 2012
Dokončení důkazu Rosserovy věty. Aritmetizace logické syntaxe, formalizace dokazatelnosti a bezespornosti v Peanově aritmetice.
26. dubna 2012
(Löbovy) podmínky pro dokazatelnost. Druhá Gödelova věta o neúplnosti.
3. května 2012
Poznámky ke Druhé Gödelově větě: souvislost s Hilbertovým programem, souvislost s modální logikou. Sentence vyjadřující bezespornost jako konkrétní příklad nezávislé sentence. Pravidla gentzenovského kalkulu pro klasickou výrokovou logiku. Pojmy: sekvent, antecedent, sukcedent, důkaz formule, bezřezový důkaz, subformula property. Iniciální sekvent, finální sekvent, formule principální, postranní, vstupní.
10. května 2012
Korektnost a úplnost gentzenovského kalkulu pro klasickou výrokovou logiku.
15. května 2012
Intuicionistická logika, kripkovská sémantika její výrokové varianty.
17. května 2012
Konstrukce kripkovských modelů. Disjunction property. Gentzenovský (multisukcedentový) kalkulus pro intuicionistickou výrokovou logiku, jeho korektnost. Důkaz (trochu nekompletní) věty o úplnosti pro tento kalkulus, zhruba dle cvičení 25 oddílu 5.1 knihy (str. 393).

Summary

This course is intended for students who already had an introductory courses of logic and of recursion theory. The following knowledge is assumed: syntax and semantics of classical propositional and predicate logic (with equality), Hilbert-style logical calculus, the deduction theorem. Completeness and compactness theorems. Recursive and recursively enumerable sets. Post's theorem, m-reducibility, m-completeness.

Grades and Exams

Požadavky ke zkoušce jsou dány následujícím sylabem, navíc je třeba předložit seznam nejméně dvaceti sedmi vyřešených cvičení z celkem tří dílů, viz soubory cvlog1, cvlog2 a cvlog3 dole. Soubor cvlog3 obsahuje sylabus stejný jako ten, který následuje, avšak v češtině.

Theories, Models, Compactness, Completeness

This part roughly follows J. Barwise's introduction to the Handbook of Mathematical Logic (chapter A1, pp. 5-46). Examples requiring deeper knowledge of algebra (fields, ideals) are omitted. Other examples are added: natural numbers with zero and the successor function allow the quantifier elimination. The theory of dense linear ordering without end elements is another example of a complete theory. The following topics are discussed: language (as a list of non-logical symbols), axioms (of a calculus, or logical axioms of a theory), semantical consequence, formal proof, contradictory and consistent theories, complete and incomplete theories, decidable and undecidable theories, theory of a structure. Some consequences of the compactness theorem: impossibility of finite axiomatization of some theories, non-axiomatizability of some classes of structures.

Robinson's and Peano arithmetic

Robinson's arithmetic is incomplete. There exists a simple structure for the arithmetical language showing that universal formulas (e.g. commutativity of addition) "usually" are not provable in Robinson's arithmetic. On the other hand, all "common facts" about natural numbers are provable in Peano arithmetic using induction. Peano arithmetic also has non-standard models. Relevant notions: arithmetical language, numerals, standard and non-standard models, hierarchy of arithmetical formulas, connection to the arithmetical hierarchy in the algorithmical sense. For the incompleteness theorems the following results are essential: Sigma-completeness of Robinson's arithmetic, recursiveness of logical syntax and definability of all RE sets in the standard model of arithmetic. The latter is a more difficult technical result that depends on definability of appropriate coding of sequences.

Incompleteness in arithmetic

Every sound recursively axiomatizable extension of Robinson's arithmetic is incomplete and undecidable (Gödel's 1st incompleteness theorem). Also, the predicate calculus e.g. in arithmetical language or in the language of set theory is undecidable. Using effectively recursively enumerable sets (or effectively non-recursive sets) one can replace the assumption of soundness in Gödel's 1st incompleteness theorem by an assumption of mere consistency; this is the Rosser's generalisation. The Self-reference Theorem (Gödel diagonal lemma) is based on a rather technical result about weak representability of primitive recursive functions. It yields e.g. an alternative (and a classical one) proof of Gödel's 1st incompleteness theorem or further the theorem on undefinability (in the standard model of arithmetic) of the set of all true arithmetical sentences. In Peano arithmetic one can formalize coding of finite sequences, which gives formalisation of logical syntax. No recursively axiomatizable consistent extension of Peano arithmetic can prove its own consistency - this is the celebrated Gödel's 2nd incompleteness theorem. The sentence expressing consistency is a concrete example of a true and unprovable sentence. Gödel's 2nd incompleteness is interesting also from the historical and philosophical point of view (Hilbert's programme).

Gentzen Sequent Calculi

Gentzen sequent calculi can be used to obtain deeper results about provability in Peano arithmetic (e.g. that Peano arithmetic is not finitely axiomatizable) but they are interesting irrespective of other fields. Brief introduction to intuitionistic logic is included because the intuitionistic calculus can be obtained from the classical one by only a small modification and in relevant books (Kleene, Takeuti) both calculi are discussed simultaneously. This part of the course hopefully also throws some more light on the concept of soundness and completeness of calculi in general. The philosophical and historical importance of intuitionistic logic is not discussed. Related notions: sequent, antecedent, succedent, Kripke model.

References

  • J Barwise (ed.), Handbook of Mathematical Logic, North-Holland, 1977
  • P Hájek, P Pudlák, Metamathematics of First Order Arithmetic, Springer, 1993
  • P Hájek, V Švejdar, Matematická logika
  • S C Kleene, Introduction to Metamathematics, D van Nostrand, 1952
  • P Odifreddi, Classical Recursion Theory, North-Holland, Amsterdam, 1989
  • H Schwichtenberg, Proof Theory, chapter D2 in the Handbook above, pp. 867--896
  • C Smorynski, The incompleteness theorems, chapter D1 in the Handbook above, pp. 819--843
  • C Smorynski, Hilbert's programme, CWI Quarterly 1,4, 1988
  • G Takeuti, Proof Theory, North-Holland, Amsterdam, 1975
  • V Švejdar, Logika: neúplnost, složitost a nutnost, Academia, Praha 2002
  • A Tarski, A Mostowski, R M Robinson, Undecidable Theories, North-Holland, Amsterdam, 1953

Download
My home page Dept. of Logic Charles University


Updated: by Vitezslav Svejdar