Post what you've tried so far, pointing out what you're not sure about.

Two Universal Eliminations and I get to p(x,y); don't know what to do next?

Two Universal Eliminations and I get to p(x,y); don't know what to do next? — Rayan

Usually a good idea to use different variable names when you add or remove quantifiers, so you remember they're not the same variables.

((And use the reply button so people helping you know you answered.))

It depends on what logical system you are using. In many axiomatisations of first-order predicate logic there is an axiom schema of Universal Quantification that allows you to put a universal quantification before a formula of any variable that is free in the formula. Doing that to p(x,y) for first x and then y gives the desired result.

How is the conclusion different from the premise (other then lexically)? What am I missing?

I think it's asking the student to prove that universal quantifiers commute with one another, which is not given as an axiom in most logical systems, but can be proven. Existential quantifiers also commute with one another. But universal and existential quantifiers do not commute with one another.

The fact that notation has no bearing on meaning doesn't seem like something you would need to prove, no? Postulate maybe, but not as an axiom but as a meta-rule.

We have to be careful using the word 'meaning' in logic, because in natural language 'meaning' is associated with 'semantics', but semantics in logic refers to a whole new area involving models and interpretations, which need not be invoked when we are just talking about theorem proving as above.

In the absence of an Interpretation, in the full model-theory sense of that word, there is no meaning of the symbol string ∀y.∀x.p(y,x). It is just a symbol string that is syntactically correct in a given language and from which can be deduced various different but logically equivalent symbol strings using the available logical and non-logical axioms and rules of inference.

A cleaner example is the two strings

∀x.q(x)

and

(r → r) ∧ ∀x.q(x)

The two are syntactically very different, but logically equivalent in most logical systems.
In the absence of a selected Interpretation, would one say they mean the same thing? Logic theory is silent on that question.


EDIT: As pointed out by @Cabbage Farmer, this proves something different from what's in the OP. I'll leave this here to avoid confusion, and post a proof that relates to the actual question below.

The proof, using the rules of a Hilbert System, and referencing logical axioms, axiom schemas and metatheorems using the labels in that link, is:

1. ∀y.∀x.p(y,x) ⊢∀y.∀x.p(y,x)
2. ∀y.∀x.p(y,x) ⊢∀y.∀x.p(y,x) → ∀x. p(y,x) [Q5 with x:=x]
3. ∀y.∀x.p(y,x) ⊢∀x.p(y,x) [Modus Ponens on 1, 2]
4. ∀y.∀x.p(y,x) ⊢∀x.p(y,x)→ p(y,x) [Q5 with y:=y]
5. ∀y.∀x.p(y,x) ⊢p(y,x) [Modus Ponens on 3, 4]
6. ∀y.∀x.p(y,x) ⊢∀y.p(y,x) [Generalisation metatheorem on 5]
7. ∀y.∀x.p(y,x) ⊢∀x.∀y.p(y,x) [Generalisation metatheorem on 6]
8. ⊢∀y.∀x.p(y,x)→∀x.∀y.p(y,x) [deduction theorem (metatheorem) on 7]

We can then switch x and y and follow the same steps to prove that

⊢ ∀x.∀y.p(y,x)→∀y.∀x.p(y,x)

and putting the two together we get

⊢∀y.∀x.p(y,x) ↔∀x.∀y.p(y,x)

So we have proven that the two are logically equivalent, despite being syntactically very different. Sometimes the symbol ≡ is used to denote full syntactic equivalence, as distinct from logical equivalence (↔). That can be useful when alternate forms of notation are used in the same system. For instance when writing in a Hilbert system, in which the only official operators are ¬ and →, it is sometimes convenient to use the symbols ∨ and ∧ as shortcuts, so that (a∨b) is shorthand for (¬a→b) and (a∧b) is shorthand for ¬(a→¬b). Then one could write (a∨b) ≡ (¬a→b) meaning that, on a formal level, the two are syntactically identical because the LHS is just an informal abbreviation for the RHS. But we could not write

