Logika dla informatyków/Ćwiczenia 11

Ć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ł:

$(a)\mathrm{\perp }\to p$;

$(b)(p\to q\to r)\to (p\to q)\to p\to r$;

$(c)\mathrm{\neg }\mathrm{\neg }\mathrm{\neg }p\to \mathrm{\neg }p$;

$(d)(p\to q)\to (\mathrm{\neg }q\to \mathrm{\neg }p)$;

$(e)\mathrm{\neg }(p\vee q)\leftrightarrow (\mathrm{\neg }p\wedge \mathrm{\neg }q)$;

$(f)\mathrm{\neg }\mathrm{\neg }(p\vee \mathrm{\neg }p)$;

$(g)(p\to \mathrm{\neg }q)\to (\mathrm{\neg }p\to \mathrm{\neg }q)\to \mathrm{\neg }q$.

Ć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.

$(a)((p\to q)\to p)\to p$;

$(b)\mathrm{\neg }(p\wedge q)\leftrightarrow (\mathrm{\neg }p\vee \mathrm{\neg }q)$;

$(c)p\vee (p\to q)$;

$(d)((p\leftrightarrow q)\leftrightarrow r)\leftrightarrow (p\leftrightarrow (q\leftrightarrow r))$;

$(e)(\mathrm{\neg }\mathrm{\neg }p\to p)\to p\vee \mathrm{\neg }p$;

$(f)(p\to q)\leftrightarrow (\mathrm{\neg }p\vee q)$;

$(g)(p\to q)\to (\mathrm{\neg }p\to q)\to q$.

Ćwiczenie 6

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

$(a)(p\to q\to r)\to (p\to q)\to p\to r$;

$(b)((p\to q)\to p)\to p$;

$(c)((((p\to q)\to p)\to p)\to q)\to q$;

$(d)((p\to q)\to r)\to (p\to r)\to r$;

$(e)((((p\to q)\to r)\to (p\to r)\to r)\to q)\to q$.