None of the axioms say anything about . Is it considered an abbreviation for ?
The problems:
a) for any
I'm confused about this one because I tried proof by contradiction, so:
(1) by assumption
(2) by assuming the negation of where is also written as
... and then isn't that already a contradiction?
b) where x is not free in
This one I think it must involve axioms 4 and 5 somehow, but I guess that's obvious
c) for any term not involving x
And this one must involve axioms 4 and 6
Derive them using these (for your convenience and my LaTeX practice):
Axioms:
1:
2:
3:
4: ( is a term freely substitutable for x in )
5: (where x is not free in )
6:
7:
As well as Modus Ponens, Generalization, and the Deduction theorem
Any help would be really appreciated!
How much has been laid down prior to these exercises i.e., much support do you have at your disposal?
On the one hand, as you've written it, it appears you've been asked to prove these claims with just the seven axiom schemes, two rules and Dth.
But this is at odds with what you comtemplate for a proof of a). Apparently, you're going to attempt a proof by contradiction.
So apparently, at least one version of this proof method has already been introduced.
This is what I mean by support. How much support do you have to work with in addition to the bare-bones deductive apparatus
you describe at the bottom?
You can also indicate what (conservative) definitional extensions to the system have been carried out.
Certainly, the existential quantifier is one.
You know, if you're working from a textbook, why not provide the pertinent information about it?
Not yet. You need remove the by applying axiom (4) with an arbitrary term, such as an unrelated variable . Then you'll have and , i.e., \bot (contradiction, which is what you need.
Note, by the way, that this law: is not so good after all because it is false in the interpretation with an empty domain. Proving it is possible because of the bad accounting of free variables -- here we picked a stray variable . If all variables are strictly accounted for -- as in branch of proof theory called type theory -- such shenanigans are not possible.
Here it becomes a little involved are would probably require a lot of intermediate helper theorems. Assume and . We'll prove by contradiction, so assume . But first we will prove ; together with this will give us the needed contradiction.
To prove , fix some and assume ; we need to obtain a contradiction. Plug into to get . By MP, we get , but earlier we assumed .
Now there is a task to translate this into using your axioms...