Logika dla informatyków/Ćwiczenia 11

Z Studia Informatyczne
< Logika dla informatyków
Wersja z dnia 13:05, 1 paź 2006 autorstwa Przemo (dyskusja | edycje)
(różn.) ← poprzednia wersja | przejdź do aktualnej wersji (różn.) | następna wersja → (różn.)
Przejdź do nawigacjiPrzejdź do wyszukiwania

Ćwiczenie 1

Twierdzenie o niedefiniowalności dobrego porządku w logice pierwszego rzędu udowodniliśmy dwukrotnie. Po raz pierwszy było to Ćwiczenie Uzupelnic c| do Rozdziału Uzupelnic EF|, po raz drugi Twierdzenie Uzupelnic nie-dobry|. Który z rozważanych dowodów dostarcza więcej informacji i dlaczego?

  1. Podać konstrukcje dla następujących formuł:
    1. ;
    2. ;
    3. ;
    4. ;
    5. Parser nie mógł rozpoznać (nieznana funkcja „\oto”): {\displaystyle \displaystyle \neg(p\vee q) \oto (\neg p\wedge \neg q)} ;
    6. ;
    7. .
  2. Udowodnić, że formuły z Ćwiczenia Uzupelnic szust| są twierdzeniami

intuicjonistycznymi.

  1. Udowodnić część "tylko wtedy" Twierdzenia Uzupelnic zwawo|.
  2. Udowodnić, że następujące klasyczne tautologie nie są

twierdzeniami intuicjonistycznymi, odwołując się do semantyki topologicznej.

    1. ;
    2. Parser nie mógł rozpoznać (nieznana funkcja „\oto”): {\displaystyle \displaystyle \neg(p\wedge q) \oto (\neg p\vee \neg q)} ;
    3. ;
    4. ;
    5. ;
    6. ;
    7. .

Czy istnieją zamknięte lambda-termy następujących typów?

    1. ;
    2. ;
    3. ;
    4. ;
    5. .