subsection‹Peirce›
theory Peirce
imports Types
begin
text‹As an example of our $\lambda\mu$ formalisation, we show show a
$\lambda\mu$-term inhabiting Peirce's Law. The example is due to
Parigot~cite‹"DBLP:conf/lpar/Parigot92"›.›
text‹Peirce's law: $((A \rightarrow B) \rightarrow A) \rightarrow A$.›
lemma "Γ, Δ ⊨T λ (A→B)→A: (μ A:(<0>((`0) 🚫 (λ A: (μ B:(<1> (`0)))))))
: ((A→B)→A)→A"
by fastforce
end
¤ Dauer der Verarbeitung: 0.5 Sekunden
¤
*© Formatika GbR, Deutschland
