Strukturregel - Structural rule

In der Beweistheorie ist eine Strukturregel eine Inferenzregel , die sich nicht auf eine logische Verknüpfung bezieht , sondern direkt auf das Urteil oder die Sequenzen wirkt . Strukturelle Regeln ahmen oft beabsichtigte metatheoretische Eigenschaften der Logik nach. Logiken, die eine oder mehrere der Strukturregeln verweigern, werden als substrukturelle Logiken klassifiziert .

Gemeinsame Strukturregeln

Drei gängige Strukturregeln sind:

• Schwächung , bei der die Hypothesen oder der Abschluss einer Sequenz um zusätzliche Mitglieder erweitert werden können. In symbolischer Form können Abschwächungsregeln wie links vom Drehkreuz und rechts geschrieben werden.${\displaystyle {\frac {\Gamma\vdash\Sigma }{\Gamma,A\vdash\Sigma}}}$${\displaystyle {\frac {\Gamma\vdash\Sigma }{\Gamma\vdash\Sigma,A}}}$
• Kontraktion , bei der zwei gleiche (oder vereinbare) Mitglieder auf derselben Seite einer Sequenz durch ein einzelnes Mitglied (oder eine gemeinsame Instanz) ersetzt werden können. Symbolisch: und . In automatisierten Theorem- Beweissystemen mit Auflösung auch als Factoring bekannt . In der klassischen Logik als Idempotenz der Folgerung bekannt .${\displaystyle {\frac {\Gamma,A,A\vdash\Sigma }{\Gamma,A\vdash\Sigma}}}$${\displaystyle {\frac {\Gamma\vdash A,A,\Sigma }{\Gamma\vdash A,\Sigma}}}$
• Exchange , bei dem zwei Mitglieder auf derselben Seite einer Sequenz getauscht werden können. Symbolisch: und . (Dies wird auch als Permutationsregel bezeichnet .)${\displaystyle {\frac {\Gamma_{1},A,\Gamma_{2},B,\Gamma_{3}\vdash\Sigma}{\Gamma_{1},B,\Gamma_{ 2},A,\Gamma_{3}\vdash\Sigma}}}$${\displaystyle {\frac {\Gamma\vdash\Sigma_{1},A,\Sigma_{2},B,\Sigma_{3}}{\Gamma\vdash\Sigma_{1},B, \Sigma_{2},A,\Sigma_{3}}}}$

Eine Logik ohne eine der obigen Strukturregeln würde die Seiten einer Sequenz als reine Sequenzen interpretieren ; mit Austausch sind sie Multisets ; und sowohl bei der Kontraktion als auch beim Austausch sind sie Mengen .

Dies sind nicht die einzigen möglichen Strukturregeln. Eine berühmte Strukturregel ist als Schnitt bekannt . Beweistheoretiker wenden erhebliche Anstrengungen auf, um zu zeigen, dass Schnittregeln in verschiedenen Logiken überflüssig sind. Genauer gesagt wird gezeigt, dass cut nur (in gewissem Sinne) ein Werkzeug zur Abkürzung von Beweisen ist und nicht zu den beweisbaren Theoremen beiträgt. Das erfolgreiche 'Entfernen' von Schnittregeln, bekannt als Schnitteliminierung , steht in direktem Zusammenhang mit der Philosophie der Berechnung als Normalisierung (siehe Curry-Howard-Korrespondenz ); es gibt oft einen guten Hinweis auf die Komplexität der Entscheidung über eine gegebene Logik.

Siehe auch

• Affine Logik
• Lineare Logik
• Geordnete Logik
• Strenge Logik
• Trennlogik