XPost: comp.theory, sci.math
From: polcott333@gmail.com
On 1/4/2026 12:55 PM, Mike Terry wrote:
> On 02/01/2026 17:54, Richard Damon wrote:
>> On 1/2/26 12:24 PM, Mike Terry wrote:
>>> On 02/01/2026 15:25, Richard Damon wrote:
>>>> On 1/2/26 1:14 AM, Tristan Wibberley wrote:
>>>>> On 02/01/2026 04:45, Richard Damon wrote:
>>>>>
>>>>>>
>>>>>>> Truth in the base system has always
>>>>>>> actually been theorems of the base system.
>>>>>>
>>>>>> But only if "Theorem" includes things proven to be true in the system
>>>>>> even if the proof is in another.
>>>>>
>>>>> If the statement is derived in another then it is a theorem of the
>>>>> other.
>>>>
>>>> I will disagree with you here. Maybe it iw what you are trying to
>>>> define "derived" as.
>>>>
>>>> I can certainly use one system to guide me in building a statement
>>>> in another. Or do you think that is a task too hard?
>>>>
>>>> I can certainly use one system that knows about another to show that
>>>> a statement must be true in that other.
>>>>
>>>> If you want to reserve the lable "Theorem" for only things provable
>>>> in taht system, I will let you, but point out I think you are in the
>>>> minority, and ask for your reference that specifies that.
>>>
>>> No, I'd say Tristan is spot on with how that's normally done.
>>>
>>> While speaking informally, "theorem" can mean "a mathematical
>>> statement that has a convincing argument for its truth" (e.g.
>>> Pythagoras' theorem), in formal logic "Theorem" and "Theory" have a
>>> technical meaning: "Theory" being the deductive closure of a set of
>>> axioms, and a Theorem being a sentence of the Theory. So every
>>> Theorem in the Theory has a "derivation" from the theories axioms.
>>> It is not directly to do with "truth" in the formal system. [Of
>>> course, we want our system (including axioms) to be sound, so all
>>> Theorems will be true.]
>>>
>>> >> Theory_(mathematical_logic)#Deductive_theories>
>>
>> Note, the addition of the adjective DEDUCTIVE.
>
> That's the type of theory most often encountered, I'd say. GIT is
> concerned with such a theory, where axioms are given etc. and we are
> looking at what sentences can be proved from those axioms. Wikipedia
> always tries to be as general as it can possibly be, making it an awful
> place for someone trying to /learn/ a maths topic. It's great if you're
> already a maths professor, then you can read some article and nod
> wisely, and suggest edits to make it /even more/ general! :)
>
>>
>>>
>>> Of course, you could be learning from an author taking a different
>>> approach, but I haven't personally come across one who would say that
>>> the sentence represented by G was a "Theorem" of the underlying
>>> logical system! (That would (IMO) be grossly misleading...)
>>
>> I will somewhat agree here, because generally the term is reserved for
>> statements about a more general truth, as opposed to a statement about
>> a specific fact. But the most generic definition is just a statment
>> that has been proven.
>
> Yes, but we are talking about formal systems, and "Theorem" in such a
> context implies a proof
> /within the proof calculus of that formal system/. That is what GIT is
> concerned with. (I give an example of what I mean by "proof calculus"
> below, but I'm sure you understand the idea, just possibly not the
> wording.)
>
>>
>>>
>>> Similarly, the word "proof" can be informal (simply an argument that
>>> convinces people of the truth of a statement), or refer to the "proof
>>> calculus" of the formal system being discussed. Most authors I've
>>> come across seem to use "proof" more or less informally and for
>>> clarity choose another word for whatever sequence of syntactic "proof
>>> steps" the formal system specifies. Often "derivation" is used, and
>>> that seems intuitive to me, so I try to always use that term here,
>>> and using "proof" for more general mathematial arguments, e.g.
>>> proving that the G statement is "true" using some meta-theory.
>>
>> The issue is that "derivation" doesn't actually imply a finiteness,
>> which is a necessity of "proof".
>
> Where do you get that idea? Are you thinking "derivation" is just an
> informal word? I'm using it in the technical sense previously explained.
>
> Within a formal system there will be a set of rules which define what a
> valid "derivation" looks like. These would ensure that such derivations
> are finite. (I'm sure someone at some time has made a special study of
> "infinite proofs", but that is off the beaten track.) As explained in
> my previous post, I'm using "derivation" as the technical term for
> whatever passes as a "formal proof conforming to the requirements of the
> proof calculus of the system". This is so that the idea does not get
> muddled with your more general kind of proof = "convincing argument in
> some meta-theory".
>
> Derivations have Gödel numbers. "Convincing arguments in the meta-
> theory" do not. The idea of a Gödel number for an infinite derivation
> does not make sense.
>
>>
>> The point is that the standard statement of "Incompleteness" talks
>> about the provability of statements in the system. Provability is
>> inherently about the ability to create a proof in the system.
>
> "(FORMAL) Proof in the system" = "derivation". You want to use the word
> "proof" more generally, namely to cover arguments in a meta-theory which
> establish some meta-truth concerning the base system. That's ok [and
> the reason I use "derivation" to distinguish from "informal proof"], but
> not the type of "proof" that incompleteness refers to.
>
>>
>> Yes, often an other will use a more confined word to establish the
>> method of a proof.
>
> Right. The logical system will have some kind of "proof calculus" which
> says EXACTLY what constitutes a valid derivation for that system. E.g.
> perhaps something like:
>
> A derivation is a finite sequence of sentences in the language of the
> formal system, such that
> each sentence is either:
> - an axiom of the system,
> - or can be constructed from previous sentences by applying one of
the
> following "deduction rules":
> - [probably something equivalent to Modus Ponens]
> - [maybe other listed rules]
> The last sentence of the derivation is the "result" of the derivation.
>
> When Gödel talks of provability in a system, he always means such a
[continued in next message]
--- SoupGate-DOS v1.05
* Origin: you cannot sedate... all the things you hate (1:229/2)
|
