Logik - reductio ad absurdum-Regel im KNS

20.09.2016, 01:44

Pippen

Logik - reductio ad absurdum-Regel im KNS

Ich referiere auf die Beispielsableitung auf wikipeda zum Kalkül natürlichen Schließens, etwas weiter unten. Sorry, aber offenbar darf ich keine URL's posten. Meiner Kenntnis nach gilt im KNS, dass wenn man aus einer Prämisse P eine Kontradiktion ableiten kann, man ~P folgern darf (sog. reductio ad absurdum-Regel). Das Problem ist nun, dass in o.g. Bsp. aus allen drei Annahmen zusammen der Widerspruch B & ~B folgt, so dass man nur alle drei Annahmen zusammen negieren könnte und nicht einfach eine einzige, die einem gerade passt. Das verstehe ich nicht, denn aus A, der 3. Annahme allein, folgt der Widerspruch nicht. Versteht jmd., was ich meine?

25.09.2016, 23:48

Pippen

Auf diesen Beitrag antworten »

RE: Logik - reductio ad absurdum-Regel im KNS
Niemand?

30.11.2022, 18:25

Finn_

Auf diesen Beitrag antworten »

Ein paar eingehendere Erläuterungen:

Natürliches Schließen (Teil 1: Aussagenlogik)
Natürliches Schließen (Teil 2: Prädikatenlogik)
Natürliches Schließen (Teil 3: Theorien mit Gleichheit)
Natürliches Schließen (Teil 4: Programme als Beweise)

01.12.2022, 04:32

Pippen

Auf diesen Beitrag antworten »

Mittlerweile habe ich es wohl verstanden. Wenn aus den Annahmen A, B ein Widerspruch folgt, dann darf man - wie man möchte!!! - folgern: ~A, ~B oder ~(A & B), weil das rein logisch den Widerspruch repariert und mehr interessiert in dem formallogischen Schema nicht.

Bsp.:

1. A -> B
2. ~B
3. A.
4. B & ~B (aus 1.-3.)

Jetzt kann Finn in 5. ~A folgern und damit weiterrechnen, während ich nur B folgere. Beide hätten wir korrekt geschlussfolgert.

Oder vllt. noch ein Beispiel aus der Praxis. Wenn gezeigt wird, dass V2 = p/q mit p,q ganze Zahlen widersprüchlich ist, dann kann man daraus folgern, dass ~(V2 = p/q) oder man könnte folgern, dass zB q keine ganze Zahl ist. Hier sieht man, dass in der Praxis aus verschiedenen möglichen Folgerungen diejenige gewählt wird, die einen interessiert.

01.12.2022, 08:37

Finn_

Auf diesen Beitrag antworten »

Im aufgeführten System ginge es folgendermaßen. Die Formel zur Exportation beweisen, das ist

$\begin{eqnarray*} \vdash (A\land B\to C)\leftrightarrow (A\to B\to C). \end{eqnarray*}$

Sie induziert die Schlussregel

$\begin{eqnarray*} \dfrac{\Gamma\vdash A\to B\to C}{\Gamma\vdash A\land B\to C}\rightsquigarrow \dfrac{\Gamma,A,B\vdash C}{\Gamma,A\land B\vdash C}. \end{eqnarray*}$

Hiermit findet sich

$\begin{eqnarray*} \dfrac{A,B\vdash\bot}{A\vdash\neg B},\qquad\dfrac{A,B\vdash\bot}{B\vdash\neg A},\qquad\dfrac{\dfrac{A,B\vdash\bot}{A\land B\vdash\bot}}{\vdash\neg (A\land B)}. \end{eqnarray*}$

Oder die Beweise der entsprechenden Formeln werden mit Coq bewältigt. Die CoqIde zeigt in jedem Schritt immer das nächste Ziel an.

code:

1:
2:
3:
4:
5:
6:
7:
8:
9:
10:
11:
12:
13:
14:
15:
16:
17:
18:
19:
20:
21:
22:
23:
24:
25:
26:
27:
28:
29:
30:

Theorem Satz0 (A B: Prop): (A -> B -> False) -> (A -> ~B).
Proof.
  intro h.
  intro a.
  intro b.
  apply h.
  * exact a.
  * exact b.
Qed.

Theorem Satz1 (A B: Prop): (A -> B -> False) -> (B -> ~A).
Proof.
  intro h.
  intro b.
  intro a.
  apply h.
  * exact a.
  * exact b.
Qed.

Theorem Satz2 (A B: Prop): (A -> B -> False) -> ~(A /\ B).
Proof.
  intro h.
  intro ab.
  destruct ab as (a, b).
  apply h.
  * exact a.
  * exact b.
Qed.

02.12.2022, 10:16

Pippen

Auf diesen Beitrag antworten »

Also nochmal am Beispiel:

1. A -> B (Prämisse)
2. ~B (Prämisse)
3. A (Prämisse)
4. B & ~B (folgt aus 1., 2., 3.)

Man kann jetzt in 5. direkt nur folgern ~((A -> B) & ~B & A), richtig?
Andere Folgerungen klappen nur indirekt; will man zB ~A folgern, dann sähe die Zeile in 5. so aus: ((A -> B) & ~B) -> ~A, man kann also nicht einfach und direkt in 5. hinschreiben: ~A, richtig?

