Thread: intuitionalistic proofs

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

Maybe you should stick to scuba.

So far, you're making no mathematicalogical sensicality.

well those are questions out of a logic text book so ?

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.

1) Premise: There exists an x Fx----> for all x Gx
Conclusion: for all x(Fx--->Gx)

I assume parentheses are as follows: implies . This is true. Fix an and assume . From this we get , and, therefore, and so .

2) Premise: There exists an x(Fx--->Gx)
Conclusion:for all x Fx---->there exists an x 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, .

thank you, all the symbols can be quite confusing, I apologise for the confusion I will be more clear in the future.

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?

ie: you can get a proof of p from a proof of <not><not>p (double negation p)

It's the other way around. From p one can prove (not (not p)) but in general not conversely.

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).

ive got it now thank you for the insight