When we specify that True(x) is the subset of the conventional
formal proofs of mathematical logic having true premises then
True(x) is always defined and never undefinable.
Introduction to Mathematical logic Sixth edition Elliott Mendelson (2015):28
A wf C is said to be a consequence in S of a set Γ of wfs if and only if there is a
sequence B1, …, Bk of wfs such that C is Bk and, for each i, either Bi is an axiom
or Bi is in Γ, or Bi is a direct consequence by some rule of inference of some of
the preceding wfs in the sequence. Such a sequence is called a proof (or deduction)
of C from Γ. The members of Γ are called the hypotheses or premisses of the proof.
We use Γ ⊢ C as an abbreviation for “C is a consequence of Γ”...
The 1936 Tarski Undefinability Proof
http://liarparadox.org/Tarski_Proof_275_276.pdf
--
Copyright 2019 Pete Olcott
All rights reserved