02.12.2022, 10:59

Finn_

Auf diesen Beitrag antworten »

Ja, richtig. Die Bestätigung vermitteln die Beweisbäume

$\begin{eqnarray*} \dfrac{\dfrac{A\to B,\neg B,A\vdash\bot}{(A\to B)\land\neg B\land A\vdash\bot}}{\vdash \neg((A\to B)\land\neg B\land A)} \end{eqnarray*}$

und

$\begin{eqnarray*} \dfrac{\dfrac{\dfrac{A\to B,\neg B,A\vdash\bot}{A\to B, \neg B\vdash\neg A}}{(A\to B)\land\neg B\vdash\neg A}}{\vdash (A\to B)\land\neg B\to\neg A}. \end{eqnarray*}$

02.12.2022, 12:04

Finn_

Auf diesen Beitrag antworten »

Unterschiedliche Darstellungsformen mit Taktiken, die Coq als korrekt befindet:

code:

1:
2:
3:
4:
5:
6:
7:
8:
9:
10:
11:
12:
13:
14:
15:
16:
17:
18:
19:
20:
21:
22:
23:
24:
25:
26:
27:
28:
29:
30:
31:
32:
33:
34:
35:
36:
37:
38:
39:
40:
41:
42:
43:
44:
45:
46:
47:

(* Rückwärtsschließen *)
Theorem Kontraposition0 (A B: Prop): (A -> B) -> (~B -> ~A).
Proof.
  unfold not.
  intro h. intro nb. intro a.
  apply nb.
  apply h.
  exact a.
Qed.

(* Vorwärtsschließen *)
Theorem Kontraposition1 (A B: Prop): (A -> B) -> (~B -> ~A).
Proof.
  unfold not.
  intro h. intro nb. intro a.
  assert (b := h a).
  exact (nb b).
Qed.

(* Vorwärtsschließen, alternative Formulierung *)
Theorem Kontraposition2 (A B: Prop): (A -> B) -> (~B -> ~A).
Proof.
  unfold not.
  intro h. intro nb. intro a.
  apply h in a as b.
  apply nb in b as contradiction.
  exact contradiction.
Qed.

(* Beweisterm *)
Theorem Kontraposition3 (A B: Prop): (A -> B) -> (~B -> ~A).
Proof.
  exact (fun (h: A -> B) => fun (nb: ~B) => fun (a: A) => nb (h a)).
Qed.

(* Beweisterm in Kurzform *)
Theorem Kontraposition4 (A B: Prop): (A -> B) -> (~B -> ~A).
Proof.
  exact (fun h nb a => nb (h a)).
Qed.

(* Bitte automatisch finden *)
Theorem Kontraposition5 (A B: Prop): (A -> B) -> (~B -> ~A).
Proof.
  auto.
Qed.

02.08.2023, 07:55

Finn_

Auf diesen Beitrag antworten »

In aller Regel verbleiben immer Unsicherheiten, ob wir wirklich Klarheit gefunden haben, wie logisches Schließen zu verstehen sei. Am Montag unternahm ich den Versuch einer teilweisen Klärung, der glücklicherweise aufgegangen ist. Im vierten Teil der Folien steht ja bereits beschrieben, wie Beweise zur Nutzung von Coq in einen Fluss von Taktiken übersetzt werden. Ich habe nun umgekehrt vermittels Coq den Kalkül des natürlichen Schließens für die klassische Aussagenlogik getreu der geläufigen Theorie spezifiziert. Definiert wird, was eine wohlgeformte logische Formel ist, was eine Sequenz ist, was eine Tautologie ist, was eine gültige Sequenz ist, und was ein Beweis ist. Daraufhin wird mit struktureller Induktion über die Beweise die Korrektheit des Kalküls hinsichtlich der klassischen Semantik gezeigt. Außerdem werden noch einige zulässige Schlussregeln bewiesen.

Eine Bemerkung zur Implementierung. Für die Wahrheitswerte habe ich der Einfachheit halber den Typ Prop genutzt. Dadurch wird allerdings die Menge der Wahrheitswerte mit der Metalogik vermischt. Zudem verhindert dies, den Wahrheitswert einer konkreten Formel für konkrete Belegungen mit Compute ausrechnen lassen zu können, weil Prop nicht berechenbar ist. Man sollte die Implementierung aber auf Wahrheitswerte eines berechenbaren Typs wie bool aus der Standardbibliothek ummodeln können.

Der Quelltext : Sequent natural deduction for classical propositional calculus
Es ist gedacht, dass man mit CoqIDE durch einen Beweis navigiert. Das Schlüsselwort Inductive leitet die Definition eines neuen Typen ein. Kommt dieser als Typ des Arguments einer der Konstruktor-Funktionen vor, handelt es sich um einen rekursiv definierten Typen. Das Schlüsselwort Fixpoint leitet die rekursive Definition einer Funktion ein.

Neue Frage »

Antworten »

Logik - reductio ad absurdum-Regel im KNS

Verwandte Themen