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!

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?

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 → ↵a^{x}_{t} 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!

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:

$\displaystyle \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

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 $\displaystyle \alpha^x_t$ from $\displaystyle \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.