∀x.q(x) ≡ (r → r) ∧ ∀x.q(x)

as the two are syntactically distinct, even though in most logics they are logically equivalent.

Not all texts distinguish between ↔ and ≡ which I think is a pity because the distinction is often useful when one is using extended symbol sets.

Syntactically equivalent, as opposed to logically equivalent - thank you, that is what I was getting at. The premise and the conclusion in the OP problem are syntactically equivalent, unless I am missing something.

∀x.∀y.p(x,y) ≡ ∀y.∀x.p(y,x)

Syntactically equivalent means that the symbol strings, once any language-extension abbreviations have been replaced by their equivalents in the core language, are identical. The strings are not identical, so they are not syntactically equivalent.

Why are they not identical? It is a commonly accepted rule of the meta-language, i.e. the formal or semi-formal language that is used to write logical expressions, regardless of the particular logical system being used, that variable substitution can be used sensu veritate. The LHS of the above formula can be transformed into the RHS using only the rules of the meta-language, with no reference to any logical axioms or theorems.

What do you mean by a meta-language? In FOPL all we have are a language, logical axioms and rules of inference.

x and y are implicitly bound variables, so there's an ambiguity involved:

∀x∈S ∀y∈T p(x,y) = ∀y∈S ∀x∈T p(y,x) ✓

∀x∈S ∀y∈T p(x,y) ⇔ ∀y∈T ∀x∈S p(y,x) ? commutative type thing

@SophistiCat, are you referring to the former? If so, then I'd say you're right.

@Rayan may be referring to the latter, under some system, with some rules, not specified in the opening post.

By meta-language I mean the implicit convention, under which, among other things, the strings x and y are interpreted as the names of variables. The meta-language is what enables us to parse the formulas in the OP without knowing anything about the particular logical system in use; without the implicit assumption of the meta-language convention andrewk's own reply to the OP would not make sense.

Depending on the system of rules of inference you have at hand, it could be as simple as
1) ∀x.∀y.p(x,y) Premise
1 2) ∀y.p(a,y) 1, Universal Elimination
1 3) p(a,b) 2, Universal Elimination
1 4) ∀x.p(a,x) 3, Universal Introduction
1 5) ∀y.∀x.p(y,x), 4, Universal Introduction
6) ∀x.∀y.p(x,y) -> ∀y.∀x.p(y,x) 1,5 Conditional Introduction

Perhaps you are referring to the fact that variable names have no meaning and can be freely swapped, a fact regularly used in physics when we want to change the summation index for an Einstein sum. That is correct, but we don't need any meta-rules to justify it. We just do something along the lines of what I wrote above, using the logical axioms of the system. I think the general approach is as follows:

Say we have a formula F that uses variable a, and we want to replace a everywhere by b, where b is a variable symbol not currently used anywhere in a. Then we can do this as follows:

- List all the sub-formulas of F in which a is universally quantified. Call them F1,....Fn. We only need to consider universal quantification because existential quant can be written in terns of universal quant and negation.
- Use the logical axiom Q5 (axiom schema of specification) together with Modus Ponens, to replace 'a' by 'b' in all the subformulas.
- Use the Generalisation Theorem to put '∀b' in front of each subformula.
- By reversing that, we can show that each subformula is logically equivalent to the version that has all 'a's replaced by 'b's.
- It is laborious, but not difficult, to show that F <-> F', where F' is F with 'a' changed to 'b' in all subformulas in which 'a' is universally quantified.
- We may have some free instances of 'a' remaining in F'. To get rid of those, we first use the Generalisation Theorem to put ∀a in front of F', call that F''.
- We then use Q5 again to replace all free 'a's by 'b' and remove the ∀a.

We now have a formula F'' that is logically equivalent to F, but has all instances of 'a' replaced by 'b'.

All a bit laborious, but what it demonstrates is that we don't need any meta-powers to swap variable names. It can be justified by the logical axioms themselves.

