Theorem zu einem korrekten und vollständigen Kalkül

[Pippen]

Gegeben ein beliebiges Kalkül K mit einer beliebigen Formelmenge F und einer beliebigen Interpretation:

Wenn K korrekt und vollständig ist, dann gilt definitionsgemäß: (F |- a) <-> (F |= a). Das wäre ein wahres Bikonditional und ein Blick auf dessen Wahrheitstabelle zeigt uns, dass damit entweder beide Teile wahr oder beide Teile falsch sein müssen, woraus folgt: (F |- a) -> (F |= a), d.h. a ist ableitbar, dann ist a wahr und ~(F |- a) -> ~(F |= a), d.h. a ist nicht ableitbar, dann ist a nicht wahr, also falsch.

MaW: In einem korrekten und vollständigen Kalkül kann man nicht nur von der Ableitbarkeit einer Formel auf deren Wahrheit schließen, sondern auch umgekehrt von der Nichtableitbarkeit auf deren Falschheit. Richtig?

[Elvis]

Ein formales System heißt korrekt und vollständig, wenn stets |=. Die Formeln müssen aus Axiomen ableitbar bzw. aufgrund von Axiomen wahr sein, nicht nur aus Formeln F oder aufgrund von Formeln. Was du "MaW" sagst ist völlig richtig.