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

1. Podać konstrukcje dla następujących formuł:
   1. $\mathrm{\perp }\to p$;
   2. $(p\to q\to r)\to (p\to q)\to p\to r$;
   3. $\mathrm{\neg }\mathrm{\neg }\mathrm{\neg }p\to \mathrm{\neg }p$;
   4. $(p\to q)\to (\mathrm{\neg }q\to \mathrm{\neg }p)$;
   5. Parser nie mógł rozpoznać (nieznana funkcja „\oto”): {\displaystyle \displaystyle \neg(p\vee q) \oto (\neg p\wedge \neg q)} ;
   6. $\mathrm{\neg }\mathrm{\neg }(p\vee \mathrm{\neg }p)$;
   7. $(p\to \mathrm{\neg }q)\to (\mathrm{\neg }p\to \mathrm{\neg }q)\to \mathrm{\neg }q$.

1. 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. 1. $((p\to q)\to p)\to p$;
   2. Parser nie mógł rozpoznać (nieznana funkcja „\oto”): {\displaystyle \displaystyle \neg(p\wedge q) \oto (\neg p\vee \neg q)} ;
   3. $p\vee (p\to q)$;
   4. $((p\leftrightarrow q)\leftrightarrow r)\leftrightarrow (p\leftrightarrow (q\leftrightarrow r))$;
   5. $(\mathrm{\neg }\mathrm{\neg }p\to p)\to p\vee \mathrm{\neg }p$;
   6. $(p\to q)\leftrightarrow (\mathrm{\neg }p\vee q)$;
   7. $(p\to q)\to (\mathrm{\neg }p\to q)\to q$.

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

1. 1. $(p\to q\to r)\to (p\to q)\to p\to r$;
   2. $((p\to q)\to p)\to p$;
   3. $((((p\to q)\to p)\to p)\to q)\to q$;
   4. $((p\to q)\to r)\to (p\to r)\to r$;
   5. $((((p\to q)\to r)\to (p\to r)\to r)\to q)\to q$.