Benutzer:Cobalt pen/p/Curry-Howard

Einige relavante Artikel in WP:

• Curry-Howard-Isomorphismus
• Hilbert-Kalkül
• Kombinatorische Logik
• Intuitionismus (Logik und Mathematik)
• Deduktionstheorem

Generell ist de:Kategorie:Typentheorie nur dünn besiedelt. Vergleiche hierzu en:Category:Type theory.

Ein Ansatz wäre, den Curry-Howard-Isomorphismus als Übergang zwischen Typisierung und Beweisen gangbar zu machen.

Dies könnte zunächst an eine minimalen propositionalen Logik erfolgen.

• en:Minimal logic
• en:Implicational propositional calculus
• en:SKI combinator calculus#Connection to intuitionistic logic

Das Lemma funktionale Vollständigkeit fehlt. Abschnitt hierzu, zitiere

Zentral wäre der Abschnitt en:Curry–Howard correspondence#Correspondence between Hilbert-style deduction systems and combinatory logic.

Entsprechung zwischen Hilbert-Kalkül und Kombinatorlogik

Erste Erwähnung findet die Entsprechung als Koinzidenz der einfachsten Sorten der Kombinatoren des SKI-Kalküls mit den Axiomen eines implikationalen Abschnitts des Hilbert-Kalküls.

Kombinator	Einfachster Kombinatortyp	Axiom im Hilbert-Kalkül
$Ix=x$	$\alpha \rightarrow \alpha$	$P\Rightarrow P$
$Kx\,y=x$	$\alpha \rightarrow \beta \rightarrow \alpha$	$P\Rightarrow Q\Rightarrow P$
$Sx\,y\,z=(xz)(yz)$	$(\alpha \rightarrow \beta \rightarrow \gamma )\rightarrow (\alpha \rightarrow \beta )\rightarrow \alpha \rightarrow \gamma$	$(P\Rightarrow Q\Rightarrow R)\Rightarrow (P\Rightarrow Q)\Rightarrow P\Rightarrow R$

Für einen Vergleich mit den entsprechenden Regeln speziell in den Logikkalkülen ist zu beachten, dass Implikation $\Rightarrow$ und Funktionspfeil $\rightarrow$ rechtsbindig verwendet werden, $P\Rightarrow Q\Rightarrow P$ also als $P\Rightarrow (Q\Rightarrow P)$ zu lesen ist. Für den Grund dieser Konvention siehe Currying.

Die angegebenen Axiome decken zusammen mit dem Modus ponens als Schlussregel denjenigen Teil intuitionistischer Aussagenlogik ab, der Aussagen betrifft, die nur Implikationen enthalten. Dieser Schlussregel entspricht auf der anderen Seite die Typisierung der Funktionsanwendung.

Typregel	Moduls ponens
${\frac {f:\alpha \rightarrow \beta \quad x:\alpha }{fx:\beta }}$	${\frac {P\Rightarrow Q\quad P}{Q}}$

Was hier als bloße Kuriosität erscheint, motiviert und begründet umfangreiche Forschung in der theoretischen Informatik, speziell mit Stoßrichtung auf maschinengestütztes Beweisen, die sich auf komplexe Ergebnisse der Typtheorie insbesondere im Zusammenhang mit dem Lambda-Kalkül und der Stufenlogik stützen kann.

Piercesches Gesetz

Nicht alle in der klassischen Aussagenlogik gültigen implikationalen Aussagen sind mit obigen Mitteln herleitbar, das Kalkül ist diesbzgl. unvollständig. Ein Beispiel für eine solche Aussage ist das Piercesche Gesetz: $((P\Rightarrow Q)\Rightarrow P)\Rightarrow P$.

• en:Peirce's law
• Fortsetzung

Currys Paradoxon

Currys Paradoxon

Siehe