Logika dla informatyków/Ćwiczenia 11

Z Studia Informatyczne
< Logika dla informatyków
Wersja z dnia 19:48, 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 4 do Rozdziału 4, po raz drugi Twierdzenie 8.8. Który z rozważanych dowodów dostarcza więcej informacji i dlaczego?

Ćwiczenie 2

Podać konstrukcje dla następujących formuł:

;
;
;
;
;
;
.

Ćwiczenie 3

Udowodnić, że formuły z Ćwiczenia 2 są twierdzeniami intuicjonistycznymi.

Ćwiczenie 4

Udowodnić część "tylko wtedy" Twierdzenia 11.5.

Ćwiczenie 5

Udowodnić, że następujące klasyczne tautologie nie są twierdzeniami intuicjonistycznymi, odwołując się do semantyki topologicznej.

;
;
;
;
;
;
.

Ćwiczenie 6

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

;
;
;
;
.