I can't resist the temptation to use one of my favourite words - this means that variable symbols are fungible, which means they can be freely swapped, like electricity, money or natural gas. Their fungibility can be proven by the logical axioms, and the problem in the OP is a particular example of that general fungibility.

Yes; thank you. Well, I came here to find the answer to a simple question and I ended up learning much more, so thanks to everyone. And, by the way, I was asked to use the Fitche System to derive the conclusion.

Thank you for your patient explanations. It will take me more work to completely follow your Hilbert system derivation, but I trust that it is sound.

However... I am compelled to resist some more. So we can formally derive the variable swapping rule in at least some formal systems. This is all well and good, but I don't think that this is relevant. Because before we can interpret the formulas in the OP in any system, we have to do some preliminary interpretation, which includes parsing the symbols x and y as arbitrary (fungible) variable names. So that variable swapping rule? We have already helped ourselves to it before we even settled on a formal system for interpreting the expressions. To then prove what we already assumed using the axioms and rules of a particular system is unnecessary and question-begging.

What do you think?

I am not sure but I have a feeling you are referring to this, the semantic interpretation of a logical language.

To make a logical theory meaningful, we usually need need to have interpretations to which it applies and that are important to us. There are a few exceptions such as Godel's incompleteness theorem, but generally theories are only interesting if they have interpretations. In the fourth para of that linked section it talks about how quantified expressions involving variables can be interpreted in the model. Does that relate to the concerns you outline above?

For the case of the OP, it is purely a syntactical exercise, devoid of any interpretation.

⊢∀y.∀x.p(y,x) ↔∀x.∀y.p(y,x) — andrewk

It seems the task indicated in the OP is to prove

∀y.∀x. p(y,x)

starting from the premise

∀x.∀y.p(x,y)

It's not just the order of the quantifiers that's reversed, but also the order of the relation -- from p(x, y) to p(y, x).

Is that covered in the proof you provided?


Such a curious form of relation!

D'oh! You are right. What a silly mistake.

Here is a proof that addresses the actual question being asked. We need to introduce another variable z because when swapping two things completely, we need to use a third as a transit point.

@SophistiCat This error of mine may have contributed to some of the crossed wires on this. Sorry about that.

1. ∀x.∀y.p(x,y) ⊢∀x.∀y.p(x,y)
2. ∀x.∀y.p(x,y) ⊢∀x.∀y.p(x,y) → ∀y. p(z,y) [Q5 with x:=z]
3. ∀x.∀y.p(x,y) ⊢∀y.p(z,y) [Modus Ponens on 1, 2]
4. ∀x.∀y.p(x,y) ⊢∀y.p(z,y)→ p(z,x) [Q5 with y:=x]
5. ∀x.∀y.p(x,y) ⊢p(z,x) [Modus Ponens on 3, 4]
6. ∀x.∀y.p(x,y) ⊢∀z.p(z,x) [Generalisation metatheorem on 5]
7. ∀x.∀y.p(x,y) ⊢∀z.p(z,x)→ p(y,x) [Q5 with z:=y]
8. ∀x.∀y.p(x,y) ⊢p(y,x) [Modus Ponens on 6,7]
9. ∀x.∀y.p(x,y) ⊢∀x.p(y,x) [Generalisation metatheorem on 8]
10.∀x.∀y.p(x,y) ⊢∀y.∀x.p(y,x) [Generalisation metatheorem on 9]
11. ⊢∀x.∀y.p(x,y)→∀y.∀x.p(y,x) [deduction theorem (metatheorem) on 10]

We can then switch y and x and follow the same steps to prove that

⊢ ∀y.∀x.p(y,x)→∀x.∀y.p(x,y)

and putting the two together we get

⊢∀x.∀y.p(x,y)↔∀y.∀x.p(y,x)

I think that's right but if I've mixed up any letters while rearranging it, please let me know.