Results 1 to 4 of 4

Math Help - Trouble with formal deduction in first order logic

  1. #1
    Newbie
    Joined
    Mar 2013
    From
    Moscow
    Posts
    3

    Trouble with formal deduction in first order logic

    Hey,

    I've been using this forum for a while now, just as to get help here, there, and it's super helpful to understand logic!

    I have this specific difficulty with understanding how to prove the existence of deductions in first order logic. Would really appreciate if someone could walk me through an example! I understand it high-level, but I don't know what axioms or meta theorems to use to do it.

    Here is "simple" question in class textbook:

    L is a FOL (First Order Language).
    L contains R, where R is a single binary predicate symbol.
    a1, a2, a3 are defined as:

    a1 = ∀x∀y∀z(Rxy → (Ryz → Rxz))

    a2 = ∀x(Rxx)

    a3 =∀x∀y(x̸=y→Rxy∨Ryx)

    We have theory, Γ = {a1, a2, a3} and for :
    Γ ⊢ ∀x∀y(Rxy → (Ryx))

    We must show that deduction exists.

    Similar examples from exercise chain use Generalization Theorem, Rule T, axioms and other meta-theorems to do so.

    How might I go about solving this? Thanks in advance for the help!
    Follow Math Help Forum on Facebook and Google+

  2. #2
    MHF Contributor
    Joined
    Oct 2009
    Posts
    5,513
    Thanks
    769

    Re: Trouble with formal deduction in first order logic

    So Γ says that R is strict total order. The fact that it is total is not essential for this problem. First, do you understand how to show informally that R is asymmetric? Second, just as the same thought or algorithm can be expressed in many natural or programming languages, the same formula can be proved in many proof systems. There is Hilbert system, natural deduction, sequent calculus and so on. I would guess that your textbook uses Hilbert system. It is easy to prove meta-theorems about it, but it is extremely inconvenient to use it in practice unless one has a sufficient supply of meta-theorems. Besides, derivations depend on what connectives are regarded as primitive (again, unless one first proves suitable properties of non-primitive connectives).

    Could you describe the system you are using? And is your question about the "most natural" derivation assuming all necessary meta-theorems are available?
    Follow Math Help Forum on Facebook and Google+

  3. #3
    Newbie
    Joined
    Mar 2013
    From
    Moscow
    Posts
    3

    Exclamation Re: Trouble with formal deduction in first order logic

    Thanks!

    So for #1 I think its easy to informally show R is asymetric. We basically use contradiction to say that if Rxy, then consider the contradiction if Rxy → Ryx.
    If so, then from a1, it means that Rxx holds, but for Rxx to hold, then there is a contradiction on a2.

    As for #2, I'm not 100% sure what is the framework we use exactly, but it seems to he the Hilbert system. We use the book A Mathematical Introduction To Logic, by Herbert B Endorton, and the specific chapter is 2.4 Deductive Calculus. To clarify more, we are allowed to use the axioms:

    Note a, b, t correspond to alpha, beta and tau

    1. First-order tautologies
    2. ∀xa → ↵axt where t is substitutable for x in a.
    3. ∀x(a → b ) → (∀xa → ∀xb),
    4. a → ∀xa where x does not occur free in a.
    5. x = x
    6. x=y → (a→a'), where a is atomic and a' is obtained from a by replacing x in zero or more (but not necessarily all) places by y.
    7. Modus poenens
    These meta/languages and theorems are also explicitly mentioned so we can for sure use them:

    Generalization on constants
    Existence of alphabetic variants
    Generalization theorem
    Rule T
    Contraposition
    Reductio ad absurdum

    Hope I answered what you needed!
    Follow Math Help Forum on Facebook and Google+

  4. #4
    MHF Contributor
    Joined
    Oct 2009
    Posts
    5,513
    Thanks
    769

    Re: Trouble with formal deduction in first order logic

    I'll write the required derivation is the so-called flag notation, also known as Fitch-style calculus. A derivation in the flag notation is a vertical list of formulas with different indents, which indicate nested scopes of applications of meta-theorems that remove assumptions, such as the deduction theorem and Reductio ad Absurdum (RAA). E.g., suppose D is a derivation of ψ from Γ and φ and suppose we apply the deduction theorem to D to derive φ → ψ. This is written as follows:

    \begin{array}{|c|}\hline \varphi\\\hline \multicolumn{1}{|c}{D}\\ \multicolumn{1}{|c}{\psi}\\ \multicolumn{1}{l}{\hspace{-.7em}\varphi\to\psi\hspace{-3em}} \end{array}

    or

    Code:
    φ
      D
      ψ
    φ → ψ
    in plain text (hence the "flag notation"). That is, the part of the meta-derivation that depends on the assumption φ is indented. (I write "meta-derivation" because in a derivation, or deduction, according to Enderton, every formula that is not an axiom or assumption is derived from previous formulas by Modus Ponens (MP). Here we may also use meta-theorems, such as the deduction and generalization theorems, so this is more like a script to construct a derivation in a proper sense.)

    The vertical list consists of three columns. The first is a step number, the second is a formula with a possible indent, and the third is the name of a rule of inference or a meta-theorem. I'll use ∀E (universal elimination) as the name for the derivation of \alpha^x_t from \forall x\,\alpha using MP and axiom 2). Similarly, ∀I (universal introduction) is a synonym for the generalization theorem, →I (implication introduction) is a synonym for the deduction theorem, →E (implication elimination) is a synonym for MP and I (negation introduction) is a synonym for RAA.

    Code:
     1. ∀xyz (Rxy → Ryz → Rxz)	a1
     2. Rxy → Ryx → Rxx		1: ∀E
     3. Rxy				Assumption
     4.   Ryx → Rxx			2, 3: →E
     5.   Ryx			Assumption
     6.     Rxx			4, 5: →E
     7.     ∀x Rxx			a2
     8.     Rxx			7: ∀E
     9.   Ryx			5, 6, 8: I
    10. Rxy → Ryx			3, 9: →I
    11. ∀xy (Rxy → Ryx)		10: ∀I
    Note that ∀I, ∀E, →I, →E and so on are primitive inference rules (not meta-theorems) in natural deduction, unlike in Hilbert calculus used by Enderton. You can see how much more natural (pun intended) constructing derivations in natural deduction is as opposed to Hilbert calculus, at the expense of possibly somewhat more complicated meta-theorems like the completeness theorem.
    Follow Math Help Forum on Facebook and Google+

Similar Math Help Forum Discussions

  1. Natural Deduction: Predicate Logic. Need help!
    Posted in the Discrete Math Forum
    Replies: 10
    Last Post: August 16th 2012, 01:17 PM
  2. Natural Deduction in propositional logic
    Posted in the Discrete Math Forum
    Replies: 4
    Last Post: August 7th 2012, 07:05 AM
  3. logic problem about deduction
    Posted in the Discrete Math Forum
    Replies: 6
    Last Post: April 13th 2012, 09:34 PM
  4. Help with Logic (Natural Deduction)
    Posted in the Discrete Math Forum
    Replies: 7
    Last Post: January 12th 2010, 02:07 PM
  5. classical logic - proofs via natural deduction
    Posted in the Discrete Math Forum
    Replies: 1
    Last Post: April 25th 2009, 10:27 AM

Search Tags


/mathhelpforum @mathhelpforum