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)\;\;\displaystyle \bot \to p$;

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

$(c)\;\;\displaystyle \neg \neg \neg p\to \neg p$;

$(d)\;\;\displaystyle (p\to q)\to (\neg q\to \neg p)$;

$(e)\;\;\displaystyle \neg (p\vee q)\leftrightarrow (\neg p\wedge \neg q)$;

$(f)\;\;\displaystyle \neg \neg (p\vee \neg p)$;

$(g)\;\;\displaystyle (p\to \neg q)\to (\neg p\to \neg q)\to \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)\;\;\displaystyle ((p\to q)\to p)\to p$;

$(b)\;\;\displaystyle \neg (p\wedge q)\leftrightarrow (\neg p\vee \neg q)$;

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

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

$(e)\;\;\displaystyle (\neg \neg p\to p)\to p\vee \neg p$;

$(f)\;\;\displaystyle (p\to q)\leftrightarrow (\neg p\vee q)$;

$(g)\;\;\displaystyle (p\to q)\to (\neg p\to q)\to q$.

Ćwiczenie 6

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

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

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

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

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

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