Abenteuer-Universum

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?

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.