Philosophy Now Forum

(1) By definition we know that every sound deductive argument
has a true conclusion. True premises plus valid deduction
necessitates a true conclusion.

(2) When this is applied to the formal proofs of mathematical
logic we know (by definition) that every deductively sound
formal proof of mathematical logic necessarily has a true consequence.

(3) Therefore (by definition) applying deductively sound formal
proofs of mathematical logic to every expression of a formal
system F selects all and only true sentences of F.

Traditionally, the definition of the notion of validity relies on the notion of truth: An inference is valid if and only if the truth of the conclusion follows from the truth of the premises.
I understand that you choose a definition of truth relying on the notion of validity.
Am I wrong?
EB

Speakpigeon wrote: ↑Sat May 25, 2019 7:52 pm Traditionally, the definition of the notion of validity relies on the notion of truth: An inference is valid if and only if the truth of the conclusion follows from the truth of the premises.
I understand that you choose a definition of truth relying on the notion of validity.
Am I wrong?
EB

Yes that is it. Now we just need to translate that to mathematical logic.

Speakpigeon wrote: ↑Sat May 25, 2019 7:52 pm Traditionally, the definition of the notion of validity relies on the notion of truth: An inference is valid if and only if the truth of the conclusion follows from the truth of the premises.
EB

Yes that is it. Now we just need to translate that to mathematical logic.

Sorry, I don't know which one to respond to. You know you can still modify your posts, so please, make clear which one is your reply.
EB

Speakpigeon wrote: ↑Sun May 26, 2019 10:19 am Sorry, I don't know which one to respond to. You know you can still modify your posts, so please, make clear which one is your reply.
EB

What it the most conventional way to formalize this?
Γ is a set of WFF of F
C is a WFF of F
Every element of Γ is true
C is provable from Γ

This is my first guess:
∀Γ ⊆ WFF(F) ∀C ∈ WFF(F) (True(Γ) ∧ (Γ ⊢ C))

PeteOlcott wrote: ↑Sun May 26, 2019 3:03 pm

Speakpigeon wrote: ↑Sun May 26, 2019 10:19 am Sorry, I don't know which one to respond to. You know you can still modify your posts, so please, make clear which one is your reply.
EB

What it the most conventional way to formalize this?
Γ is a set of WFF of F
C is a WFF of F
Every element of Γ is true
C is provable from Γ

This is my first guess:
∀Γ ⊆ WFF(F) ∀C ∈ WFF(F) (True(Γ) ∧ (Γ ⊢ C))

You're not going to like it but I don't think we need to talk about wff, any "formal system", or specifying True(Γ). You can't formally prove anything that's not a wff and you don't formally prove any formula outside the context of a formal system.
A formula is never known to be true. True formulas are either those you define as true from the start or those that are true as a result of the conventions of the logical language you are using. Any formula F is provable if and only if it is the valid consequent of some true formula G:

Provable(F) ≡ G ∧ (G → F)

OK, it's just the modus ponens, but you do need to find a logical truth G to derive F from it.
For example, in Aristotelian logic, (A ∨ ¬A) ∨ C is provable because A ∨ ¬A is a logical truth and (A ∨ ¬A) → (A ∨ ¬A ∨ C) is valid.
So we have:

Provable(A ∨ ¬A ∨ C) ≡ (A ∨ ¬A) ∧ ((A ∨ ¬A) → (A ∨ ¬A ∨ C))

And of course you need to specify your language and in particular what formulas are defined as true.
EB