Thread: logic problem about deduction

This is Exercise 3 of Section 2.5 of Enderton's "A mathematical introduction to logic".

Assume that ⊢ ϕ and that P is a predicate symbol which occurs
neither in nor in ϕ. Is there a deduction of ϕ from in which
P nowhere occurs?Suggestion: There are two very different approaches
to this problem. The "soft" approach makes use of two
languages, one that contains P and one that does not. The "hard"
approach considers the question whether P can be systematically
eliminated from a given deduction of ϕ from .
__________________________________________________ ________________________

I don't know how to start from the "soft" approach , so I choose the "hard" approach .
Suppose {a1 , ... , an} is a deduction of ϕ from ,
I tried to replace all P in{a1 , ... , an} by another predicate symbol Q, and obtain {a1' , ... , an'} (I don't know can I assume that there is another predicate symbol in this language)
I want to show that {a1' , ... , an'} is still a deduction of ϕ from , but I am stuck here.
Any help will be appreciated.

I'm a little fuzzy on the question. Is it asking whether any given entailment can always be deduced using only those predicate symbols which are contained in both the conclusion and set of assumptions?

Also, it may be helpful to know the logical system that you're using, e.g. is it a Hilbert-style set of axioms together with modus ponens and a quantifier rule? What are the axioms and rules?

Anyway, if you just replace P with some Q, presumably your Q occurs either in the conclusion or one of the assumptions, in which case the switch is not generally harmless. The switch may change a valid proof into an invalid proof. (If the Q does not occur in the conclusion or premises then switching serves no purpose, given that I understand the assignment. If Q does not occur elsewhere, then when you switch you're again left with a proof where some predicate does not occur in the premises or conclusion.)

Originally Posted by ragnar

I'm a little fuzzy on the question. Is it asking whether any given entailment can always be deduced using only those predicate symbols which are contained in both the conclusion and set of assumptions?

-- I think maybe It is enough to find a deduction of ϕ from in which P nowhere occurs? But if we can use only those predicate symbols which are contained in \Gamma or ϕ , it will be better.

Originally Posted by ragnar

Also, it may be helpful to know the logical system that you're using, e.g. is it a ? What are the axioms and rules?

-- Yes, I use Hilbert-style set of axioms together with modus ponens and a quantifier rule.

Originally Posted by ragnar

Anyway, if you just replace P with some Q, presumably your Q occurs either in the conclusion or one of the assumptions, in which case the switch is not generally harmless. The switch may change a valid proof into an invalid proof. (If the Q does not occur in the conclusion or premises then switching serves no purpose, given that I understand the assignment. If Q does not occur elsewhere, then when you switch you're again left with a proof where some predicate does not occur in the premises or conclusion.)

--OK, thanks. I think I need a more systematically elimination, but I can't find it.

I think the "soft" approach uses the soundness and completeness theorems.

The idea of the hard approach is that any parameter or a free variable can be systematically replaced throughout a derivation by something else, and the resulting formula sequence is be a valid derivation. That is, an n-ary predicate symbol P can be replaced by a formula in the sense that every occurrence of for some terms is replaced by . Similarly, a constant can be replaced by any term. The replacement has to be done in every formula of the derivation, including the axioms. So, for example, P can be replaced by the formula x = x (alternatively, by ~(x = x)) for a fresh variable x.

This works because such substitution converts axioms into axioms. Also, if in the original derivation Modus Ponens was aplied to A -> B and A, the substitution converts these formulas into some A' -> B' and A', so MP is again applicable. Formally, one proves that a derivation remains valid by induction on the length of the derivation.

This is just an outline; feel free to discuss the details.

Originally Posted by emakarov

I think the "soft" approach uses the soundness and completeness theorems.

The idea of the hard approach is that any parameter or a free variable can be systematically replaced throughout a derivation by something else, and the resulting formula sequence is be a valid derivation. That is, an n-ary predicate symbol P can be replaced by a formula in the sense that every occurrence of for some terms is replaced by . Similarly, a constant can be replaced by any term. The replacement has to be done in every formula of the derivation, including the axioms. So, for example, P can be replaced by the formula x = x (alternatively, by ~(x = x)) for a fresh variable x.

This works because such substitution converts axioms into axioms. Also, if in the original derivation Modus Ponens was aplied to A -> B and A, the substitution converts these formulas into some A' -> B' and A', so MP is again applicable. Formally, one proves that a derivation remains valid by induction on the length of the derivation.

This is just an outline; feel free to discuss the details.

Thank you, is the "soft" approach look like this?
Let L be the language that contains P , L' be the language that doen't contain P.
if Γ ⊢ ϕ in L, by soundness, Γ ⊨ ϕ in L
and because P occurs neither in Γ nor in ϕ, so in L' , Γ ⊨ ϕ is also right . (I am not sure this make sense)
so by completeness, Γ ⊢ ϕ in L' , i.e. , there is a deduction of ϕ from Γ in which P nowhere occurs.

and I also try the "hard" approach,
but in the induction, i don't know how to explain or proof "such substitution converts axioms into axioms"?
and is the number of formula Q's variables(X1,...,Xn) must be n? (Assume that P is n-ary predicate symbol) can I just replace P by the formula x=x?(Assume that the Language have equality symbol, otherwise, must have another predicate symbol Q, and I can use Q to replace P , but maybe Q is not n-ary)

Originally Posted by Alexya

but in the induction, i don't know how to explain or proof "such substitution converts axioms into axioms"?

For example, you need to show that replacing P with some formula turns a tautology into a tautology, i.e., a substitutional instance of a propositional tautology.

Originally Posted by Alexya

and is the number of formula Q's variables(X1,...,Xn) must be n? (Assume that P is n-ary predicate symbol)

No. It's like a definition of a function. When you define an n-argument function:

f(x1, ..., xn) = rhs

the left-hand side must have n variables, but the right-hand side does not have to include all, or even any, of those variables. The fact that is used in the proof is that P t1 ... tn for fixed arguments t1 ... tn is always replaced by the same formula.

Originally Posted by emakarov

For example, you need to show that replacing P with some formula turns a tautology into a tautology, i.e., a substitutional instance of a propositional tautology.

No. It's like a definition of a function. When you define an n-argument function:

f(x1, ..., xn) = rhs

the left-hand side must have n variables, but the right-hand side does not have to include all, or even any, of those variables. The fact that is used in the proof is that P t1 ... tn for fixed arguments t1 ... tn is always replaced by the same formula.

OK, I got it. Thanks a lot !!
and how about the "soft" one?

Originally Posted by Alexya

Let L be the language that contains P , L' be the language that doen't contain P.
if Γ ⊢ ϕ in L, by soundness, Γ ⊨ ϕ in L
and because P occurs neither in Γ nor in ϕ, so in L' , Γ ⊨ ϕ is also right . (I am not sure this make sense)
so by completeness, Γ ⊢ ϕ in L' , i.e. , there is a deduction of ϕ from Γ in which P nowhere occurs.

I'm not sure whether this line is true or not:
and because P occurs neither in Γ nor in ϕ, so in L' , Γ ⊨ ϕ is also right . (I am not sure this make sense)