Axiome basierend auf ↔,∨,⊥↔,∨,⊥\leftrightarrow, \lor, \bot für aussagenlogische intuitionistische Logik?

Aussagenlogische intuitionistische Logik kann basierend auf axiomatisiert werden → , ∧ , ∨ , ⊥ , mit modus ponens

aus  ϕ  Und  ϕ → ψ  schließen  ψ
als einzige Folgerungsregel und eine Liste von Axiomen wie
ϕ → ( χ → ϕ )
Eine vollständige Liste der Axiome finden Sie auf der Wikipedia-Seite über „Intuitionistische Logik“ unter „Kalkül im Hilbert-Stil“ .

Nun behauptet dieselbe Seite auch, dass „{∨, ↔, ⊥} und {∨, ↔, ¬} vollständige Grundlagen intuitionistischer Konnektoren sind.“ Und was ich suche, ist eine Liste von Inferenzregeln und Axiomen, um die Behauptung von Wikipedia zu untermauern.

Genau genommen ist das natürlich einfach: Man kann das nehmen → , ∧ , ∨ , ⊥ Axiome, und ersetzen Sie alle ϕ → ψ von ( ϕ ∨ ψ ) ↔ ψ , Und jeder ϕ ∧ ψ von ( ϕ ∨ ψ ) ↔ ( ϕ ↔ ψ ) . Aber das Ergebnis ist nicht sehr elegant.

Ich habe ein wenig darüber nachgedacht, eine schönere Axiomatisierung zu konstruieren, und ich denke, sie sollte zumindest die Inferenzregel haben

aus  ϕ  Und  ϕ ↔ ψ  schließen  ψ
und Axiome wie
( ϕ ↔ ψ ) ↔ ( ψ ↔ ϕ ) ( ϕ ↔ ( χ ↔ ψ ) ) ↔ ( ( ϕ ↔ χ ) ↔ ψ )

Daher meine Frage: Worauf basiert eine vollständige und elegante Axiomatisierung der aussagenlogischen intuitionistischen Logik? ↔ , ∨ , ⊥ ?

Es gibt immer "definieren ∨ , → in Bezug auf diese, und verwenden Sie dann die nette Axiomatisierung, die Sie bereits kennen".
@Hurkyl: Das scheint der Punkt des OP-Absatzes "Streng genommen ..." zu sein. Ich stimme zu, dass das Ergebnis davon kaum elegant wäre.
Wer sagt, dass es einen eleganten Weg gibt, dies zu tun?
@dfeuer Niemand, soweit ich weiß. Ich hoffe, es gibt eine elegante Möglichkeit, dies zu tun.
Sind Sie sicher, dass ( ϕ ∧ ψ ) ist intuitiv äquivalent zu ( ϕ ∨ ψ ) ↔ ( ϕ ↔ ψ ) ? Es funktioniert natürlich klassisch, aber ich sehe nicht, wie man das herleiten kann ϕ von letzterem intuitiv.
Möglicherweise finden Sie die Art der Charakterisierung, nach der Sie suchen, wenn Sie sich mit Heyting-Algebren befassen .
@HenningMakholm, ich denke, du hast Recht, aber ich weiß nicht genug, um es zu beweisen . Ich nehme an, ich muss eine Heyting-Algebra finden, in der sie nicht gilt? Ich versuche, etwas in der Menge der offenen Mengen der reellen Linie zu finden, aber erweitere sogar den Ausdruck ( P ∪ Q ) ↔ ( P ↔ Q ) erweist sich als ein ziemlich langer Prozess und gibt mir nichts, was viel Hoffnung auf eine intuitive Bedeutung zu haben scheint, die für die Produktion von Gegenbeispielen anfällig ist.
@dfeuer: Kripke-Modelle sind möglicherweise einfacher. Seit ϕ ≡ ( A ∨ B ) ↔ ( A ↔ B ) nur zwei Satzvariablen hat, gibt es nur vier mögliche Zustände der Welt. Und es scheint nicht möglich zu sein, wo einen Rahmen zusammenzustellen ϕ hat immer einen anderen Wert als A ∧ B , was IIRC bedeuten sollte, dass diese Darstellung von ∧ tatsächlich intuitionistisch gültig ist . Es erzeugt nicht wirklich eine Ableitung von A aus ϕ , obwohl ...
@HenningMakholm, leider bist du mir jetzt klar über den Kopf geflogen. Wenn es intuitionistisch gültig ist, würde das nicht bedeuten, dass es eine Ableitung geben muss (was unwahrscheinlich erscheint)?
@dfeuer: Ja, wenn es gültig ist, dann muss es eine Ableitung geben. Leider hilft eine Brute-Force-Überprüfung der möglichen Kripke-Modelle nicht dabei, diese Ableitung zu finden , obwohl sie (es sei denn, ich erinnere mich falsch, wie sie funktionieren, was möglich ist) implizieren, dass es irgendwo eines geben muss.
Laut Wikipedia, ( P ∧ Q ) ≡ ( ( ( P ∨ Q ) ⟺ P ) ⟺ Q ) , aber ich weiß auch nicht woher das kommt.
@dfeuer: Ich habe einen Beweis gefunden; siehe meine antwort.
Ich glaube nicht, dass "↔" mit intuitionistischer Logik assoziiert wird, oder?
Impliziert die Behauptung von Wikipedia etwas über die Möglichkeit einer solchen Axiomatisierung oder nur eine Behauptung über die Darstellbarkeit von Konnektoren?

Antworten (1)

Wie wäre es mit einem sequentiellen Kalkül mit Standardregeln:

