Re: Question regard implication and being a theorem of FOL.
- From: MoeBlee <jazzmobe@xxxxxxxxxxx>
- Date: Fri, 10 Oct 2008 16:58:38 -0700 (PDT)
On Oct 10, 4:18 pm, Scott <ToaTe...@xxxxxxxxx> wrote:
I still don't see how you are explaining the problem away.
I don't know of an actual particular problem you have found.
Perhaps a
change in notation would be helpful. Let F and G be any wff.
I think we all agree we have:
|- (F&~F) -> G
and for all intepretations the above is true so we have:
|= (F&~F) -> G
Right.
Suppose we have (F&~F)
What do you mean "we have"? We have in what context? As a line in a
proof?
then we get:
{ F&~F, (F&~F)->G } |- G
We have that in any case. It's just an instance of modus ponens. (My
'we have' here means 'it is a meta-theorem'.)
then for some interpretations M1 and M2 we can have:
M1: { F&~F, (F&~F)->G } |= G
That notation doesn't make sense.
For a model M, sentence P and a set of sentences G, (I'm stating for
sentences; thouth we can restate for formulas in general), we have
these notations:
|=_M P
to assert that P is true in M.
|= P
to assert that P is true in all models.
G |= P
to assert that any model in which all the members of G are true is a
model in which P is true.
We do NOT have a notation:
G |=_M P
What would it even mean?
Or, if you want to have such a notation, then please define it.
M2: { F&~F, (F&~F)->G } |/= G
Same remarks as above.
Thus, across all intepretations (ie, limited to the pure predicate
calculus) we have:
{ F&~F, (F&~F)->G } |- G
We don't need to mention interpretations for the above.
{ F&~F, (F&~F)->G } |/= G
No, that is INCORRECT.
{ F&~F, (F&~F)->G } |= G
if and only if
every interpretation that satisifes {F&~F (F&~F)->G} is an
interpretation that satisfies G.
And it IS the case that every interpretation that satisifes {F&~F
(F&~F)->G} is an interpretation that satisfies G, since there is no
interpretation that satisifies {F&~F (F&~F)->G}.
My question is: We say from a contradiction any wff can be proved, but
I don't see that. I see we can derive (symbolic manipluation to
generate the string of symbols forming the wff) any wff G,
What we mean by 'G is proven from a contradiction', is that we get G
by the rules of our system, using only logical axioms and the
contradiction as a premise.
And it should be clear to you by now (as you have studied enough
sentential logic) how to prove G from a contradiction, in whatever
ordinary proof system you're using.
but not
prove (wff is true) every wff G since G's truth value is dependent
upon the intepretation.
(1) I just addressed the notion of proof.
(2) The other notion is semantic. That is the notion of entailment, as
formulated in terms of interpretations. In that regard, it is the case
that a contradiction entails G. I.e., for any formula F and G we have:
F&~F |= G.
That is, any interpretation that satisfies F&~F is an interpretation
that satisifes G. Or more exactly:
For all formulas F, sets of formulas G, and interpretations M, if M
satisfies F&~F, then M satisfies G.
Or, if we're dealing with sentences:
For all sentences F, sets of sentences G, and models M, if F&~F is
true in M, then G is true in M.
MoeBlee
.
- References:
- Prev by Date: Re: Question regard implication and being a theorem of FOL.
- Next by Date: Re: Question regard implication and being a theorem of FOL.
- Previous by thread: Re: Question regard implication and being a theorem of FOL.
- Next by thread: Re: Question regard implication and being a theorem of FOL.
- Index(es):
Relevant Pages
|
