Maybe you should stick to scuba.
So far, you're making no mathematicalogical sensicality.
I need some help deciding if these inferences are intuitionalistically valid
1) Premise: There exists an x Fx----> for all x Gx
Conclusion: for all x(Fx--->Gx)
2) Premise: There exists an x(Fx--->Gx)
Conclusion:for all x Fx---->there exists an x Gx
These are perfectly valid questions about intuitionistic, or constructive, logic.
Scubasteve123, when you are asking questions with narrow specialization, it may make sense to briefly describe the context; otherwise, people not familiar with the subject don't know whether it is nonsense or just something they don't know.
I assume parentheses are as follows: implies . This is true. Fix an and assume . From this we get , and, therefore, and so .1) Premise: There exists an x Fx----> for all x Gx
Conclusion: for all x(Fx--->Gx)
The conclusion is , right? This is also true. Assume . From the assumption take an that makes true. Then is true, so is true as well. Therefore, .2) Premise: There exists an x(Fx--->Gx)
Conclusion:for all x Fx---->there exists an x Gx
im having one hopefully last issue.
in the text it seems to say that in intuitionist logic you can take negations away but cannot add the negations
ie: you can get a proof of p from a proof of <not><not>p (double negation p)
but i am under the impression that you cannot add negations, so one of the questions is to show you can conclude <not> <not> p from a proof of p.
I didnt think this was valid?
It's the other way around. From p one can prove (not (not p)) but in general not conversely.ie: you can get a proof of p from a proof of <not><not>p (double negation p)
Usually, is taken as an abbreviation for ( denotes falsehood). So, given and an assumption one gets by Modus Ponens. Closing the assumption one gets , i.e., .
An intriguing thing is that one does not use the properties of in the derivation above. I.e., from one can prove for any formula .
One can also remove double negations, but only if the remaining formula itself starts with a negation: . In general, there is no difference between classical and intuitionistic logic for formulas that start with a negation: classically implies \ intuitionistically (Glivenko's theorem).