george
Posts:
800
Registered:
8/5/08
|
|
Re: If ZFC is a FORMAL THEORY ... then what is THEOREM 1 ?
Posted:
Oct 13, 2012 8:13 PM
|
|
On Oct 13, 4:30 pm, Graham Cooper <grahamcoop...@gmail.com> wrote:
> RESOLUTION IS STATED AS:
>
> ((p v q) ^ (!p v r)) -> (q v r)
>
> So you have to get
>
> xRr <-> !xRr
> p = xRr
> !p = xRr
>
> ???
>
> Mind you, only 1 inference rule is needed, modus ponens
Resolution is also complete as an "only needed" inference rule, but
these things
are not complete in the way you think. If you are using MP as your
only inference rule
then --> IS YOUR ONLY CONNECTIVE, so you have to RE-WRITE any and
everything
that started out using /\ , V , or <--> TO USE --> INSTEAD,
IF you are going to use nothing but MP.
Similarly, since resolution ONLY operates on conjunctions of
disjunctions,
IF you are going to use resolution as your only inference rule, THEN
you AGAIN
have TO REWRITE everything that PREVIOUSLY had <--> or /\ in it AS a
collection
of disjunctions.
In particular (going for resolution),
p <--> q becomes
p --> q And q --> p; so, therefore,
rRr <--> ~rRr
becomes
(rRr --> ~rRr) and (~rRr --> rRr).
--> is the wrong connective for resolution; you have to translate -->
to V in order to use resolution.
Since, by definition, p --> q means ~p V q, the above pair of converse
conditionals become
~rRr V ~rRr and rRr V rRr .
Since disjunction is idempotent, each of these two-disjunct
disjunctions becomes a ONE-junct -junction (a "unit clause"), and the
two things you are trying to "resolve" become
~rRr resolved with rRr.
If you resolve THOSE two WITH EACH OTHER then you very quickly get
THE EMPTY CLAUSE, which is a "proof of false", which proves that the
original collection
of disjunctions was inherently contradictory, which is exactly the
result you want,
since this REALLY IS a paradox.
|
|
