Results 1 to 5 of 5

Math Help - derivations in predicate calculus

  1. #1
    Newbie
    Joined
    Mar 2010
    Posts
    4

    derivations in predicate calculus

    The problems:

    a) \vdash (\forall x \phi \rightarrow \exists x \phi) for any \phi

    I'm confused about this one because I tried proof by contradiction, so:
    (1) \forall x \phi by assumption
    (2) \forall x \neg\phi by assuming the negation of \exists x \phi where \exists x is also written as \neg \forall x \neg
    ... and then isn't that already a contradiction?

    b) \forall x(\phi \rightarrow \psi) \vdash (\exists x \phi \rightarrow \psi) where x is not free in \psi

    This one I think it must involve axioms 4 and 5 somehow, but I guess that's obvious

    c) \vdash \exists x (x = \tau) for any term \tau 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: (\phi \rightarrow (\psi \rightarrow \phi))
    2: ((\phi \rightarrow (\psi \rightarrow \theta)) \rightarrow ((\phi \rightarrow \psi) \rightarrow (\phi \rightarrow \theta)))
    3: ((\neg\phi\rightarrow\neg\psi)\rightarrow(\psi\rig  htarrow\phi))
    4: (\forall x \phi(x) \rightarrow \phi (\tau)) ( \tau is a term freely substitutable for x in \phi)
    5: (\forall x (\phi \rightarrow \psi) \rightarrow (\phi \rightarrow \forall x \psi)) (where x is not free in \phi)
    6: \forall x (x=x)
    7:  (x = y \rightarrow (\phi(x,x) \rightarrow \phi(x,y)))

    As well as Modus Ponens, Generalization, and the Deduction theorem

    Any help would be really appreciated!
    Follow Math Help Forum on Facebook and Google+

  2. #2
    MHF Contributor
    Joined
    Oct 2009
    Posts
    5,501
    Thanks
    765
    None of the axioms say anything about \exists. Is it considered an abbreviation for \neg\forall\neg?
    Follow Math Help Forum on Facebook and Google+

  3. #3
    Newbie
    Joined
    Mar 2010
    Posts
    4
    Quote Originally Posted by emakarov View Post
    None of the axioms say anything about \exists. Is it considered an abbreviation for \neg\forall\neg?
    Yes, it is, do you think I should just immediately go through and change all the \exists to \neg\forall\neg?
    Follow Math Help Forum on Facebook and Google+

  4. #4
    Junior Member
    Joined
    Oct 2006
    Posts
    71
    Quote Originally Posted by logicloser View Post
    The problems:

    a) \vdash (\forall x \phi \rightarrow \exists x \phi) for any \phi

    I'm confused about this one because I tried proof by contradiction, so:
    (1) \forall x \phi by assumption
    (2) \forall x \neg\phi by assuming the negation of \exists x \phi where \exists x is also written as \neg \forall x \neg
    ... and then isn't that already a contradiction?

    b) \forall x(\phi \rightarrow \psi) \vdash (\exists x \phi \rightarrow \psi) where x is not free in \psi

    This one I think it must involve axioms 4 and 5 somehow, but I guess that's obvious

    c) \vdash \exists x (x = \tau) for any term \tau 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: (\phi \rightarrow (\psi \rightarrow \phi))
    2: ((\phi \rightarrow (\psi \rightarrow \theta)) \rightarrow ((\phi \rightarrow \psi) \rightarrow (\phi \rightarrow \theta)))
    3: ((\neg\phi\rightarrow\neg\psi)\rightarrow(\psi\rig  htarrow\phi))
    4: (\forall x \phi(x) \rightarrow \phi (\tau)) ( \tau is a term freely substitutable for x in \phi)
    5: (\forall x (\phi \rightarrow \psi) \rightarrow (\phi \rightarrow \forall x \psi)) (where x is not free in \phi)
    6: \forall x (x=x)
    7:  (x = y \rightarrow (\phi(x,x) \rightarrow \phi(x,y)))

    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?
    Follow Math Help Forum on Facebook and Google+

  5. #5
    MHF Contributor
    Joined
    Oct 2009
    Posts
    5,501
    Thanks
    765
    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?
    Not yet. You need remove the \forall by applying axiom (4) with an arbitrary term, such as an unrelated variable y. Then you'll have \phi(y) and \neg\phi(y), i.e., \bot (contradiction, which is what you need.

    Note, by the way, that this law: \forall x.\,\phi\to\exists x.\,\phi 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 y. If all variables are strictly accounted for -- as in branch of proof theory called type theory -- such shenanigans are not possible.

    b) where x is not free in
    Here it becomes a little involved are would probably require a lot of intermediate helper theorems. Assume \forall x.\,\phi(x)\to\psi and \neg\forall x.\,\neg\phi(x). We'll prove \psi by contradiction, so assume \neg\psi. But first we will prove \forall x.\,\neg\phi(x); together with \neg\forall x.\,\neg\phi(x) this will give us the needed contradiction.

    To prove \forall x.\,\neg\phi(x), fix some x_0 and assume \phi(x_0); we need to obtain a contradiction. Plug x_0 into \forall x.\,\phi(x)\to\psi to get \phi(x_0)\to\psi. By MP, we get \psi, but earlier we assumed \neg\psi.

    Now there is a task to translate this into using your axioms...
    Follow Math Help Forum on Facebook and Google+

Similar Math Help Forum Discussions

  1. predicate calculus
    Posted in the Discrete Math Forum
    Replies: 8
    Last Post: December 13th 2009, 11:01 AM
  2. Predicate calculus - propositions
    Posted in the Discrete Math Forum
    Replies: 3
    Last Post: August 2nd 2009, 08:50 PM
  3. Predicate Calculus
    Posted in the Calculus Forum
    Replies: 1
    Last Post: May 21st 2009, 05:19 PM
  4. Predicate Calculus Question
    Posted in the Discrete Math Forum
    Replies: 0
    Last Post: May 20th 2009, 05:39 PM
  5. Predicate Calculus help
    Posted in the Discrete Math Forum
    Replies: 5
    Last Post: March 6th 2009, 10:19 PM

Search Tags


/mathhelpforum @mathhelpforum