| |
 |
|
|
Science Forum Index » Logic Forum » -- Deduction Theorem
Page 1 of 1
|
| Author |
Message |
| William Hale |
 Posted: Thu Apr 24, 2008 7:08 pm |
|
|
|
Guest
|
I am reading Mendelson's "Introduction to Mathematical Logic".
On page 30, he defines what it means for a wf A to be a consequence of a
set Gamma of wfs, denoted by:
Gamma |- A.
My problem is that I want to do the following:
Given:
Gamma |- A.
Delta |- B.
Gamma subset Delta.
Gamma |- A is already proved.
Delta |- B is being proved.
On page 30, Mendelson says the proof of "Delta |- B" is a sequence B_1,
...., B_n of wfs such that B = B_n and, for each i, either A_i is an
axiom or A_i is in Delta, or A_i is a direct consequence by some rule of
inference of some of the preceding wfs in the sequence. However, my
problem is that I want to also allow B_i to be equal to some previous
theorem, provided the hypotheses Gamma of that theorem are a subset of
Delta. In the above example, I would like to be allowed to have a B_i =
A.
I couldn't find any reference to this situation in the book or in the
exercises (didn't spend a lot of time looking though).
Of course, I can transform "Gamma |- A" to "|- G_1 -> G_2 ... -> A" and
proceed from there.
I guess what I am asking for is why does Mendelson's definition of a
proof not allow you to refer to previous theorems.
As an aside, it would also be nice to replace the condition "Gamma
subset of Delta" with the condition "Gamma subset of Delta union prior
B_i's".
Bill Hale |
|
|
| Back to top |
|
| MoeBlee |
| Posted: Thu Apr 24, 2008 7:08 pm |
|
|
|
Guest
|
On Apr 24, 5:08 pm, William Hale <h...@tulane.edu> wrote:
Quote: I guess what I am asking for is why does Mendelson's definition of a
proof not allow you to refer to previous theorems.
To do so would mess up some technicalities (especially, it would
complicate the definition, since it would then require that the
definition be an inductive definition). However, we can still show
that inserting a previous proof into a proof results in a proof,
which is as good as needed to acheive the "practical" result that, we
can insert a previously proven formula into a proof (and leave tacit
that, actually technically, what we're inserting is not just the
previously proven formula but its proof too).
By the way, when it comes to the deduction theorem, e.g., Enderton's
system is much less complicated than Mendelson's.
MoeBlee |
|
|
| Back to top |
|
| David C. Ullrich |
| Posted: Fri Apr 25, 2008 8:13 am |
|
|
|
Guest
|
On Thu, 24 Apr 2008 19:08:57 -0500, William Hale <hale@tulane.edu>
wrote:
Quote: I am reading Mendelson's "Introduction to Mathematical Logic".
[...]
I guess what I am asking for is why does Mendelson's definition of a
proof not allow you to refer to previous theorems.
The question is whether (i) we're interested in finding specific
proofs in the system or (ii) we're interested in proving results
_about_ the system.
In a system that we want to actually use to prove things of
course we want to allow previously proved results. Which is
why they're allowed in ordinary mathematical proofs. But
when studying logic per se we're more interested in proving
things _about_ the system. If so then we want to make the
definition of the system as simple as possible.
Quote: As an aside, it would also be nice to replace the condition "Gamma
subset of Delta" with the condition "Gamma subset of Delta union prior
B_i's".
Bill Hale
David C. Ullrich |
|
|
| Back to top |
|
| |
|
Page 1 of 1
All times are GMT - 5 Hours
The time now is Tue Oct 07, 2008 3:38 am
|
|