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