Re: Sorry Godel - All Truths are Provable


Jan Burse wrote:
Howdy


G'day.

Rupert wrote:
What logic? I don't understand your reasons for thinking the
truth-value of a statement has to coincide with its provability-value.

Doesn't have to, but for most logics it does,
respectively one can develop valuations
that coincide with some deductive systems.


Sure, but I was under the impression we were talking about first-order
arithmetic, "provability" probably referring to PA or something like
that.

Lemma 1: Correktness of Provability:
|- A => |= A.

Proof: Done by induction on the
proof length usually.

Lemma 2: Completness of Provability:
|= A => |- A.

Proof: Usually shown that if |/- A
then exists M with M |= ~A, i.e.
counter model construction.

Lemma 3:
|= A <=> |- A.

Proof: Follows from Lemma 1 and Lemma 2.

Highly recommended reading:
Ebbinghaus et al.: Mathematical Logic,
Second Edition, Springer Verlag, 1996

IV A Sequent Calculus, 6.2 Theorem on the Correctness
V The Completeness Theorem, 4.1 Completness Theorem

Further References for the Completeness Theorem:
K. Gödel, Die Vollständigkeit (=Completness) der
Axiome des logischen Funktionenkalküls, Monatshefte für
Mathematik und Physik 37 (1930)

L. Henkin, The Completness of First-Order
Functional Calculus, The Journal of Symbolic
Logic 14 (1949)

.

Relevant Pages

  • Re: Sorry Godel - All Truths are Provable
    ... truth-value of a statement has to coincide with its provability-value. ... Lemma 1: Correktness of Provability: ... IV A Sequent Calculus, ... V The Completeness Theorem, 4.1 Completness Theorem ...
    (sci.logic)
  • Re: Sorry Godel - All Truths are Provable
    ... truth-value of a statement has to coincide with its provability-value. ... Doesn't have to, but for most logics it does, respectively one can ... This observation, correct as it is, is not any more relevant to Rupert's puzzlement than the completeness theorem in its usual form, and I don't see how it could sensible be construed as the "truth-value" of a statement coinciding with its "provability-value". ...
    (sci.logic)
  • Re: Godels Incompleteness and Nonmonotonic Logic
    ... >> provability to have to be decidable. ... > Decidability is a separate issue. ... If the logics we're talking about ... without any reference to Goedel theorems. ...
    (comp.lang.prolog)
  • Re: Godels Incompleteness and Nonmonotonic Logic
    ... >> provability to have to be decidable. ... > Decidability is a separate issue. ... If the logics we're talking about ... without any reference to Goedel theorems. ...
    (sci.logic)
  • Re: Simple yet Profound Metatheorem
    ... >>premises is not a valid proof in these logics. ... denoted by the "absurdity symbol") from P&~P and then ... truth as provability. ...
    (sci.logic)