Google Groups no longer supports new Usenet posts or subscriptions. Historical content remains viewable.
Dismiss

Deductively sound formal proofs (v6)

1 view
Skip to first unread message

peteolcott

unread,
May 12, 2019, 2:11:28 AM5/12/19
to
All that we have to do to provide
[deductively sound formal proofs of mathematical logic]
is select the subset of conventional [formal proofs of mathematical logic]
having true premises and now we have
[deductively sound formal proofs of mathematical logic].

This tiny little change provides the entire basis for this predicate:
∀Γ∀C Deductively_Sound(Γ, C) := (True(Γ) ⊢ C)

Since the above predicate precisely specifies actual sound deduction
whenever it rejects any expression as deductively unsound it is sound
deduction itself that is rejecting this expression.

Every expression of any formal language that is not provable: (F ⊬ G)
is according to sound deductive logic itself: ¬Deductively_Sound(F, G)


Deductively Sound Formal Proofs
https://www.researchgate.net/publication/332864362_Deductively_Sound_Formal_Proofs

--
Copyright 2019 Pete Olcott
All rights reserved

peteolcott

unread,
May 12, 2019, 2:32:20 AM5/12/19
to
On 5/12/2019 1:11 AM, peteolcott wrote:
> All that we have to do to provide
> [deductively sound formal proofs of mathematical logic]
> is select the subset of conventional [formal proofs of mathematical logic]
> having true premises and now we have
> [deductively sound formal proofs of mathematical logic].
>
> This tiny little change provides the entire basis for this predicate:
CORRECTION:
∀Γ∀C Deductively_Sound(Γ, C) := (True(Γ) ∧ (Γ ⊢ C))
0 new messages