Γ , P , P ⊢ Q Γ , P ⊢ Q C L Γ , P ⊢ P A X Γ , ⊥ ⊢ P ⊥ L
Γ ⊢ Q Γ , P ⊢ R Γ , P ↔ Q ⊢ R ↔ L 1 Γ ⊢ P Γ , Q ⊢ R Γ , P ↔ Q ⊢ R ↔ L 2 Γ , P ⊢ Q Γ , Q ⊢ P Γ ⊢ P ↔ Q ↔ R
Γ , P ⊢ R Γ , Q ⊢ R Γ , P ∨ Q ⊢ R ∨ L Γ ⊢ P Γ ⊢ P ∨ Q ∨ R 1 Γ ⊢ Q Γ ⊢ P ∨ Q ∨ R 2
Dies ist vollständig für die { ↔ , ∨ , ⊥ } Fragment, weil der vollständige intuitionistische Folgenkalkül die Schnittelimination erfüllt.

Um zu zeigen, dass dieses Fragment in seiner Expressivität vollständig ist , drücken Sie aus P → Q als ( P ∨ Q ) ↔ Q -- diese Äquivalenz ist intuitiv gültig, und die üblichen Links- und Rechtsregeln für → lassen sich leicht als Kombinationen der obigen Regeln aufbauen.

Ähnlich, ¬ P ist natürlich gleichbedeutend mit P ↔ ⊥ .

Für die Konjunktion stellt sich entgegen Spekulationen in Kommentaren heraus, dass ( P ∨ Q ) ↔ ( P ↔ Q ) ist in der Tat intuitiv äquivalent zu P ∧ Q . Die schwierige Richtung ist, das Übliche zu sehen ∧ L Regel zulässig, was im obigen Folgenkalkül wie folgt gemacht werden kann:

0. Γ ,   P ,   Q ⊢ R Prämisse der abgeleiteten Regel 1. P ⊢ P ∨ Q einfach 2. P ↔ Q ,   P ⊢ Q einfach 3. ( P ∨ Q ) ↔ ( P ↔ Q ) ,   P ⊢ Q 1 , 2 , ↔ L 2 4. ( P ∨ Q ) ↔ ( P ↔ Q ) ,   Q ⊢ P sinngemäß 5. ( P ∨ Q ) ↔ ( P ↔ Q ) ⊢ P ↔ Q 3 , 4 , ↔ R 6. P ∨ Q ⊢ P ∨ Q Axiom 7. Γ ,   P ∨ Q ,   P ↔ Q ⊢ R leichte Folge von  0 8. Γ ,   ( P ∨ Q ) ↔ ( P ↔ Q ) ,   P ∨ Q ⊢ R 6 , 7 , ↔ L 2 9. Γ ,   ( P ∨ Q ) ↔ ( P ↔ Q ) ,   ( P ∨ Q ) ↔ ( P ↔ Q ) ⊢ R 5 , 8 , ↔ L 1 10. Γ ,   ( P ∨ Q ) ↔ ( P ↔ Q ) ⊢ R 9 , C L

(Beweis durch erschöpfende Suche gefunden!)

Oder, für diejenigen, die den Curry-Howard-Isomorphismus für intuitionistische Beweise bevorzugen, die Idee in Haskell-ähnlicher Pseudosyntax für die ↔ ∨ ⊥ Fragment ist zu ersetzen

conj :: (P,Q)
let (x::P,y::Q) = conj
in  <..x..y..>

von

conj :: (Either P Q) <-> (P <-> Q)
let eq1 :: P <-> Q
    eq1 (x :: P) = let eq2 :: P <-> Q = conj (Left x) in eq2 x
    eq1 (y :: Q) = let eq2 :: P <-> Q = conj (Right y) in eq2 y
    disj :: Either P Q = conj eq1
in case disj of
     Left(x::P) -> let y::Q = eq1 x in <..x..y..>
     Right(y::Q) -> let x::P = eq1 y in <..x..y..>

wobei sich wie eine Funktion verhalten soll, die entweder auf oder P <-> Qangewendet werden kann und eine Ausgabe des entgegengesetzten Typs erzeugt, und die Disjunktion durch den Standardtyp dargestellt wird .PQEither

Welche Regeln sind ↔ L Und ↔ R , Exakt?
@dfeuer: Ich habe Regelnamen hinzugefügt
Vielleicht bin ich doof, aber wie geht das? Γ , P , Q ⊢ R als Prämisse sinnvoll?
@dfeuer: Das Ziel hier ist zu konstruieren
Γ , P , Q ⊢ R Γ ,   P ∧ Q ⊢ R ∧ L
als abgeleitete Regel. Wenn Sie nur ableiten möchten P ∧ Q ⊢ P , ersetzen R mit P und lass Γ leer sein.
Ich habe mir das jetzt etwas genauer durchgelesen. Es scheint, dass die wichtigsten Schritte wirklich 3–5 sind, während der Rest alles Aufbau und Abbau ist. Ist das ungefähr richtig?
@dfeuer: Ich denke schon, obwohl "Schlüsselschritte" natürlich subjektiv sind. Man könnte argumentieren, dass die Schlussfolgerung, die 9 abschließt, auch ziemlich wichtig ist: „Nun, da wir bewiesen haben P ↔ Q , unsere Kodierung von P ∧ Q sagt uns, dass wir auch haben P ∨ Q ". Meiner Meinung nach fangen wir an, etwas Positives zu wissen . Aber andererseits war es von Anfang an leicht zu sehen, dass wir das tun könnten, wenn wir es nur beweisen könnten P ↔ Q , also sind die Schritte 3-5 tatsächlich das, was Inspiration (oder vielmehr für mich rohe Gewalt) erforderte, um sie zu finden.
Axiome basierend auf ↔,∨,⊥↔,∨,⊥\leftrightarrow, \lor, \bot für aussagenlogische intuitionistische Logik?
AntwortenHierDatenschutz-Bestimmungen1y, 0v