(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.
How do we say this using the notation conventions of mathematical logic?
-
- Posts: 1514
- Joined: Mon Jul 25, 2016 6:55 pm
How do we say this using the notation conventions of mathematical logic?
Last edited by PeteOlcott on Sun May 26, 2019 3:01 pm, edited 1 time in total.
- Speakpigeon
- Posts: 987
- Joined: Sat Nov 11, 2017 3:20 pm
- Location: Paris, France, EU
Re: How do we say this using the notation conventions of mathematical logic?
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
I understand that you choose a definition of truth relying on the notion of validity.
Am I wrong?
EB
-
- Posts: 1514
- Joined: Mon Jul 25, 2016 6:55 pm
Re: How do we say this using the notation conventions of mathematical logic?
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.
I understand that you choose a definition of truth relying on the notion of validity.
Am I wrong?
EB
-
- Posts: 1514
- Joined: Mon Jul 25, 2016 6:55 pm
Re: How do we say this using the notation conventions of mathematical logic?
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
- Speakpigeon
- Posts: 987
- Joined: Sat Nov 11, 2017 3:20 pm
- Location: Paris, France, EU
Re: How do we say this using the notation conventions of 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
EB
-
- Posts: 1514
- Joined: Mon Jul 25, 2016 6:55 pm
Re: How do we say this using the notation conventions of mathematical logic?
What it the most conventional way to formalize this?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
Γ 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))
- Speakpigeon
- Posts: 987
- Joined: Sat Nov 11, 2017 3:20 pm
- Location: Paris, France, EU
Re: How do we say this using the notation conventions of mathematical logic?
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.PeteOlcott wrote: ↑Sun May 26, 2019 3:03 pmWhat it the most conventional way to formalize this?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
Γ 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))
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:
OK, it's just the modus ponens, but you do need to find a logical truth G to derive F from it.Provable(F) ≡ G ∧ (G → F)
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:
And of course you need to specify your language and in particular what formulas are defined as true.Provable(A ∨ ¬A ∨ C) ≡ (A ∨ ¬A) ∧ ((A ∨ ¬A) → (A ∨ ¬A ∨ C))
EB