I just copied and pasted it from google.Nice solution, I can follow both parts. (G→H)→((F→G)→(F→H)) and F→(G→H) ≡ G→(F→H) are two very useful theorems now that I think about it.
Leib (Leibniz) is a basic rule of inference in our logic. It allows us to apply a theorem to part of the formula and...
We have a theorem that states: (∀x)(A'∨B') ≡ A'∨(∀x)B' if x dnof in A'
So the equational style proof is:
((∃x)A)→B
⇔<def'n of ∃>
(¬(∀x)¬A)→B
⇔<abs thm + Leib>
¬(¬(∀x)¬A)∨B
⇔<abs thm + Leib>
((∀x)¬A)∨B
⇔<axiom>
B∨((∀x)¬A)
⇔<thm (∀x)(A'∨B') ≡ A'∨(∀x)B' if x dnof in A'>
(∀x)(B∨¬A)
⇔<abs thm +...
Hey techmologist, thanks for those hints and I have since solved it after knowing there are no free occurrences of x in B.
Interesting, thanks for the references. I am going to look at some other logic books to broaden my perspective, especially since no one logic system or even notation seems...
Yeah, that was actually the typo from the instructor, it was supposed to say that x does not occur free in B.
The original problem actually did not specify that B contains no free occurrences of x so, as you said, the equivalence is not valid.
Hey RUber, WWGD, and anyone else who was working on this problem. I actually just disproved this statement to be true and then found out it was indeed a typo by my teacher. Sorry if I caused anyone much pain over this problem.
To disprove that (∀x)(A → B) ≡ ((∃x)A) → B is an absolute theorem...
Hey RUber,
Yeah, it gets kind of confusing. The way our class is interpreting them is like this:
∃x(A→B) is true if at least one x in the domain satisfies A→B
A→B is true if the specific x we have just picked from the domain satisfies A→B
∀x(A→B) is true if for all x in the domain A→B is...
Hmm, I'm still not sure of the first two. They seem right, but I just can't find any support for them.
Assume this interpretation: A is "x=0", B is "x=1", the domain is {0, 1}, and x is 1.
A→B is true, because A is false
∀x(A→B) is false because there is an x that will make A true and B false...
Wow, that is actually at least very close, but I still can't figure out a few of your steps.
∀x (~B)→∀x(~A) ⇔~B→ ∀x(~A)
is this a theorem that is true in general? I can't seem to find any reference in the text that allows for this removal of universal quantifier (but I could be missing...
Hey RUber,
I definitely see what you are saying, and if I could prove this using intuition or naive logic, it would be so much easier.
I just can't seem to translate that reasoning into the strict formal logic of only using inference rules and absolute theorems to derive one side from the...
Hey WWGD,
Thanks for the response.
Truth trees seem like an interesting concept from my quick Googling, but we weren't introduced to those yet in the text and I think that would be outside of the scope of a formal proof in first-order logic (or a Hilbert style proof).
Is there perhaps any way...
Hey RUber,
Thanks for the reply and you understood my notation perfectly.
I think we can assume the contrapositive. However, when you get to for all x (not B implies not A), I don't know how to make that equivalent to (not B) implies for all x (not A)
left side: ∀x(~B → ~A)
right side: ~B →...
Hello,
I am having particular trouble with the below problem. We are using http://studygig.com/uploads/materials/math1090_mathematical_logi.pdf and we must prove this statement using Hilbert style or Equational style proof (first-order logic), but any proof of any type would point me in the...
I see, good point mathwonk, I guess it is better to not skip courses. Also, your mathematician thread is really good. I'll definitely remember it for future reference.
@tycon69: Well, summer school is an option for only 1-2 courses here in Canada, and even then it is penalized on your...
mathwonk, I read the first half of that pretty well but I couldn't finish it (I only had about 20 minutes). I think I would need to draw a diagram and break it down piece-by-piece. Is this bad, should I be able to read that easily if I know high school math?
@Larphraulen : Thank you, that was...